Abstract:
The complexity of model checking branching and linear time
temporal logics over Kripke structures has been addressed by Clarke, Emerson,
and Sistla, among others. 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 
-bounded Petri nets and synchronised automata,
and in these cases the well-known algorithms presented by Clarke, Emerson,
and Sistla (1985,1986) 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 -bounded Petri nets are
PSPACE-complete.
Available as PostScript, PDF, DVI.