Algorithmic metatheorems for decidable LTL
model checking over infinite systems
Anthony Widjaja To and Leonid Libkin
LFCS, School of Informatics, University of Edinburgh
anthony.w.to,libkin@ed.ac.uk

Abstract. By algorithmic metatheorems for a model checking problem
P over infinite-state systems we mean generic results that can be used toinfer decidability (possibly complexity) of P not only over a specific classof infinite systems, but over a large family of classes of infinite systems.
Such results normally start with a powerful formalism F of infinite-statesystems, over which P is undecidable, and assert decidability when is restricted by means of an extra “semantic condition” C. We prove various
algorithmic metatheorems for the problems of model checking LTL and
its two common fragments LTL(Fs , Gs ) and LTLdet over the expressiveclass of word/tree automatic transition systems, which are generated bysynchronized finite-state transducers operating on finite words and trees.
We present numerous applications, where we derive (in a unified manner) many known and previously unknown decidability and complexity
results of model checking LTL and its fragments over specific classes of
infinite-state systems including pushdown systems; prefix-recognizable
systems; reversal-bounded counter systems with discrete clocks and afree counter; concurrent pushdown systems with a bounded number ofcontext-switches; various subclasses of Petri nets; weakly extended PAprocesses; and weakly extended ground-tree rewrite systems. In all cases,
we are able to derive optimal (or near optimal) complexity. Finally, we
pinpoint the exact locations in the arithmetic and analytic hierarchiesof the problem of checking a relevant semantic condition and the LTL
model checking problems over all word/tree automatic systems.

1

Introduction

The study of model checking over infinite-state systems is now an active researcharea. This can be justified by the plethora of real-world scenarios that can be
more conveniently modeled using infinite-state systems rather than finite-statesystems, e.g., those that typically arise as programs with unbounded data structures (including stacks, lists, and FIFO queues), numeric variables, and clocks.
To make sense of the problem of verifying infinite-state systems, the systems under consideration need to have some finite representations, e.g., timed automata,pushdown automata, counter machines, Turing machines, and so forth. Unlikein the case of finite systems, model checking even the most basic properties,
such as safety and liveness, is already undecidable over infinite-state systems
in general. For this reason, one either adopts non-Turing-powerful formalisms

2

Anthony Widjaja To and Leonid Libkin

which admit decidability or resorts to semi-algorithms for general formalisms.
Examples of formalisms that admit certain decidable model checking problems
include pushdown automata [9], higher-order pushdown automata [20], Petrinets [9], timed automata [3], lossy channel systems [1, 4], certain subclasses ofcounter machines [11, 21, 24], and classes of term/tree rewrite systems [9, 25, 31],
to name a few. On the other hand, various notions of finite-state transducers onwords/trees [2, 7, 12, 15, 29, 34] and certain extensions of counter machines [6, 11]have emerged as popular general (Turing-powerful) frameworks of infinite-statemodel checking, for some of which semi-algorithmic approaches to verifying basic model checking properties, including safety and liveness, have been proposed(e.g. see [2, 6, 8] and references therein).
The vast literature of infinite-state model checking in the past decade orso can be extremely daunting and easily obscure proof patterns that can bereused with ease to obtain model checking decidability results for seemingly unrelated formalisms of infinite-state systems. This issue motivates the study ofalgorithmic metatheorems for infinite-state model checking, which are genericresults that can be used in a “plug-and-play” manner for inferring decidabilityof certain model checking tasks over a large family of formalisms of infinite-statesystems, instead of doing so for a single formalism at a time. Of course the concept of algorithmic metatheorems is not new; the classical decidability of S2S
can be viewed as such for MSO model-checking, due to its wide applicability
via the method of interpretations. Other results of this nature include results onflat counter machines [11, 24], well-structured transition systems [4, 17], and theextension of the S2S result to Caucal hierarchy [33]. In the finite case, algorithmic metatheorems are used extensively to obtain good algorithmic bounds forevaluating logical formulae over finite structures [19].
In this paper we study generic algorithmic metatheorems for designing efficient algorithms for model checking LTL, together with two of its commonly
considered fragments LTL(Fs , Gs ) [31, 32] and LTLdet [27], over infinite-statesystems. Our choice of logic is justified by the fact that LTL, LTL(Fs , Gs ), andLTLdet can express frequently checked properties including safety and liveness,and that their model checking problem have been frequently studied in the setting of infinite-state systems (e.g. [8, 9, 22, 31]). We will use as our framework theexpressive class of word/tree automatic transition systems [7, 15, 34], which are
generated by synchronized rational transducers [12, 15] over finite words and finite ranked trees. Such systems subsume many important decidable formalisms,
including many which we previously mentioned and others, and still possess desirable closure and decidability properties (e.g. see [7, 12]), many of which are notsatisfied by the general class of rational transducers on words [29]. Since verifying
safety and liveness are in general undecidable over automatic transition systems[7], we will study various “semantic restrictions” for ensuring decidability ofLTL, LTL(Fs , Gs ), or LTLdet , without unnecessarily sacrificing applicability andalgorithmic efficiency.
Contributions We identify semantic conditions on word/tree automatic transition systems that let us conclude decidability (and complexity) of model-

Algorithmic metatheorems for LTL over infinite systems

3checking. We start with a condition (C1) stating that the reachability relation
is effectively computable and given by a synchronized rational word/tree transducer. There are many examples of classes of systems satisfying this condition(e.g. see Section 4 and Table 1) Another condition (C2) says that a class of
systems is closed under products with finite systems. We show that under (C1)and (C2), LTL model-checking is decidable with good complexity bounds: exponential in the formula, and polynomial in the size of the input automaticpresentation of the system, assuming an oracle for computing the reachability
relation.
While many classes of systems satisfy (C1), extending it to products (condition (C2)) could be problematic. Thus, we study various weakening of (C2)that could be used to obtain metatheorems for fragments of LTL. In this paper,
we look at the following fragments: (1) LTL(Fs , Gs ) with only strict F and G
operators, and (2) LTLdet of [27]. We show that restricting to (C2) to closure
under products with dag-like finite systems, or dropping (C2) altogether at theexpense of a slightly worse complexity bound, decidability (and complexity) results for LTL(Fs , Gs ) and LTLdet model checking could be retained. We also
look at variations of these results for Presburger-definable infinite systems.
We then turn to applications, and show how our metatheorems can be used
to derive (in a unified manner) known asymptotic upper bounds for LTL modelchecking over some classes of systems, or produce new (or improved) complexity
bounds for LTL and its fragment over other classes. Our results are summarizedin Table 1.
Finally, we study the degrees of undecidability for the model checking problem and the problem of checking a relevant semantic condition over all word/tree
automatic transition systems. We point out their locations in the arithmetic andanalytic hierarchies.
Organization Definitions and notations are given in Section 2. Metatheorems
are presented in Section 3. Applications are given in Section 4. Undecidability
results are described in Section 5. Due to space limitations, proofs are relegatedinto the appendix, which can be requested from the authors.
Related Work The study of logical structures generated by finite-state automata
and transducers can be traced far back (e.g., [15]). Since then, various models offinite-state automata and transducers have been studied, e.g., rational transducers on words (cf. [5, 29]), synchronized rational transducers on words and trees(cf. [5, 7, 12, 34]), synchronized rational transducers on infinite words and infinite
trees (cf. [5, 7, 8]), and length-preserving synchronized rational transducers on finite words (cf. [2]). See [5] for a detailed comparison of their expressive power.
In this paper we are concerned only with synchronized rational transducers on
finite words and trees. In the case of length-preserving rational transducers on
finite words, it is easy to show that LTL model checking is decidable under condition (C1) and (C2) (cf. [2]). The difficulty of extending this result to (notnecessarily length-preserving) synchronized rational transducers on finite words
lies in the fact that one has to deal with genuinely infinite execution paths, which

4

Anthony Widjaja To and Leonid Libkin

do not visit two states twice, in the transition systems. Such paths do not exist
when the length-preserving restriction is imposed on the transducers.
It is natural to ask whether our results hold in the case of the more generalclass of rational transducers or synchronized rational transducers on ω-words(they are actually incomparable [5]). We do not know the answer to this question
and leave this for future work. We also mention the paper [8], which offers a semialgorithmic approach to handling LTL model checking over systems generated
by deterministic-weak synchronized rational transducers on ω-words. Finally, we
mention that even though the aforementioned notions of transducers are Turingpowerful, they cannot capture all transition systems generated by higher-order
pushdown systems (cf. [5, 20]).

2

Preliminaries

Transition systems, reachability, and recurrent reachability Let ACT
be a finite set of action labels. A transition system over ACT is given as S =hS, (→a )a∈ACT i, where S is a set of states and each →a is a binary relation on
S, i.e., a subset of S × S. The set S is not required to be finite. We write →for the union of all transition relations →a (a ∈ ACT) and →+ (resp. →∗ ) todenote the transitive (resp. transitive-reflexive) closure of →.
Given a transition system S = hS, (→a )a∈ACT i and a set X ⊆ S, by
Reach∞ (S, X) we denote the set of states s ∈ S from which there exists an
infinite execution path in S visiting X infinitely often, i.e., there exists an infinite
sequence s →+ s0 →+ s1 →+ s2 →+ . . . so that si ∈ X for all i ≥ 0. We referto these sets as recurrent reachability sets.
Automata and transducers We assume basic familiarity with automata
on finite and ω-words. Let Σ be a finite alphabet. Given an automaton A =(Q, δ, q0 , F ) with states Q, initial state q0 , final states F and transition function
δ, a run of A on w = a1 . . . an (with n ≤ ω) is a function ρ : {0, . . . , n} → Q with
ρ(0) = q0 that obeys δ, i.e. ρ(i + 1) ∈ δ(ρ(i), ai+1 ). The length kρk of ρ is n. We
use abbreviations NWA and NBWA for nondeterministic (Büchi) automata.
We use synchronized rational (letter-to-letter) transducers [7] to define relations P over Σ-words, i.e., P ⊆ Σ ∗ × Σ ∗ . Such transducers are simply NWA
R over Σ⊥ × Σ⊥ , where Σ⊥ := Σ ∪ {⊥} and ⊥∈/ Σ is a padding symbol (sothat the NWA could take two input words of different length). More precisely,
given two words w = a1 . . . an and w′ = b1 . . . bm over the alphabet Σ, we define
a word w ⊗ w′ of length» k–= max{n, m} over alphabet Σ⊥ × Σ⊥ so that the′
ith letter of w ⊗ w′ is ab′i , where a′i is ai for i ≤ n, and ⊥ for i > n (andilikewise b′i = bi for i ≤ m and ⊥ for i > m). That is, the shorter word is
padded with ⊥’s, and the ith letter of w ⊗ w′ is then the pair of the ith lettersof padded w and w′ . The binary relation “recognized” by the transducer R is
the set {(w, w′ ) ∈ Σ ∗ × Σ ∗ : w ⊗ w′ ∈ L(R)}. Such a relation is also called
regular. We refer to such an automaton as a transducer over Σ ∗ , since it can beAlgorithmic metatheorems for LTL over infinite systems

5alternatively viewed as mapping words w ∈ Σ ∗ nondeterministically into words
w′ so that w ⊗ w′ is accepted by R.
Likewise we define transducers over finite k-ary trees [7, 12, 34]. In the following, we recall the definition for k = 2. A binary tree T = (D, τ ) consists of atree domain (a finite prefix-closed subset of {0, 1}∗ ) and a node labeling function
τ : D → Σ. The notation T = T1 ⊗ T2 is used to refer to a tree over the labeling2alphabet Σ⊥
similarly to the definition of w ⊗ w′ . That is, the domain of T is2
D1 ∪ D2 , and the labeling τ : D1 ∪ D2 → Σ⊥is defined as τ (u) = (a1 , a2 ) sothat ai = τi (u) if u ∈ Di and ⊥ otherwise, for i = 1, 2. With this definition, thenotion of tree transducers is defined similarly to the notion of word transducers,
as a nondeterminsitic tree automaton working on T1 ⊗ T2 . Binary relations overtrees defined that can be recognized by such transducers are called (tree) regular.
In the sequel, we use NTA (resp. NTT) for tree automata (resp. transducers).
We shall use the notations L(A) (or L(R)) for the language (or relation)
accepted by automaton (or transducer) A (or R).
Automatic presentations of transition systems We deal with infinite transition systems that can be finitely presented by automata and transducers. A
word-automatic presentation is ϑ = hA; {Ra }a∈ACT i where A is an automaton
over some finite alphabet Σ, and each Ra is a transducer over Σ. This presentation generates an automatic transition system Λ(ϑ) = hS; {→a }a∈ACT i, where
S = L(A) and →a := L(Ra ) ∩ S for each a ∈ ACT. Tree-automatic presentations
and transition systems generated by them are defined similarly except that A isa tree automaton and Ra ’s are tree transducers.
Given a transition system hS; {→a }a∈ACT i generated by a word or a treeautomatic presentation, each first-order (FO) formula ϕ(x) with one free variable(resp. ϕ(x, y) with two free variable) can effectively be converted into a word ortree automaton defining {s ∈ S | ϕ(s) is true} (resp. word or tree transducer
defining {(s, s′ ) ∈ S × S : ψ(s, s′ ) is true}. This could actually be generalized tok free variables [7].
We denote by wAutp and tAutp the classes of word-automatic and treeautomatic presentations, respectively. In the sequel, our metatheorems will talkabout subclasses C ⊆ wAutp or C ⊆ tAutp satisfying certain conditions. The
following several conditions will be tacitly assumed for such C. First, it should beeasy (i.e. in poly-time) to check membership in C. This condition has a standard
complexity-theoretic explanation: checking whether the input encoding of an
instance to a problem is valid should be easily doable. Secondly, we do not
require these classes C to be isomorphism-closed, i.e., there possibly exist two
automatic presentations ϑ ∈ C and ϑ′ ∈ C generating two isomorphic transition
systems Λ(ϑ) and Λ(ϑ′ ). In fact, asserting closure under isomorphism is toostrong as it is undecidable to check isomorphisms for automatic systems [7].
LTL The syntax of LTL over ACT isϕ, ϕ′ := a (a ∈ ACT) | ¬ϕ | ϕ ∨ ϕ′ | ϕ ∧ ϕ′ | Xϕ | ϕUϕ′ .

6Anthony Widjaja To and Leonid Libkin

We shall use the standard abbreviations: Fϕ for trueUϕ, Gϕ for ¬F¬ϕ, and Fs
and Gs for their strict versions: Fs ϕ = XFϕ and Gs ϕ = ¬Fs ¬ϕ.
Given an ω-word w ∈ ACTω , we define the satisfaction relation w |= ϕ inthe standard way. We write [[ϕ]] for the set of all w ∈ ACTω such that w |= ϕ.
It is well-known [35] that there exists an exponential-time algorithm which,given an LTL formula ϕ, computes an NBWA Aϕ satisfying L(Aϕ ) = [[ϕ]].
Given a transition system S = hS, (→a )a∈ACT i and a word u = a0 a1 a2 . . . ∈ACTω , we say that w0 ∈ S realizes u if there is a sequence of w0 , w1 , w2 , . . . ofai
wi+1 for all i ≥ 0. We then define the semantics
elements of S so that wi −→of LTL formulae in the standard way: (S, w0 ) |= ϕ iff every ω-word u ∈ ACTω
realized by w0 satisfies ϕ. We write [[ϕ]]∀S for the set of all w0 ∈ S such that(S, w0 ) |= ϕ (where ∀ means that every path starting in w0 satisfies ϕ). We
also write [[ϕ]]∃S for the complement of the set [[¬ϕ]]∀S , i.e., for the set of w0 thatrealizes at least one path satisfying ϕ.

3Metatheorems for LTL and its fragments

Since LTL formulae are translated into Büchi automata, a starting point for us isa known metatheorem that gives a semantic condition which implies bounds (andstructural properties) for recurrent reachability sets. We now define condition
on a class C of presentations in wAutp (resp. in tAutp ):(C1) There exists an algorithm AC which, given an input presentation ϑ = hA; {Ra }a∈ACT i ∈ C of the automatic transition system
Λ(ϑ) = hS; {→a }a∈ACT i, computes an NWT (resp. NTT) R+ rec+S.
ognizing the transitive closure relation →+ =a∈ACT →aIntuitively, (C1) asserts that the transitive closure relations of systems Λ(ϑ)
with ϑ ∈ C are effectively regular. We denote the running time of AC to be tAC .
The following results state that under (C1), recurrent reachability sets can becomputed with polynomial-time overhead.
Theorem 1 ([34]). Fix any class C ⊆ wAutp (resp. C ⊆ tAutp ) satisfying(C1). Given an automatic presentation ϑ ∈ C and an NWA (resp. NTA) A0 ,the set Reach∞ (Λ(ϑ), L(A0 )) is regular, for which an NWA (resp. NTA) is computable in time polynomial in kϑk + kA0 k + tAC (|ϑ|). In particular, if AC runsin poly-time, then an NWA (resp. NTA) for Reach∞ (Λ(ϑ), L(A0 )) is poly-time
computable.
3.1

A metatheorem for LTL

We now adapt Theorem 1 to produce a metatheorem for LTL. Consider a finite
system F = hQ = {q0 , . . . , qn }, δi, with δ : Q × ACT → Q. Given a presentationϑ ∈ wAutp of the system Λ(ϑ) = hS ⊆ Σ ∗ , {→a }a∈ACT i, we define F · Λ(ϑ) to
be the automatic transition system hS ′ ; {→′a }a∈ACT i as follows:– S ′ := QS := {qs : q ∈ Q, s ∈ S}; it is a regular language over S ∪ Q.

Algorithmic metatheorems for LTL over infinite systems

7– qw →′a q ′ w′ iff q ′ ∈ δ(q, a) and w →a w′ .
It is easy to give an automatic presentation ϑ′ of F · Λ(ϑ) and show that ϑ′ ispoly-time computable. For presentations ϑ ∈ tAutp , we could define F · Λ(ϑ) ina similar way (e.g. by defining the domain to be Q(S) = {q(T ) : q ∈ Q, T ∈ S}
where q(T ) is the tree obtained by attaching q to T as a root).
We now define another condition (C2) stating that the class C is closed under
products with finite systems:(C2) if ϑ ∈ C and F is a finite system then F · Λ(ϑ) ∈ C.
The following theorem is now almost immediate from Theorem 1 and thestandard translation from LTL into Büchi automata. Intuitively, it says that for
automatic presentations satisfying both (C1) and (C2), for LTL model-checking
the overhead (compared to tAC ) is polynomial in the automatic presentation andexponential in the LTL formula. In particular, if tAC is polynomial itself, thenLTL model-checking is polynomial in the size of the representation of the systemand exponential in the size of the formula.
Theorem 2. Fix any set C ⊆ wAutp (resp. C ⊆ tAutp ) satisfying both (C1)and (C2). Given ϑ ∈ C and an LTL formula ϕ, the set [[¬ϕ]]∃Λ(ϑ) is regular, for which an automaton is computable in time polynomial in kϑk + kAk +tAC (2O(kϕk) × kϑk). Thus, checking whether (Λ(ϑ), v0 ) |= ϕ can be done in timepolynomial in kϑk + kv0 k + tAC (2O(kϕk) × kϑk).
There are many examples of classes of automatic structures of interest inverification that satisfy condition (C1) (see, e.g., [34] for a list). So it is natural
to ask whether having condition (C1) for a class of automatic presentations C
implies having it for products of structures in that class with finite systems.
While we shall see some examples of classes where this happens (e.g., pushdown
systems), in general such an extension is impossible even in very simple cases,
e.g., for single structures, as the result below shows.
Proposition 3. There exist an automatic presentation ϑ satisfying (C1) anda finite system F so that in F · Λ(ϑ) the reachability relation is not regular (infact, not even recursive).
So the applicability of Theorem 2 in full generality may be rather limited. We
thus look at cases when conditions weaker than (C2) will allow us to conclude
the decidability of model-checking. They will not apply to full LTL, but they
will apply to some of its well-studied fragments. The distinguishing feature ofthese fragments is that formulae in them can be translated into special typesof Büchi automata, whose graph structures are rather nice (essentially, almost
DAGs). We next look at such cases.
3.2

Metatheorems for LTLdet

We first recall the definition of the fragment LTLdet of LTL [27].
ϕ, ϕ′ := p | Xϕ | ϕ ∧ ϕ′ | (p ∧ ϕ) ∨ (¬p ∧ ϕ′ ) |(p ∧ ϕ)U(¬p ∧ ϕ′ ) | (p ∧ ϕ)W(¬p ∧ ϕ′ ).

8Anthony Widjaja To and Leonid Libkin

Here p is a boolean combination of ACT, and ϕWϕ′ is interpreted as the formulaGϕ ∨ (ϕUϕ′ ), i.e., the “weak until” operator.
Formulae in this fragment can be translated into a special kind of automata
called 1-weak NBWAs. Formally, a 1-weak NBWA A = (Σ, Q, δ, q0 , F ) is an
NBWA with a partial order ⊆ Q × Q such that q ′ ∈ δ(q, a) implies q  q ′ .
Intuitively, the partial order ensures that once A leaves a state q, it will never
be able to come back to q. In other words, graph-theoretically A looks like a dag
possibly with self-loops.
It was shown in [27] that there exists a poly-time algorithm which, given an
LTLdet formula ϕ, computes a 1-weak NBWA A¬ϕ such that L(A¬ϕ ) = [[¬ϕ]].
(The running time was not explicitly mentioned in [27], but one can easily checkthat it is polynomial).
We now weaken the condition (C2) to the following:(C2’) if ϑ ∈ C and F is a finite system that is 1-weak then F · Λ(ϑ) ∈ C.
Combining Theorem 1 with the translation of [27], we may proceed as in the
proof of Theorem 2 and obtain the following theorem.
Theorem 4. Fix any set C ⊆ wAutp (resp. C ⊆ tAutp ) satisfying (C1) and(C2’). Given ϑ ∈ C and an LTLdet formula ϕ, the set [[¬ϕ]]∃Λ(ϑ) is regular, forwhich an automaton is computable in time polynomial in kϑk + kAk + tAC (kϕk ×
kϑk). Thus, checking whether (Λ(ϑ), v0 ) |= ϕ can be done in time polynomial inkϑk + kv0 k + tAC (kϕk × kϑk).
We now show that decidability can still be obtained without assuming condition(C2’) but by slightly strengthening condition (C1). Namely, we use a condition
stating that the transitive closure can be computed not only for → but also for
all unions of →a ’s:(C1’) there exists an algorithm AC which, given an input presentation
ϑ = hAδ ; {Ra }a∈ACT i ∈ C of the automatic transition system
Λ(ϑ) = hS; {→a }a∈ACT i and each subset ACT′ ⊆ ACT, com+putes an NWT (resp. NTT) RACT′ recognizing the transitive clo+S.
→
sure relation
′
a
a∈ACT
In practice, (C1’) is not much stronger than (C1); all our examples in thenext section which satisfy (C1) also satisfy (C1’). In this case, LTLdet modelchecking can be done in PSPACE assuming an oracle for tAC ; its running timeis only exponential in the the size of the formula.
Theorem 5. Fix any set C ⊆ wAutp (resp. C ⊆ tAutp ) satisfying (C1’).
Given a presentation ϑ ∈ C, and an LTLdet formula ϕ, checking whether(Λ(ϑ), v0 ) |= ϕ can be done in time polynomial in kϑk, kv0 k, tAC (kϑk), andexponential in kϕk. Whenever C ⊆ wAutp , the space consumed by the algorithm
is polynomial in kϑk, kv0 k, tAC (kϑk), and kϕk.

Algorithmic metatheorems for LTL over infinite systems

3.3

9

Metatheorems for LTL(Fs , Gs )Recall that in LTL(Fs , Gs ) we use operators Fs and Gs rather than U and X.
It turns out that our conditions (C1) and (C2) imply bounds on LTL(Fs , Gs )model-checking. We start with the following.
Theorem 6. Fix any set C ⊆ wAutp (resp. C ⊆ tAutp ) satisfying (C1) and(C2). Given a presentation ϑ ∈ C and an LTL(Fs , Gs ) formula ϕ, checking
whether (Λ(ϑ), v0 ) |= ϕ can be done in coNP assuming an oracle for tAC . Moreprecisely, checking whether (Λ(ϑ), v0 ) 6|= ϕ can be done in nondeterministic timepolynomial in kϑk + kv0 k + tAC (kϕk × kϑk).
The proof of this result is based on a translated into 1-weak NBWAs extended
with fairness constraints, which are conjunctions of formulae Gs Fs p, where p isa disjunction over action labels in ACT [31]. We have to extend translation
results from [31] to obtain more precise information about the structure of theautomata, and then use it to prove the result along the lines of the proof in theprevious section. Details are in the appendix.
Our second metatheorem for LTL(Fs , Gs ) uses only condition (C1) and produces slightly higher, but still acceptable, complexity bounds.
Theorem 7. Fix any set C ⊆ wAutp (resp. C ⊆ tAutp ) satisfying (C1).
Given a presentation ϑ ∈ C, and an LTL(Fs , Gs ) formula ϕ, checking whether(Λ(ϑ), v0 ) |= ϕ can be done in time polynomial in kϑk, kv0 k, tAC (kϑk), andexponential in kϕk.
3.4

A metatheorem for Presburger-definable systems

In this subsection, we will make an extra assumption that the input presentations
can be given by existential Presburger formulas. More precisely, we consider presentations of the form ϑ = hϕ(x); {ϕa (x, y)}a∈ACT i, where x and y are k-tuplesof variables for some k ∈ Z>0 and ϕ’s some existential Presburger formulas.
Such a presentation gives rise to the system Λ(ϑ) = hS; {→a }a∈ACT i, whereS = {a ∈ Nk : (N, +) |= ϕ(a)} and →a = {(a, b) ∈ N2k : (N, +) |= ϕa (a, b)}. Let
presAutp denote the set of all such presentations. Automatic presentations for
presAutp could be given (cf. [7]).
For sets C ⊆ presAutp (which, as before, need not be isomorphism-closed),
we define a new semantic condition, which is essentially an adaption of (C1’)
to the class of Presburger-definable systems:(C3) there exists an algorithm AC which, given an input presentation
ϑ = hϕ; {ϕa }a∈ACT i ∈ C of the system Λ(ϑ) = hS; {→a }a∈ACT i
and a subset ACT′ ⊆ ACT, computes an existential Presburger
formula R+ (x, y) which defines the transitive closure relation
+S.
a∈ACT′ →a
We denote by tAC the running time of AC in (C3). In addition, we require thatthe class C satisfy the following monotonicity condition: for every S ∈ C every

10

Anthony Widjaja To and Leonid Libkina, b ∈ Nk satisfying a  b (i.e. inequality holds component-wise), if a →a a + δ
for some δ ∈ Zk and a ∈ ACT, then b →a b + δ. This is a strong condition, but
is still satisfied by any subclass of Petri nets.
Theorem 8. Fix any monotone C ⊆ presAutp satisfying (C3). Given ϑ ∈ C,
v0 ∈ Nk represented in binary, and an LTL(Fs , Gs ) or LTLdet formula ψ, checking whether (Λ(ϑ), v0 ) 6|= ψ can be done in nondeterministic time polynomial inkϑk, kv0 k, tAC (kϑk) and kϕk

4

Applications

In this section we apply our metatheorems from the previous section to obtain
decidability and complexity results for LTL, LTL(Fs , Gs ), and LTLdet model
checking over specific classes of infinite systems. In some cases, we re-derive
known results with asymptotically the same complexity bounds; in other cases
we obtain new results. Our results are summarized in Table. 1.
Pushdown systems (PDS). A pushdown system [9] is a tuple P =(ACT, Γ, Q, ∆) where Γ is a stack alphabet, Q a set of states, and ∆ is a finite
subset of Q×Γ ×ACT×Q×Γ ∗. Let ∆a be the set of tuples (called “rules”) in ∆ ofthe form (q, σ, a, q ′ , w). Let Λ(P) be the transition system hQ × Γ ∗ ; {→a }a∈ACT i,
where →a := {((q, wσ), (q ′ , ww′ )) : (q, σ, a, q ′ , w′ ) ∈ ∆a }. It is straightforward(and in poly-time) to give a word-automatic presentation of P (cf. [34]), andshow that the class PDS of such presentations satisfy (C2). Furthermore, it is
known [10, 34] that PDS satisfies (C1) with polynomial running time.
Combined with our results in the previous section, it follows that model
checking LTL, LTL(Fs , Gs ), and LTLdet are respectively in EXPTIME, coNP,
and PTIME. It also follows that all these problems are in PTIME when fixing theformula. It was known (cf. [9]) that the complexity of model checking LTL over
pushdown systems is EXPTIME-complete, and is PTIME for a fixed formula.
On the other hand, the results for LTL(Fs , Gs ) and LTLdet are new (in the caseof LTL(Fs , Gs ) coNP-hardness can be derived from [32]).
Prefix-recognizable systems (Pref-RS). A prefix-recognizable system (withstates) P is a tuple hACT, Γ, Q, ∆) where ACT, Γ , and Q are defined as inpushdown systems, whereas ∆ is a set of rules of the form ((q, U, V ), a, (q ′ , V ′ )),where q, q ′ ∈ Q; a ∈ ACT; and U ,V , and V ′ are regular languages over Γ
given by NWAs. Let Λ(P) be the transition system S = hQ × Γ ∗ ; {→a }a∈ACT i,
where →a is the set of tuples ((q, uv), (q ′ , uv ′ )) ∈ S × S such that, for some((q, U, V ), a, (q ′ , V ′ )) ∈ ∆a , we have u ∈ U , v ∈ V , and v ′ ∈ V ′ . It is straightforward (and in poly-time) to give a word-automatic presentation for P.
Using Theorem 2, we can also rederive the known EXPTIME upper bound[22] for LTL model checking over prefix-recognizable systems (details are in
the appendix). Furthermore, EXPTIME-hardness for model checking a fixedAlgorithmic metatheorems for LTL over infinite systems

11

LTLdet and LTL(Fs , Gs ) formula is obtained by reducing from the unreachability problem for prefix-recognizable systems, which has recently been proven to
be EXPTIME-complete [18].
Concurrent pushdown systems (CPDS). A concurrent pushdown system (cf. [30]) is a tuple P = (ACT, Γ, Q, ∆0 , . . . , ∆N ), where each Pi =(ACT, Γ, Q, ∆i ) is a pushdown system. Suppose that Λ(Pi ) = hQ × Γ ∗ ;{→i,a }a∈Γ i. Then the transition system Λ(P) generated by P is hQ × (Γ ∗ )N ;SN{→a }a∈Γ i, where →a := i=0 →i,a . Although concurrent pushdown systems are
well-known to be Turing-powerful (so checking safety and liveness is undecidable), [23, 30] have shown that reachability is NP-complete if we consider runsof P with a bounded number k of “context-switches” (k part of the input). Intuitively, a context of P is an uninterrupted sequence of actions performed byexactly one “thread” Pi . A context-switch occurs when P interrupts the execution of a thread Pi and resumes by executing a (possibly different) thread Pj .
The context-bounded reachability for P is simply the problem of reachability
restricted to executions of P with exactly k context-switches for any given inputk. One could similarly define the context-bounded LTL model checking problem
for concurrent pushdown systems by restricting the executions of P to thosewith exactly k context-switches for any given k.
Using the results of [23, 30] and our metatheorems, we can show that contextbounded model checking LTL, LTL(Fs , Gs ), and LTLdet over concurrent pushdown systems are respectively EXPTIME-complete, coNP-complete, and coNPcomplete. If the formula is fixed, they are all coNP-complete.
Discrete timed counter systems (RCM and d-RCM). Although verifying safety and liveness for general counter machines is undecidable, it is known
that these problems are decidable (cf. [14, 21]) when all the counters but one arereversal-bounded (only executions with a fixed number of reversals are considered). We denote by RCM the class of such machines. The LTL model checking
problem for RCM is also known to be decidable [14], but no complexity analysis was given for their algorithm. Furthermore, it was left as an open question
whether the same result holds for such machines extended with discrete clocks(in the sense of [3]), for which reachability is known to be decidable [13]. We
write d-RCM for the class of such machines.
We answer this open question positively and give upper bounds for the caseswith and without discrete clocks. Using our metatheorems in combination witha slightly refined version of the algorithms for computing binary reachability
relations in [13, 21], we can give an algorithm for model checking LTL (resp.
LTLdet and LTL(Fs , Gs )) over RCM that runs in time exponential in the size ofthe machine and double exponential (resp. exponential) in the size of the LTL(resp. LTLdet and LTL(Fs , Gs )) formula. Details of the construction and theanalysis are in the appendix.
For d-RCM, we have exactly the same upper bound complexity except thatthe algorithms run double exponential in the number of clocks.

12

Anthony Widjaja To and Leonid Libkin

Communication-free Petri nets (BPP). Communication-free nets (a.k.a.
BPPs) [16, 28] are Petri nets where each transition has exactly one incomingarc (and, hence, “communication-free”). The LTL model checking over BPPs isknown to be EXPSPACE-complete when only infinite traces are considered (cf.
[28]). When finite traces are also considered, the problem is still decidable but
no primitive recursive upper bound is known [28], since reachability for Petrinets could be reduced to this problem.
In contrast, we could show that LTLdet and LTL(Fs , Gs ) model checking
for BPPs is coNP-complete even when finite traces are considered. In fact, it is
known that the transitive closure relations for BPPs are semi-linear [16]. Furthermore, one can then adapt the proof of [36, Theorem 4] to show that there
exists a poly-time algorithm computing an existential Presburger formula defining the transitive closure relation for a given BPP. Since any subclass of Petrinets is monotone, Theorem 8 (which also holds when finite traces are considered)
implies that LTL(Fs , Gs ) and LTLdet model checking over BPPs are in coNP.
Furthermore, a matching lower bound could be easily given for a fixed formulain LTL(Fs , Gs ) and LTLdet by reducing from the non-reachability problem for
BPPs, which is coNP-complete [16].
Weakly extended PA processes (wPA). PA (cf. [26, 28, 31]) is a well-known
process algebra allowing sequential and parallel compositions, but no communication. It is a common generalization of BPP (with unary representation for
numbers) and the class of pushdown systems with one state (a.k.a. BPA). It is
known (cf. [28, 31]) that LTL model checking over PA is undecidable. It is also
known that decidability could be retained when restricting to LTL(Fs , Gs ) and
LTLdet [31]. However, no upper bound to these problems are known.
We can use Theorem 5 and Theorem 7 in combination with the encoding of
PA and their binary reachability relations as tree-automatic systems (cf. [26, 34])
to give an exponential time upper bound for these problems. They are coNPhard, which can be shown by a reduction from non-reachability problem for BPP[16]. The upper bound also holds when we consider weakly extended PA (wPA)[31], which are simply PA extended with weak finite control (i.e. 1-weak NBWA).
Weakly extended ground-tree rewrite systems (wGTRS). A ground tree
rewrite system (GTRS) (cf. [25, 34]) over Σ-labeled trees is a finite set ∆ of“rules” of the form (t, a, t′ ) where t, t′ ∈ Tree(Σ) and a ∈ ACT. For a tree T anda node u in it, let Tu be the subtree of T rooted at u. For a given t ∈ Tree(Σ),
we write T [t/u] for the tree obtained from T by replacing the subtree Tu by t.
The GTRS ∆ generates the transition system Λ(∆) = hTree(Σ); {→a }a∈ACT i
where T →a T ′ iff there exists a node u in T and a rule (t, a, t′ ) ∈ ∆ such that
Tu = t and T ′ = T [t′ /u]. One could easily conclude that LTL model checking
over GTRS is undecidable, using results of [25, 31].
On the other hand, our results imply that decidability is retained when we
restrict to LTL(Fs , Gs ) or LTLdet . This follows from the fact that (C1’) is satisfied by the class of automatic presentations of GTRSs (cf. [12, 34]). Therefore, weAlgorithmic metatheorems for LTL over infinite systems

13

obtain exponential-time algorithms for model checking LTLdet and LTL(Fs , Gs )over GTRS, whose complexity becomes polynomial when the formula is fixed.
We could also show that these problems are coNP-hard for non-fixed formulas.
One can also extend these results to GTRSs with weak finite control, as we
did for PA-processes. Details are in the appendix.

LTL
Comb.
Data
EXP
in P
EXP
EXP
EXP
coNP
×
×

LTL(Fs , Gs )LTLdet
Comb.
Data
Comb.
Data
PDS
coNP
in P
in P
in P
Pref-RS
EXP
EXP
EXP
EXP
CPDS
coNP coNP
coNP coNP
BPP
coNP coNP
coNP coNP
in EXP in EXP in EXP in EXP(w)PA× (ud)× (ud)
coNP-h coNP-h coNP-h coNP-h
in EXP
in EXP
GTRS
× (ud)× (ud)in P
in P
coNP-hcoNP-hin EXP in EXP in EXP in EXP
wGTRS
× (ud)× (ud)
coNP-h coNP-h coNP-h coNP-h
RCM
in 2-EXP in EXP in EXP in EXP in EXP in EXP
d-RCM
in 2-EXP
Table 1. A summary of combined and data complexity that we obtain. Here, × (resp.
ud) means that the result cannot be obtained using our metatheorems (resp. undecidable). Whenever written in bold, the results are new. Also, coNP-h means coNP-hard.

5

How hard are these problems in general?

Relevant to condition (C1) is the problem of checking whether the transitive
closure relation of a given automatic presentation is regular, and the problem ofchecking whether a given transducer R′ represents the transitive closure relationof another one R (over the same domain). We shall point out the degrees ofundecidability of such problems in the arithmetic hierarchy. We shall then pointout the degrees of undecidability of the model checking problems in the generalcase (i.e. over all word/tree automatic presentations), and compare this withthe length-preserving case. We start with the problems related to “computing”
transitive closure relations.
Theorem 9. – Given two nondeterministic word transducers R and R′ ,checking whether R′ is the transitive closure of R is Π20 -complete.
– Given a nondeterministic word transducers R, checking whether its transitive
closure is regular is in Σ30 and Π20 -hard.
We now address the degrees of undecidability for checking recurrent reachability and model checking LTL, LTL(Fs , Gs ), and LTLdet over automatic transition systems. Unlike the problem of reachability which can be shown to beΣ10 -complete (cf. [7, 29]), checking liveness is highly undecidable:

14

Anthony Widjaja To and Leonid Libkin

Theorem 10. Recurrent reachability for both word and tree automatic transition systems is Σ11 -complete, and model-checking LTL, LTL(Fs , Gs ), and LTLdet
for them are all Π11 -complete.
In fact, Theorem 10 could be shown to also hold when the general class of rationaltransducers is used (instead of synchronized rational).
Finally, many examples in the “regular model checking” literature (cf. [2])deal with the subcase of length-preserving synchronized rational transducers(i.e., w →a w′ would imply |w| = |w′ |). In this case, the LTL (resp. recurrent
reachability) model checking problem is usually defined with respect to a regular
set Init of initial states with either “existential” (resp. “universal”) semantics inthe following sense: there exists w ∈ Init such that (resp. all w ∈ Init satisfies)(Λ(ϑ), w) |= ϕ. [Note: when Init is finite, the model checking problems become
decidable since then the set of reachable states from Init is finite.] In contrast to
Theorem 10, we have the following proposition.
Proposition 11. For automatic transition systems with length-preserving
transducers, global recurrent reachability and LTL model checking are all– Σ10 -complete (when existential semantics is considered);– Π10 -complete (when universal semantics is considered).
This result confirms the intuition that checking liveness is much easier when
considering length-preserving transducers.

References
1. P. A. Abdulla, and B. Jonsson. Verifying programs with unreliable channels. Inf.
Comput., 127(2):91–101, 1996.
2. P. A. Abdulla, B. Jonsson, M. Nilsson, and M. Saksena. A survey of regular model
checking. In CONCUR’04, pages 35–48.
3. R. Alur and D. Dill. A theory of timed automata. TCS, 126 (1994), 183–235.
4. C. Baier, N. Bertrand, and Ph. Schnoebelen. On Computing Fixpoints in WellStructured Regular Model Checking, with Applications to Lossy Channel Systems.
In LPAR’06, pages 347–361.
5. V. Barany. Automatic Presentations of Infinite Structures. PhD Thesis, RWTH
Aachen. 2007.
6. S. Bardin, A. Finkel, J. Leroux, L. Petrucci. FAST: acceleration from theory topractice. STTT 10(5): 401–424 (2008)
7. A. Blumensath and E. Grädel. Finite presentations of infinite structures: automata
and interpretations. Theory Comput. Syst. 37(6): 641–674 (2004)
8. A. Bouajjani, A. Legay, and P. Wolper. A Framework to Handle Linear Temporal
Properties in (ω)Regular Model Checking CoRR abs/0901.4080: (2009)
9. O. Burkart, D. Caucal, F. Moller and B. Steffen. Verification on infinite structures.
In Handbook of Process Algebra, Elsevier, 1999.
10. D. Caucal. On the regular structure of prefix rewriting. TCS, 106 (1992), 61–86.
11. H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. In CAV’98, pages 268–279.

Algorithmic metatheorems for LTL over infinite systems

15

12. H. Comon et al. Tree Automata: Techniques and Applications. Available on:
http://www.grappa.univ-lille3.fr/tata, 2007.
13. Z. Dang, O. Ibarra, T. Bultan, R. Kemmerer, J. Su. Binary reachability analysis
of discrete pushdown timed automata. In CAV 2000, pages 69–84.
14. Z. Dang, O. Ibarra, P.S. Pietro. Liveness verification of reversal-bounded multicounter machines with a free counter. In FSTTCS’01, pages 132–143.
15. C. Elgot and J. Mezei. On relations defined by generalized finite automata. IBM
J. Res. Develop. 9 (1965), 47–68.
16. J. Esparza. Petri Nets, Commutative Context-Free Grammars, and Basic Parallel
Processes. Fundam. Inform. 31(1): 13-25 (1997)
17. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere!
Theor. Comput. Sci. 256(1-2):63–92 (2001)
18. S. Göller. Reachability on prefix-recognizable graphs. Inf. Process. Lett. 108(2):71-74 (2008)
19. M. Grohe. Logic, graphs, and algorithms. In Logic and Automata - History andPerspectives, pages 357–422, Amsterdam University Press, 2007.
20. M. Hague and C.-H.L. Ong. Symbolic Backwards-Reachability Analysis for HigherOrder Pushdown Systems. LMCS 4(4): (2008)
21. O. Ibarra, J. Su, Z. Dang, T. Bultan, R. Kemmerer. Counter machines and verification problems. Theor. Comput. Sci. 289 (2002), 165–189.
22. O. Kupferman, N. Piterman, M. Vardi. Model checking linear properties of prefixrecognizable systems. In CAV 2002, pages 371–385.
23. A. Lal, T. Touili, N. Kidd and T. Reps. Interprocedural Analysis of Concurrent
Programs Under a Context Bound. In TACAS’08, pages 282–298.
24. J. Leroux and G. Sutre. Flat Counter Automata Almost Everywhere! In ATVA
’05, pages 489–503.
25. C. Löding. Infinite Graphs Generated by Tree Rewriting, PhD thesis, RWTH
Aachen, 2003.
26. D. Lugiez and P. Schnoebelen. Decidable first-order transition logics for PAprocesses. Inf. Comput., 203(1):75–113, 2005.
27. M. Maidl. The Common Fragment of CTL and LTL. In FOCS’00, pages 643–652.
28. R. Mayr. Decidability and Complexity of Model Checking Problems for InfiniteState Systems. PhD thesis, TU-Munich, 1998.
29. C. Morvan. On rational graphs. In FOSSACS’00, pages 252–266.
30. S. Qadeer and J. Rehof. Context-Bounded Model Checking of Concurrent Software.
In TACAS’05, pages 242–254.
31. V. Rehak. On Extensions of Process Rewrite Systems, PhD thesis, Masaryk University, 2007.
32. A. P. Sistla and E. M. Clarke. The Complexity of Propositional Linear Temporal
Logics. J. ACM 32(3): 733-749 (1985)
33. W. Thomas. Constructing infinite graphs with a decidable MSO-theory. In MFCS,
pages 113–124, 2003.
34. A. W. To and L. Libkin. Recurrent reachability analysis in regular model checking.
In LPAR’08, pages 198–213.
35. M. Y. Vardi, P. Wolper. Automata-theoretic techniques for modal logics of programs. JCSS 32(2): 183–221 (1986).
36. K. N. Verma, H. Seidl, T. Schwentick. On the complexity of equational Hornclauses. In CADE’05, pages 337–352.