Model Checking with Finite Complete Prefixes is PSPACE-complete

Reference:

Keijo Heljanko. Model checking with finite complete prefixes is PSPACE-complete. In Catuscia Palamidessi, editor, Proceedings of the 11th International Conference on Concurrency Theory (Concur'2000), volume 1877 of Lecture Notes in Computer Science, pages 108–122, State College, Pennsylvania, USA, August 2000. Springer-Verlag.

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.

Keywords:

net unfoldings, temporal logics, PSPACE-completeness

Suggested BibTeX entry:

@inproceedings{Heljanko:Concur2000,
    address = {State College, Pennsylvania, USA},
    author = {Keijo Heljanko},
    booktitle = {Proceedings of the 11th International Conference on Concurrency Theory (Concur'2000)},
    editor = {Catuscia Palamidessi},
    month = {August},
    pages = {108--122},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {Model Checking with Finite Complete Prefixes is {PSPACE}-complete},
    volume = {1877},
    year = {2000},
}