The complexity of propositional linear temporal logics in simple cases.
It is well known that model checking and satisfiability for PLTL are PSPACE-complete. By contrast, very little is known about whether there exist some interesting fragments of PLTL with a lower worst-case complexity. Such results would help understand why PLTL model checkers are successfully used in practice. In this article we investigate this issue and consider model checking and satisfiability for all fragments of PLTL obtainable by restricting (1) the temporal connectives allowed, (2) the number of atomic propositions, and (3) the temporal height. 2002 Elsevier Science (USA).
INTRODUCTION
Background. PLTL is the standard linear-time propositional temporal logic
used in the specification and automated verification of reactive systems [MP92,
Eme90]. It is well-known that model checking and satisfiability for PLTL are
PSPACE-complete [SC85, HR83, Wol83]. This did not deter some research
groups from implementing PLTL model checkers or provers, and using them successfully
in practice [BBC Hol97]. The fundamental question this
raises is "what makes PLTL feasible in practice ?".
To this question, the commonanswer starts with the observation that the PSPACE
complexity only applies to the formula part of the problem [LP85], and it is only
a worst-case complexity. Then, it is often argued that the PLTL formulae used
in actual practical situations are not very complex, have a low temporal height
This article is a completed version of [DS98].
S. DEMRI AND PH. SCHNOEBELEN
(number of nested temporal connectives) and are mainly boolean combinations of
simple eventuality, safety, responsiveness, fairness, . properties.
Certainly the question calls for a systematic theoretical study, aiming at turning
the above answers into formal theorems and helping understand the issue at hand.
If we consider for example SAT, the famous Boolean Satisfiability problem, there
are current in-depth investigations of tractable subproblems (e.g., [Dal96, FV98]).
Regarding PLTL, we know of no systematic study of this kind in the literature.
This is all the more surprising when considering the wide use of PLTL model
checkers for reactive systems.
Our objectives. In this article, we develop a systematic study, looking for natural
subclasses of PLTL formulae for which complexity decreases. The potential
results are (1) a better understanding of what makes the problem PSPACE-hard,
(2) the formal identification of classes of temporal formulae with lower complex-
ity, called simple cases, (3) the discovery of more efficient algorithms for such
simple cases. Furthermore, since PLTL is the most basic temporal logic, simple
cases for PLTL often have corollaries for other logics.
As a starting point, we revisit the complexity questions from [SC85] when
there is a bound on the number of propositions and/or on the temporal height of
formulae. More precisely, let us write H 1 , H 2 , . for an arbitrary set of linear-time
combinators among {U, F, X, .} and let L k
.) denote the fragment of
restricted to formulae (1) only using combinators H 1 , ., (2) of temporal
height at most k, and (3) with at most n distinct atomic propositions. In this
article we measure the complexity of model checking and satisfiability for all
these fragments.
The choice of this starting point is very natural, and it is relevant for our original
motivations:
. For the propositional calculus and for several modal logics (K45, KD45, S5,
von Wright's logic of elsewhere, . ), satisfiability becomes linear-time when at
most n propositions can be used (see [Hal95, Dem96]). By contrast, satisfiability
for K remains PSPACE-complete even when only one proposition is allowed.
What about PLTL ?
. In practical applications, the temporal height often turns out to be at most
(or 3 when fairness is involved) even when the specification is quite large and
combines a large number of temporal constraints. This bounded height is often
invoked as a reason why PLTL model checking is feasible in practice. Can this be
made formal ?
Our contribution.
1. Our first contribution is an evaluation of the computational complexity of
model checking and satisfiability for all L k
fragments. A table in section
8 summarizes this.
2. We also identify new simple cases for which the complexity is lowered (only
NP-complete). For these we give (non-deterministic) algorithms. We think it
is worth investigating whether the ideas underlying these algorithms could help
develop deterministic algorithms that perform measurably better (on the relevant
simple case) than the usual methods. These results also have implications beyond
PLTL: e.g. NP-completeness of PLTL without temporal nesting (Prop. 7.4) leads
to a # P
model checking algorithm for CTL + and FCTL [LMS01].
3. A third contribution is the proof techniques we develop: we show how a
few logspace reductions allow to compute almost all the complexity measures
we needed (only a few remaining ones are solved with ad-hoc methods). These
reductions lead to a few rules of thumb (summarized in section 8) that can be
used as guidelines. Additionally, some of our reductions transform well-known
problems (SAT or QBF) into model checking problems for formulae with a simple
structure (e.g., low temporal height) and can be used in other contexts. The second
author used them for very restricted fragments of CTL+Past [LS00].
We believe that these constructions are interesting in their own right and think
that the scarcity of available proofs and exercices suitable for a classroom frame-work
is unfortunate when PLTL model checking is now widely taught in computer
science curriculums.
Related work. It is common to find papers considering extensions of earlier
temporal logics. The search for fragments with lower complexity is less
common (especially works considering model checking). [EES90] investigates
(very restricted) fragments of CTL (a branching-time logic) where satisfiability
is polynomial-time. [KV98] studies particular PLTL formulae for which there is
a linear-sized equivalent CTL formula: one of the aims is to understand when
and why PLTL model checking often behaves computationally well in practice.
[BK98] tries to understand why Mona performs well in practice and isolates a fragment
of WS1S where the usual non-elementary blowup does not occur. [Hal95]
investigates, in a systematic way, the complexity of satisfiability (not model check-
ing) for various multimodal logics when the modal height or the number of atomic
propositions is restricted: in fact PLTL is quite different from the more standard
multimodal logics and we found it behaves differently when syntactic restrictions
are enforced. In [Hem00], the complexity of fragments of modal logics is also
4 S. DEMRI AND PH. SCHNOEBELEN
studied by restricting the set of logical (boolean and temporal) operators. These
fragments are mainly relevant for description logics (see, e.g., [DLNN97]).
As far as PLTL is concerned, some complexity results for some particular restricted
fragments of PLTL can be found in [EL87, CL93, Spa93, DFR00] but
these are not systematic studies sharing our objectives. [Har85] has a simple
proof, based on a general reduction from tiling problems into modal logics, that
satisfiability for L(F, X) is PSPACE-hard. In fact, the same proof (or the proofs
from [Spa93, DFR00]) shows that PSPACE-hardness is already obtained with
temporal height 2.
Finally, there is a special situation with L(F) and L(X). These two very limited
fragments of PLTL actually coincide (semantically) with, respectively, the
modal logics S4.3Dum (also called S4.3.1 or D) [Bul65, Seg71, Gor94] and
NP-completeness of S4.3Dum satisfiability has been first proved
in [ON80] and generalized in [Spa93] to any modal logic extending the modal logic
S4.3. The complexity of L(X) satisfiability is also studied in [SR99].
Plan of the article. Section 2 recalls various definitions we need throughout
the article. Sections 3 and 4 study the complexity of PLTL fragments when the
number of atomic propositions is bounded. Logspace transformations from QBF
into model checking can be found in Section 5 and Section 6. Section 7 studies the
complexity of PLTL fragments when the temporal height is bounded. Section 8
contains concluding remarks and provides a table summarizing the complete picture
we have established about complexity for PLTL fragments.
2. BASIC DEFINITIONS AND RESULTS
Computational complexity. We assume that the reader understands what is
meant by complexity classes such as L (deterministic logspace), NL (non-de-
logspace), P (polynomial-time), NP and PSPACE, see e.g. [Pap94].
Given two decision problems P 1 and there exists a
logspace transformation (many-one reduction) from P 1 into P 2 . In the rest of the
article, all the reductions are logspace, and by "C-hardness" we mean "logspace
hardness in the complexity class C".
Temporal logic. We follow notations and definitions from [Eme90]: PLTL is a
propositional linear-time temporal logic based on a countably infinite set P
propositional variables, the classical boolean connectives
#, and the temporal operators X (next), U (until), F (sometimes).
The set {#, .} of formulae is defined in the standard way, using the connectives
# and G (always) as abbreviations with their standard meaning. We
let |#| denote the length (or size) of the string #, assuming a reasonably succinct
encoding.
Following the usual notations (see, e.g., [SC85, Eme90]), we let L(H 1 , H 2 , .)
denote the fragment of PLTL for which only the temporal operators H 1 , H 2 , .
are allowed 3 . For instance L(U) is "PLTL without X", as used in [Lam83].
denotes the set of propositional variables occurring in #. The temporal
height of #, written th(#), is the maximum number of nested temporal operators in
#. We write L k
.) to denote the fragment of L(H 1 , .) where at most n # 1
propositions are used, and at most temporal height k # 0 is allowed. We write
nothing for n and/or k (or we use #) when no bound is imposed: L(H 1 ,
For example, for # given as
and
Flat Until. We say a #, of the form #U# , uses flat Until when
the left-hand side, #, does not contain any temporal combinator (i.e., # is a boolean
combination of propositional variables) and we write #U - # when we want to
stress that this occurrence of U is flat. E.g., we sometimes write (AU - B)UC for
(AUB)UC.
To the best of our knowledge, Dams was the first to explicitely isolate and name
this restricted use of Until 4 and prove that U - is less expressive than U [Dam99].
He argued that flat Until is often sufficiently expressive in practice, and hoped
model checking and satisfiability would be simpler for U - than for U. In the
following, we treat U - as if it were one more PLTL combinator, more expressive
than F but less than U.
Semantics. A linear-time structure (also called a model) is a pair (S, #) of an
#-sequence . of states, with a mapping
labeling each state s i with the set of propositions that hold in s i . We often only
write S for a structure, and use the fact that a structure S can be viewed as an
infinite string of subsets of P rop. Let S be a structure, i # N a position, and # a
formula. The satisfiability relation |= is inductively defined as follows (we
omit the usual conditions for the propositional connectives):
. S, i |= A def
. S, i |= X# def
. S, i |= F# def
3 Negations are allowed. For instance, L(F) and L(G) denote the same fragment.
4 But flat fragments of temporal logics have been used in many places, e.g. [MC85, DG99, CC00].
6 S. DEMRI AND PH. SCHNOEBELEN
. S, i |= #U# def
# there is a j # i such that S, j |= and for all
We
Satisfiability. We say that a formula # is satisfiable iff S |= # for some S.
The satisfiability problem for a fragment L(.), written SAT (L(.)), is the set
of all satisfiable formulae in L(.
Model checking. A Kripke structure #) is a triple such that N
is a non-empty set of states, R # N - N is a total 5 next-state relation, and
labels each state s with the (finite) set of propositions that hold
in s. A path in T is an #-sequence . of states of N such that
path in T is a linear-time structure and a linear-time
structure is a possibly infinite Kripke structure where R is a total function.) We
follow [Eme90, SC85] and write T , s |= # when there exists in T a path S starting
from s such that S |= # 6 . The model checking problem for a fragment L(.),
written MC(L(.)), is the set of all #T , s, # such that T , s |= # where T is finite
and # is in L(. For the definition of |T |, the size of T , we use a reasonably
succinct encoding of In practice, it is convenient to pretend
Complexity of PLTL. As far as computational complexity is concerned we
make a substantial use of the already known upper bounds:
Theorem 2.1. [ON80, HR83, SC85]
SAT (L(F)) and MC(L(F)) are NP-complete.
SAT (L(F, X)), MC(L(F,X)), SAT (L(U)) andMC(L(U)) are PSPACE-complete.
As a consequence, most of our proofs establish lower bounds.
Stuttering equivalence. Two models are equivalent modulo stuttering, written
they display the same sequence of subsets of P rop when repeated
(consecutive) elements are seen as one element only (see [Lam83, BCG88] for a
Only considering Kripke structures with total relations is a common technical simplification. Usually
it has no impact on the complexity of temporal logic problems. However the "total R" assumption
implies that any two states satisfy the same temporal formulae in L #
fragment for which
satisfiability is trivial. In "non-total R" frameworks there is a branching-time formula that behaves
as a propositional variable. This can impact complexity: satisfiability for the fragment of K with no
propositions is PSPACE-complete in a "non-total R" framework [Hem00], and is in L in a "total R"
framework.
6 This existential formulation is well suited to complexity studies because it makes model checking
closer to satisfiability. It is the dual of the definition used in verification ("all paths from s satisfy #"),
so that all complexity results for model checking can be easily translated, modulo duality, between the
two formulations.
formal definition). Lamport argued that one should not distinguish between stutter-
equivalent models and he advocated prohibiting X in high-level specifications since
Theorem 2.2. [Lam83] S # S # iff S and S # satisfy the same L(U) formulae.
3. BOUNDING THE NUMBER OF ATOMIC PROPOSITIONS
In this section we evaluate the complexity of satisfiability and model checking
when the number of propositions is bounded, i.e. for fragments L n (.
When the number of propositions is bounded, satisfiability can be reduced to
model checking:
Proposition 3.1. Let H 1 , . be a non-empty set of PLTL temporal combi-
nators. Then for any n # N, SAT (L n (H 1 , .)) #L MC(L n (H 1 , .
Proof. Take # L n (H 1 , .) such that P rop(# {A 1 , . , A n }. Let
#) be the Kripke structure where N def
is the set of all 2 n
relates any two states, and for all s # N , s is its own
One can see that # is satisfiable iff there is a s # N s.t.
For a many-one reduction, we pick any s 0 # N and use
The reduction is logspace since n, and then |T |, are constants.
Prop. 3.1 is used extensively in the rest of the article. Note that the reduction does
not work for an empty set of combinators, as could be expected since SAT (L())
is NP-complete while MC(L()) amounts to evaluating a boolean expression and
is in L [Lyn77]. Also, Prop. 3.1 holds when n is bounded and should not be
confused with the reductions from model checking into satisfiability where one
uses additional propositions to encode the structure of T into a temporal formula
(used in, e.g., [SC85, Eme90]).
3.1. PSPACE-hardness with few propositions
The next two propositions show that, for model checking problems, n propositional
variables can be encoded into only two if U is allowed, and into only one
one if F and X are allowed.
Proposition 3.2. MC(L(H 1 , .)) #L MC(L 2 (U)) for any set H 1 , . of
temporal operators.
8 S. DEMRI AND PH. SCHNOEBELEN
Proof. With a Kripke structure #) and a formula # L(H 1 , .)
such that P we associate a Kripke structure D n
#s, i#R #s # ,
sRs # and
{} otherwise.
Fig. 1 displays an example. Here alternations between A and
s
A,B
A,B
A
A
A
A
A
A
FIG. 1. T and D3 (T ) - An example
-A in D n (T ) define visible "slots", the #s, 2j + 2#'s, that are used to encode the
truth value of the propositional variables: B in the i-th slot encodes that P i holds.
be given by
Alt 0
At D Alt k+1
At D is satisfied in D n (T ) at all #s, j# with only there. Alt k
the fact that there remain k "A-A" alternations before the next state satisfying
At D .
We now translate formulae over T into formulae over D n (T ) via the following
inductive definition:
This gives the reduction we need since
for any s #
Clearly the construction of D n (T ) can be done in space O(log(|T | + |#|)) and the
construction of D n (#) can be done in space O(log |#|).
Observe that D n (# L 2 (U - ) when # L(F, X). Combining with Theorem
2.1 we obtain
Corollary 3.1. MC(L 2 (U - )) is PSPACE-complete.
Proposition 3.3. MC(L(H 1 , .)) #L MC(L 1 (X, H 1 , .)) for any set
. of PLTL temporal operators.
Proof. With a Kripke structure #) and a formula # L(H 1 , .)
such that P
#s, j#R #s # ,
#s, 1#s, 2#) def
{} otherwise.
Fig. 2 displays an example.
S. DEMRI AND PH. SCHNOEBELEN
s
A
A
A
A
A
A
A
FIG. 2. T and C3 (T ) - An example
The idea is to use -A.A (resp. -A.-A) in the i-th slot after a A.A to encode
that P i holds (resp. does not hold). The A.A is a marker for the beginning of some
s and the -A in a #s, 2j + 1# is to distinguish slots for starting a new s and slots
for a P i . We now translate formulae over T into formulae over C n (T ) via the
following inductive definition:
with At C
-A. Clearly, At C is satisfied in C n (T ) at all #s, j#
only there. For any s # N , we have T , s |= # iff C n (T ), #s, 1# |=
Finally, the construction of C n (T ) can be done in space O(log(|T |+|#|)) and the
construction of C n (#) can be done in space O(log |#|).
Combining with Theorem 2.1 we obtain
Corollary 3.2. MC(L 1 (F, X)) is PSPACE-complete.
Similar results exist for satisfiability problems:
Proposition 3.4. For H 1 , . a set of PLTL temporal operators,
Proof. (1) Let # L(H 1 , .) be such that P
be the formula
#G  At D # At DU -A # -B # ((-A # -B)U - Alt n
describes the shape of models that have the form of some D n (S). More
formally, one can show that for any model S, D n (S) |= #
n and for any S # over
{A, B}, if S # n then there exists a (unique) S such that S # D n (S). Then
an L n (H 1 , .) formula # is satisfiable iff the L 2 (U, H 1 , .) formula #
is satisfiable. We already know that D n (#) can be built in space O(log |#|).
Moreover, #
n can be also built in space O(log |#|) since we already know that
Alt n
n can be built in space O(log n) which is a fortiori in space O(log |#|).
.) such that P be the
describes the shape of models of the form C n (S): for any model S, C n (S) |=
# n and for any S # over {A} if S # n then there exists a (unique) S such that
S # is (isomorphic to) C n (S). Then the L n (H 1 , .) formula # is satisfiable iff the
(#) is satisfiable. We already know that C n (#)
can be built in space O(log |#|). Moreover, # n can be also built in space O(log |#|)
since we need to count until n which requires space in O(log n). So, computing
space in O(log |#|).
the proof of Proposition 3.4 also shows that
Combining with Theorem 2.1, we get
Corollary 3.3. SAT (L 2 (U - are PSPACE-complete.
3.2. NP-hardness with few propositions
We now show that MC(L 2 are NP-hard using Prop. 3.1
and
Proposition 3.5. SAT (L 0
Proof. We consider structures on P Say S has n A-alternations
iff there exist positions
that k. Hence S contains an alternation of
2n consecutive non-empty segments : A holds in the first and all odd-numbered
segments, A does not hold in even-numbered segments. Then there is an infinite
suffix where A holds continually.
Let us define the following formulae:
. # 0
. #
. #
One can check that # n [# 0 that a structure has n # A-alternations
for some n # n. Thus
is a formula with size in O(n), stating that the modelS has exactly nA-alternations.
An A-alternation is a segment composed of an A-segment followed by an -A-
segment. For l # {A, -A}, an l-segment is a (non-empty) finite sequence of states
where l holds true. Generally, # n [#] expresses that there is n # n such that #
holds at some state belonging to the n # th A-alternation in which -A also holds.
When S has exactly n A-alternations, we can view it as the encoding of a
valuation v S of {P 1 , . , P n } by saying that P k holds iff both B and -B can
be found in the k-th -A-segment in S. Formally, v S
# iff there exist
We now encode a propositional formula # over {P 1 , . , P n } into f n (#), an
L(F)-formula with
and the obvious homomorphic rules for # and -. One can see that, for S with n
A-alternations, v S |= # iff S |= f n (#), so that # is satisfiable iff f n (# n is
The proof is completed by checking that f n (# n is an L #
2 (F)-formula that can
be computed from # in space O(log |#|) .
The transformation from 3SAT into MC(L(F)) in [SC85] only uses formulae
of temporal height 1. Here we provide a logspace transformation from 3SAT into
using only formulae with two different propositional variables.
Proposition 3.6. 3SAT #L MC(L #
Proof. Consider an instance I of 3SAT. I is a conjunction V m
clauses,
where each C i is some disjunction W 3
l i,j of literals, where each l i,j is a propositional
variable x r(i,j) or the negation -x r(i,j) of a propositional variable from
W.l.o.g. we assume that n # 3 - m and that, for any i, the
r(i, are all distinct.
We consider the structure T n labeled with propositions A and B as in Figure 3.
Observe that T n only depends on n, the number of different boolean variables
occuring in I.
A
A
A
FIG. 3. The structure
With a path S from s 0 , we associate a valuation v S
=#). Symmetrically, any valuation
v is v S for a unique path S in T n .
For
, an L(F) formula stating that v S does not satisfy
clause C i . This is done in several steps: define
and, for
l i,j is x r or its negation.
Because it involves alternations between -(A#B) andA#B,# r
i cannot be satisfied
starting from s n-r # for r # > r. Thus, if S |= # 0
i , the rth positive occurence of A
or B or A # B is necessarily satisfied in t r or u r . Hence
Now define # I
I is satisfiable. Finally, both
I can be computed in space O(log |I|).
Corollary 3.4. MC(L 2 are NP-complete.
14 S. DEMRI AND PH. SCHNOEBELEN
4. FRAGMENTS WITH ONLY ONE PROPOSITION
In this section, we give a polynomial-time algorithm for L #
1 (U) that relies on
linear-sized B- uchi automata.
Recall that the standard approach for PLTL satisfiability and model checking
computes, for a given PLTL formula #, a B- uchi automaton 7
A# recognizing
exactly the models of # (the alphabet of the B- uchi automaton is the set of possible
valuations for the propositional variables from #).
Satisfiability of # is non-emptiness of A# . Checking whether a path in some T
satisfies # is done by computing a synchronous product of T and A# and checking
for non-emptiness of the resulting system (a larger B- uchi automaton) This method
was first presented in [WVS83], where a first algorithm for computing A# was
given.
The complexity of this approach comes from the fact that A# can have exponential
size. Indeed, once we have A# the rest is easy:
Lemma 4.1. [Var94] It is possible, given a B-uchi automaton A recognizing
the models of formula #, and a Kripke structure T , to say in non deterministic
space O(log|T | log|A|) whether there is a computation in T accepted by A.
From these remarks, it easily follows that fragments of PLTL will have low
complexity if the corresponding A# are small.
4.1. The fragment L #(U)
Here we consider a single proposition: P linear model is
equivalent, modulo stuttering, to one of the following: for n # N
-A # , S ndef
3 and S n
6 do not depend on n.
Now a satisfiable L #
Lemma 4.2. For any
# iff S n
7 or a Muller automaton, or an alternating B- uchi automaton, or .
Proof. By structural induction on # and using the fact that the first suffix of a S n
is a S n #
e.g. the first suffix of S n
1 is S n-1
and the
first suffix of S n
2 is S n
1 .
Recognizing the S n
i 's is easy:
Lemma 4.3. For any 1 # i # 6 and n # N, there exists a B-uchi automaton
A =n
i and a B-uchi automaton A #n i s.t. A =n
accepts a model S iff
Furthermore, the A =n
's and A #n i 's have O(n) states and can be generated uniformly
using log n space.
Proof. We only show A 2
3 as examples (see Fig. 4.1).
A =2
A =n
FIG. 4. B- uchi automata for Lemma 4.3
Combining lemmas 4.1 and 4.3, we see that the problem of deciding, given T
with s 0 a state, given n # N and 1 # i # 6, whether there is a path S in T that starts
from s 0 and s.t. S # S n
i , can be solved in non deterministic space O(log(n- |T |))
or in deterministic time O(n - |T |). Similarly, the problem of deciding whether
there is a path S and a m # n s.t. S
i can be solved with same complexity.
Theorem 4.1. Model checking for L #
1 (U) is in P.
Proof. Consider a Kripke structure #) and some state s 0 # N .
If there is a path S from s 0 satisfying # L #
and some
Conversely, if S n
and there is a path
i starting from s 0 , then T , s 0 |= #.
It is possible to check whether T contains such a path in polynomial-time: We
consider all
seen in time O(k.|#|), we check
S. DEMRI AND PH. SCHNOEBELEN
in time O(k.|T |), whether, from s 0 , T admits a path S # S k
i . We also consider all
know that S k+m
so that it is correct to check whether there is a m such that T admits a path S #
. Because k #|, the complete algorithm only needs O(|T |-|#| 2 )-time.
Remark 4. 1. We do not know whether MC(L #
1 (U)) is P-hard. We only know
it is NL-hard 8 . The same open question applies to SAT (L #
Looking at the algorithm used in the proof of Theo. 4.1, it appears 9 that this
open question is linked to an important open problem that remained unnoticed for
many years:
Open Problem 4.1. What is the complexity of model checking a path?
Here a "path" is a finitely presented linear-time structure. It can be given by a
deterministic Kripke structure (i.e., where any state has exactly one successor) or
by an #-regular expression u.v # where u and v are finite sequences of valuations.
Model checking a path is clearly in P but it is not known whether it is P-hard or
in NL or somewhere in between.
4.2. The fragment L #
Proposition 4.2. SAT (L #
1 (X)) are NP-complete.
Proof. Satisfiability for L(X) is in NP because, for # L(X) with temporal
height k, it is enough to guess the first k states of a witness S. Model checking
also is in NP for the same reason.
NP-hardness of SAT (L #
1 (X)) can be shown by a reduction from 3SAT: consider
a boolean formula # with propositional variables P 1 , . , P n and replace the
A's: the resulting L #
is. Then, by Prop. 3.1,
1 (X)) is NP-hard too.
Proposition 4.3. For any k, n < #, SAT (L k
(U, X)) is in L.
Proof. Here the key observation is that there are only a finite number of
essentially distinct formulae in a given fragment L k
Given n and k, one
can compute once and for all a finite subset J k
that
8 One easily shows that already MC(L 1
1 is NL-hard by a reduction from GAP, the graph accessibility
problem of [Jon75].
9 M. Y. Vardi pointed out the connection to us.
1. any # L k
equivalent to a # i # J k
is the canonical
representative for #);
2. for i #= j, i and j are not equivalent. Then a given # is satisfiable iff its
canonical representative is not the canonical representative of #.
Any J k
n is finite and, more precisely, |J 0
and |J k+1
n | is in 2 2 O(|J k
We assume n and k are fixed and we consider the problem, given #, of computing
its canonical representative (or equivalently its index 1 # i # N ). This can be
done in a compositional way: if # i and # j then the representative # k of
#U# (say) is the representative of # i U# j , so that we just need to compute once
and for all a finite table t U : (i,
operators, temporal or boolean.
Once we have these tables, computing the canonical representative of any #
amounts to evaluating an expression over a fixed finite domain,which can
be done in logspace (see [Lyn77]).
Proposition 4.4. For any k, n < #, MC(L k
(U, X)) is in NL.
Proof. As in the proof of Prop. 4.3, for # L k
logspace
a canonical representative
. By Lemma 4.1, checking whether T , s |= i
can be done in non deterministic space O(log |T | log |A i |). Since n and k are
fixed, is a constant, so that MC(L k
(U, X)) is in
NL.
1 is NL-hard (Remark 4.1), we get
Corollary 4.1. For any 1 # k < # and 1 # n < #, for any set H 1 , . of
temporal operators, MC(L k
By contrast, by [Lyn77], MC(L 0
# (U, X)) is in L.
This concludes the study of all fragments with a bounded number of proposi-
tions. In the remaining of the article, this bound is removed.
5. FROM QBF TO MC(L(U))
In this section, we offer a logspace transformation from validity of Quantified
Boolean Formulae (QBF) into model checking for L(U) that involves rather simple
constructions of models and formulae. This reduction can be adapted to various
fragments and, apart from the fact that it offers a simple means to get PSPACE-
hardness, we obtain a new master reduction from a well-known logical problem.
S. DEMRI AND PH. SCHNOEBELEN
As a side-effect, we establish that MC(L 2
is PSPACE-hard, which is not
subsumed by any reduction from the literature.
Consider an instance I of QBF. It has the form
I # Q
z }| {
where every Q r (1 # r # n) is a universal, #, or existential, #, quantifier. I 0
is a propositional formula without any quantifier. Here we consider w.l.o.g. that
I 0 is a conjunction of clauses, i.e. every l i,j is a propositional variable x r(i,j) or
the negation -x r(i,j) of a propositional variable from
question is to decide whether I is valid or not. Recall that
Lemma 5.1. I is valid iff there exists a non-empty set V #} X of
valuations such that
correctness:
closure: for all v # V , for all r such that Q #, there is a v # V such that
With I we associate the Kripke structure T I as given in Figure 5, using labels
1 , . AssumeS is an infinite path starting
. A n
FIG. 5. The structure T I associated with I # Q1x1 . Qnxn # m
from s 0 . Between s 0 and s n , it picks a boolean valuation for all variables in X ,
then reaches wm and goes back to some B r -labeled state (1 # r # n) where
(possibly distinct) valuations for x r , x r+1 , . , x n are picked.
In S, at any position lying between a s n and the next wm , we have a notion of
current valuation which associates # or # with any x r depending on the latest u r
or t r node we visited. With S we associate the set V(S) of all valuations that are
current at positions where S visits s n (there are infinitely many such positions).
Now consider some r with Q assume that whenever S visits s r-1
then it visits both t r and u r before any further visit to s r-1 . In L(U), this can be
Let # clo
clo , then V(S) is closed in the sense
of Lemma 5.1.
Now, whenever S visits a L j
-state, we say it agrees with the current valuation v
if v |= l i,j . This too can be written in L(U), using the fact that the current valuation
for x r cannot be changed without first visiting the B r -state. For
then V(S) is correct in the sense
of Lemma 5.1.
Lemma 5.2. Let # I
I is valid.
Proof. If S |= # I , then V(S) is non-empty, closed and correct for I so that I
is valid. Conversely, if I is valid, there exists a validating V (Lemma 5.1). From V
one can build an infinite path S starting from s 0 such that
from a lexicographical enumeration of V , S is easily constructed so that S |= clo .
Then, to ensure S |= corr , between any visit to s n and to the next wm , S only visits
-states validated by the current valuation v, which is possible because v |= I 0 .
It is worth observing that # I belongs to L 2
I and
# I can be computed from I in logspace, and because th(# I using
Prop. 3.2), we get
Corollary 5.1. QBF #L MC(L 2
Corollary 5.2. MC(L 2
are PSPACE-hard.
6. FROM QBF TO MC(L(F, X))
As in section 5, we consider an instance I # Q
l i,j of
QBF . With I we associate the Kripke structure T #
I given in Figure 6. Here, any
S. DEMRI AND PH. SCHNOEBELEN
path S starting from s 0 can be seen as an infinite succession of segments of length
Each segment directly yields a valuation for X: they form an
infinite sequence v 1 , v 2 , . (necessarily with repetitions) and we let V(S) denote
the associated set.
FIG. 6. The structure T #
I associated with I # Q1x1 . Qnxn # m
Using F and X, it is easy to state that any segment in S visits the L j
-states
in a way that agrees with the corresponding valuation. For
Now
implies that V(S) is correct in the sense of Lemma 5.1.
There remains to enforce closure of V(S). For this, we require that the valuations
are visited according to the lexicographical ordering, and then cycling.
This means that the successive choices of truth values for universally quantified
propositional variables behave as the successive binary digits of counting modulo
(assuming there are n # universal quantifiers in Q 1 , . , Q n ). As usual, the
existentially quantified variables are free to vary when an earlier variable varied.
Assume When moving from a valuation v t to its successor v t+1 , we
require that v t remains unchanged iff for some r # > r with Q r # we have
This is written
does not change"
z }| {
r
{ r | Q restricted to the universally quantified variables,
behaves like counting modulo 2 n # .
Assume now that Q r #. When moving from v t to its successor, v t
not change unless v t #, or equivalently
for the latest r < r # with Q (thanks to our assumption
about counting). Equivalently, this means that if for a universally quantified x r ,
does not change, then for any following existentially quantified x r # , v t
does not change either. By "following" we mean that there is no other # between
Q r and Q r # , i.e. that r # sc(r) with
This behaviour can be written:
"if v(x r ) does not change"
z }| {
r #sc(r)
"then v(x # r ) does not change"
z }| {
r #   .
Now we define
I
Lemma 6.1. T #
I , s 0 |= # I iff I is valid.
Proof. If S |= # I then V(S)validates I as we explained. Conversely, if someV
validates I, then, enumerating V in lexicographical order, it is easy to build a S such
that S |= # I .
I and #
I can be computed from I in logspace (and using
Prop. 3.3) we get
Corollary 6.1. QBF #L MC(L(F,X)) #L MC(L #
Corollary 6.2. MC(L #
7. BOUNDING THE TEMPORAL HEIGHT
In this section we investigate the complexity of satisfiability and model checking
when the temporal height is bounded. From Section 5, we already know that
22 S. DEMRI AND PH. SCHNOEBELEN
We first consider ways of reducing the temporal height (sections 7.1 and 7.2).
Then we show how to improve the upper bounds when temporal height is below 2
(sections 7.3 and 7.4).
7.1. Elimination of X for model checking
Assume T is a Kripke structure and k # N. It is possible to partially unfold T
into a Kripke structure T k where a state s (in codes for a state s 0 in T with the
k next states s 1 , . , s k already chosen. In T k , s is labeled with new propositions
encoding the fact that some s i 's satisfy some A j 's.
Formally, let k # N and P First let P rop k def
defined as the Kripke
structure
.
R and for any j # {1, . , k},
This peculiar unraveling is also called bulldozing (see e.g. [Seg71]). Fig. 7 contains
a simple example. Observe that |T k
| is in O(|T | k+1 ) and T k can be computed in
A
FIG. 7. An example of bulldozing: T and T 2 side by side
space O(log(k
Say a formula # has inner-nexts if all occurrences of X are in subformulae of
the form XX . XA (where A is a propositional variable).
If now # has inner-nexts, with at most k nested X, and if we replace all X i A j in
# by propositions A i
, we obtain a new formula, denoted # k , such that
starting with s. (1)
Both T k and # k can be computed in space O(log(|T |
Not all formulae have inner-nexts but, using the following equivalences
as left-to-right rewrite-rules, it is possible to translate any PLTL formula into an
equivalent one with inner-nexts. This translation may involve a quadratic blow-up
in size but it does not modify the number of propositional variables or the temporal
height of the formula 10 .
Corollary 7.1. For any k # N and set H 1 , . of PLTL temporal combina-
tors, MC(L k
Proof. Given # in L k
# (X, .), and someT , we transform # into some equivalent
# with inner-nexts and then evaluate # k on T k .
Corollary 7.2. MC(L k
# (X)) is in L and MC(L k
# (F, X)) is in NP for any
fixed k # 0.
# NP-hard as can be seen from the proof of NP-hardness of
# in [SC85]. Hence for k # 1, MC(L k
7.2. Elimination of X for satisfiability
Elimination of X for satisfiability relies on the same ideas. If # is satisfiable,
then, thanks to (1), # k is. The converse is not true: consider # given as GA#G-XA,
clearly not satisfiable. Here # 1 is GA 0
#G-A 1 which is satisfiable. This is because
if # k is satisfiable, then it may be satisfiable in a model that is not a S k for some
S. But, using an L 2
express the fact that a given model is
a S k , so that
# is satisfiable iff # k
Actually, this approach based on standard renaming techniques can get us fur-
ther. We write # A} to denote a formula obtained by replacing all occurences
These rules may introduce X's in the right-hand side of U - 's but this will be repaired when we
later replace the X i A j 's with the A i
's.
S. DEMRI AND PH. SCHNOEBELEN
of # with A inside #. If A does not occur in #, then
# is satisfiable iff # A} # G(A #) is.
By using this repeatedly and systematically, we can remove (by renaming) all
and, (2) there exists at least one occurence of #
in # that is under the scope of two temporal combinators (or in the left-hand side
of a U). For example, F(AU(FGB # GB)) is replaced by F(AU(FA 1
new #
new
new # GB) in turn replaced by
new # A 1
new
new # GB) #
new # FA 1
new ).
Starting from some #, this repetitive construction eventually halts (when no #
can be found), the resulting formula # has temporal height at most 2, uses flat
until, and is satisfiable iff # is. It can be computed in logspace, so that
Proposition 7.1. For any set H 1 , . of PLTL temporal combinators,
Corollary 7.3. SAT (L 2
are PSPACE-hard

7.3. Satisfiability without temporal nesting
We now consider formulae in L 1
# (U, X), i.e. without nesting of temporal opera-
tors. The main result is
Proposition 7.2. Assume # L 1
# (U, X). If # is satisfiable then it is satisfiable
in a model S . such that for any i, j #(s i
Such a S # can be guessed and checked in polynomial time, hence
Corollary 7.4. For any set H 1 , . of PLTL temporal combinators,
is in NP, and hence is NP-complete.
We now proceed with the proof of Prop. 7.2. Our main tool is a notion of
extracted structure:
Definition 7.1. An extraction pattern is an infinite sequence n 0 <
. of increasing natural numbers. Given an extraction pattern (n i ) i#N and a
structure S, the extraction from S along (n i ) i#N is the structure s # 0 , s # 1 , . where,
a copy of s n i
Now consider a formula # L 1
# (U, X). Since # has temporal height 1, it is a
boolean combination of atomic propositions and of temporal subformulae of the
form X or U # where # and # have temporal height 0. For example, with #
given as
the temporal subformulae of # are
Definition 7.2. From any
# (U, X), we
extract a set of positions, called the witnesses for # in S. The rules are that 0 is
always a witness, and that each temporal subformula of # may require one witness:
1. for a temporal subformula X#, 1 is the witness,
2. for a temporal subformula #U# , we have three cases
(i) if S |= #U# and i is the smallest position such that S, i |= # , then i is
the witness. (Observe that for all j < i, S, j |= # .)
(ii) if S #|= F# , then no witness is needed.
(iii) otherwise S #U# and S |= F# . Let i be the smallest position such
that S, i #, then i is the witness. (Observe that S, i # and for all j < i,
Clearly, if {n 0 , are the witnesses for #, then k < |#|.
We continue our earlier example: let S be the structure
S: A
A
A
A
A
A
where C never holds. Here S |= #. Indeed, S |=
S |= XA and S #|= AUC. The witness for XA is 1. The witness for
is 6 since we are in case (a) from definition 7.2, and s 6 is the first position where
holds. No witness is needed for AUC since we are in case (b). The witness for
AUB is 4 since we are in case (c) and s 4 is the first position where A does not
hold. Finally, the witnesses for # are {0, 1, 4, 6}.
Lemma 7.1. Let # L 1
# (U, X) and S be a structure. Let (n i ) i#N be an
extraction pattern containing all witnesses for # in S. Let S # be the structure
extracted from # along (n i ) i#N . Then for any subformula # of #, S |= # iff
26 S. DEMRI AND PH. SCHNOEBELEN
Proof. By induction on the structure of #. Since all other cases are obvious, we
only need deal with the case # 1 U# 2 and show that S # 1 U# 2 iff S |= # 1 U# 2 .
Assume S |= # 1 U# 2 . Let i be the witness for # 1 U# 2 . So S, i |= # 2 and, for any
appears in S # as some s # n and all s # n # for n # < n
are (copies of) s j 's for j < i, hence S # 1 U# 2 (remember that # 1 and # 2 have
no temporal operator.)
Now assume S # 1 U# 2 . If # 1 U# 2 has no witness, then no s
and therefore no s is the witness for # 1 U# 2 , then
appears as s # n in S # : we
have
We may now conclude the proof of Prop. 7.2: Consider now a satisfiable #
# (U, X) and assume S |= #. Let {n 0 , . , n k } be the witnesses for # in S.
We turn these into an extraction pattern by considering the sequence n 0 <
prolongated by some n k+1 < n k+2 < . where the n k+i are positions
of states carrying the same valuation (there must be at least one valuation appearing
infinitely often). The extracted S # has the form required for Prop. 7.2.
Continuing our previous example, and assuming the valuation of s 6 appears
infinitely often, the resulting S # is made out of s 0 , s 1 , s 4 and s 6 , and it satisfies #:
A
7.4. Model checking without temporal nesting
We now consider model checking of formulae where the temporal height is at
most 1.
Proposition 7.3. MC(L 1
# (U, X)) is in NP.
Proof. Consider # L 1
# (U, X) and assume T , s |= #. Then there is a path S
in T starting from s such that S, s |= #.
The witnesses for # in S are some We consider an extraction
pattern containing all witnesses of W and such that the extracted S # be a path
in T : this may imply to retain some positions from S, between a n i # W and the
following to ensure connectivity in T . In any case, it is possible to find an
extraction pattern where n k appears as some position l # k - |T |.
Therefore, if T , s |= # then this can be seen along a path S of the form
|. Guessing this path and
checking it can be done in non deterministic polynomial-time.
#
Corollary 7.5. For any set H 1 , . of PLTL temporal combinators,
8. CONCLUDING REMARKS
In this article we have measured the complexity of model checking and satisfiability
for all fragments of PLTL obtained by bounding (1) the number of atomic
propositions, (2) the temporal height, and (3) restricting the temporal operators
one allows. Table 1 provides a complete summary.
In this table we use U ? to denote any of U and U - since one outcome of our study
is that all the problems we considered have the same computational complexity
when "Until" is replaced by the weaker "flat Until", thereby ruining some hopes
of [Dam99].
Some general conclusions can be read in the table. In most cases no reduction in
complexity occurs when two propositions are allowed, or with temporal height two.
Moreover, in most cases, for equal fragments, satisfiability and model checking
belong to the same complexity class. Still the table displays some exceptions, two
of which deserve comments :
1. Model checking and satisfiability for L #
(only one proposition) are in
P. Admittedly this fragment is not very relevant when it comes to, say, protocol
verification. Moreover, it is open whether those problems are P-hard or in NL, to
quote a few possibilities.
2. Model checking for L k
This shows that F+X
can be simpler than U. Because NP-hardness is already intractable, this result
does not immediately suggest improved deterministic algorithms. However, the
isolated fragment is very relevant.
Another way to see our results is to focus on the general techniques that we
developed: we provided a simple transformation from QBF into model checking
problems, and we formalized a number of logspace transformations leading to a
few basic rules of thumb:
(1) when the number of propositions is fixed, satisfiability can be transformed
into model checking,
28 S. DEMRI AND PH. SCHNOEBELEN


1.
A complete summary of complexity measures
checking Satisfiability
L(F) NP-complete [SC85] NP-complete [ON80]
propositional variables can be encoded into
only one if F (sometimes) and X (next) are allowed,
(2.2) only two if U (until) is allowed,
(3) when arbitrarily many propositions are allowed, temporal height can be
reduced to 2 if F is allowed, and
model checking for logics with X can be transformed into model checking
without X.
Besides, when the formula # has temporal height at most 1, knowing whether
only depends on O(|#|) places in S.
Most of the time, these techniques are used to strengthen earlier hardness results,
showing that they also apply to specific fragments. In some cases we develop specific
arguments showing that the complexity really decreases under the identified
threshold values.
The general situation in our study is that lower bounds are preserved when
fragments are taken into account. Hence our investigations do not give a formal
justification of the alleged simplicity of "simple practical applications". Rather,
we show that several natural suggestions are not sufficient.
Understanding and taming the complexity of linear temporal logics remains an
important issue and the present work can be seen as some additional contribu-
tion. The ground is open for further investigations. We think future work could
. different, finer definitions of fragments (witness [EES90]) that can be inspired
by practical examples, or that aim at defeating one of our hardness proofs, e.g.
forbidding the renaming technique we use in sections 7.1 and 7.2,
. restrictions on the models rather than the formulae,
. other complexity measures: e.g. average complexity, or separated complexity
measure for models and formulae, or analysis of hard and easy distributions.
Additionaly, it must be noted that we only considered satisfiability and model
checking, and ignored other problems that are important for verification: module
checking, semantic entailment, .



--R





Automata based symbolic reasoning in hardware verification.
An algebraic study of Diodorean modal systems.
Flatness is not a weakness.
Another look at LTL model checking.
The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic
The complexity of theorem-proving procedures
An almost quadratic class of satisfiability problems.

Flat fragments of CTL and CTL
A simple tableau system for the logic of elsewhere.
Execution and proof in a Horn-clause temporal logic
An expressively complete temporal logic without past tense operators for Mazurkiewicz traces.
The complexity of concept languages.
Information and Computation
The complexity of propositional linear temporal logics in simple cases (extended abstract).
On the limits of efficient temporal decidability.

Modalities for model checking: Branching time logic strikes back.
Temporal and modal logic.
A perspective on certain polynomial time solvable classes of Satisfiability.

The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic.
Recurring dominos: Making the highly undecidable highly understandable.
The complexity of Poor Man's logic.
The model checker Spin.
The propositional dynamic logic of deterministic

Relating linear and branching model checking.
What good is temporal logic?
Model checking CTL
Checking that finite state concurrent programs satisfy their linear specification.
Specification in CTL
Log space recognition and translation of parenthesis languages.
Hierarchical verification of asynchronous circuits using temporal logic.
The Temporal Logic of Reactive and Concurrent Systems: Specification.
On the size of refutation Kripke models for some linear modal and tense logics.
Computational Complexity.
The complexity of propositional linear temporal logics.
An essay in classical modal logic (three vols.
Complexity of Modal Logics.
"initially"

Temporal logic can be more expressive.
Reasoning about infinite computation paths (extended abstract).
--TR
The complexity of propositional linear temporal logics
Modalities for model checking: branching time logic strikes back
Characterizing finite Kripke structures in propositional temporal logic
Temporal and modal logic
The temporal logic of reactive and concurrent systems
The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic
The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic
The complexity of concept languages
The Model Checker SPIN
Automata based symbolic reasoning in hardware verification
The logic of MYAMPERSANDldquo;initiallyMYAMPERSANDrdquo; and MYAMPERSANDldquo;nextMYAMPERSANDrdquo;
Checking that finite state concurrent programs satisfy their linear specification
Log Space Recognition and Translation of Parenthesis Languages
Specification in CTL + Past for verification in CTL
Another Look at LTL Model Checking
A perspective on certain polynomial-time solvable classes of satisfiability
Nontraditional Applications of Automata Theory
The Complexity of Propositional Linear Temporal Logics in Simple Cases (Extended Abstract)
The Complexity of Poor Man''s Logic
Model Checking CTL+ and FCTL is Hard
Relating linear and branching model checking
Flatness Is Not a Weakness
A Simple Tableau System for the Logic of Elsewhere
An Expressively Complete Temporal Logic without Past Tense Operators for Mazurkiewicz Traces
The complexity of theorem-proving procedures

--CTR
Nicolas Markey , Philippe Schnoebelen, Mu-calculus path checking, Information Processing Letters, v.97 n.6, p.225-230, 31 March 2006
Alexander Rabinovich , Philippe Schnoebelen, BTL
F. Laroussinie , Ph. Schnoebelen , M. Turuani, On the expressivity and complexity of quantitative branching-time temporal logics, Theoretical Computer Science, v.297 n.1-3, p.297-315, 17 March
Stphane Demri, A polynomial space construction of tree-like models for logics with local chains of modal connectives, Theoretical Computer Science, v.300 n.1-3, p.235-258, 07 May
S. Demri , F. Laroussinie , Ph. Schnoebelen, A parametric analysis of the state-explosion problem in model checking, Journal of Computer and System Sciences, v.72 n.4, p.547-575, June 2006
model checking;computational complexity;temporal logic;logic in computer science;verification