Sciweavers

Share
CONCUR
2000
Springer

Model Checking with Finite Complete Prefixes Is PSPACE-Complete

12 years 3 months ago
Model Checking with Finite Complete Prefixes Is PSPACE-Complete
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.
Keijo Heljanko
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where CONCUR
Authors Keijo Heljanko
Comments (0)
books