Reference:
Keijo Heljanko. Model checking with finite complete prefixes is PSPACEcomplete. 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. SpringerVerlag.
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 PSPACEcomplete in the size of a finite complete prefix of a 1safe Petri net. This proof employs a class of 1safe Petri nets for which it is easy to generate a finite complete prefix in polynomial time.
Keywords:
net unfoldings, temporal logics, PSPACEcompleteness
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 = {108122},
publisher = {SpringerVerlag},
series = {Lecture Notes in Computer Science},
title = {Model Checking with Finite Complete Prefixes is {PSPACE}complete},
volume = {1877},
year = {2000},
}
