Complexity Results for Model Checking

The complexity of model checking branching and linear time
temporal logics over Kripke structures has been addressed in e.g. [SC85,
CES86]. In terms of the size of the Kripke model and the length of the
formula, they show that the model checking problem is solvable in
polynomial time for CTL and NP-complete for L(F). The model checking
problem can be generalised by allowing more succinct descriptions of
systems than Kripke structures. We investigate the complexity of the
model checking problem when the instances of the problem consist of
a formula and a description of a system whose state space is at most
exponentially larger than the description. Based on Turing machines,
we define compact systems as a general formalisation of such system
descriptions. Examples of such compact systems are K-bounded Petri
nets and synchronised automata, and in these cases the well-known
algorithms presented in [SC85, CES86] would require exponential space in
term of the sizes of the system descriptions and the formulas; we present
polynomial space upper bounds for the model checking problem over
compact systems and the logics CTL and L(X,U,S). As an example of
an application of our general results we show that the model checking
problems of both the branching time temporal logic CTL and the linear
time temporal logics L(F) and L(X,U, S) over K-bounded Petri nets are
PSPACE-complete.