@inproceedings{
    Heljanko:Concur2000,
    editor = "Palamidessi, Catuscia",
    author = "Heljanko, Keijo",
    publisher = "Springer-Verlag",
    title = "Model Checking with Finite Complete Prefixes is {PSPACE}-complete",
    url = "http://users.ics.tkk.fi/kepa/publications/",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of the 11th International Conference on Concurrency Theory (Concur'2000)",
    address = "State College, Pennsylvania, USA",
    abstract = "Unfoldings are a technique for verification of concurrent and distributed systems introduced by McMillan. The method constructs a finite complete prefix, which can be seen as a symbolic representation of an interleaved reachability graph. We show that model checking a fixed size formula of several temporal logics, including LTL, CTL, and CTL*, is PSPACE-complete in the size of a finite complete prefix of a 1-safe Petri net. This proof employs a class of 1-safe Petri nets for which it is easy to generate a finite complete prefix in polynomial time.",
    month = "August",
    volume = "1877",
    juforank = "1",
    flags = "SA-LO-00-02",
    year = "2000",
    keywords = "net unfoldings, temporal logics, PSPACE-completeness",
    pages = "108--122"
}