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.

• Type: Conference
• Year: 2000
• Where: CONCUR
• Authors: Keijo Heljanko
• Keywords: 1-safe Petri Nets, CONCUR 2000, Distributed And Parallel Computing, Finite Complete Prefix, Interleaved Reachability Graph