Model checking FO(R) over one-counter
processes and beyond
Anthony Widjaja To
LFCS, School of Informatics, University of Edinburgh
anthony.w.to@ed.ac.uk

Abstract. One-counter processes are pushdown processes over a singleton stack alphabet (plus a stack-bottom symbol). We study the problems of model checking asynchronous products of one-counter processes
against 1) first-order logic FO(R) with reachability predicate, 2) the finite variable fragments FOk (R) (k ≥ 2) of FO(R), 3) EF-logic which
is a fragment of FO2 (R), and 4) all these logics extended with simple
component-wise synchronizing predicates. We give a rather complete picture of their combined, expression, and data complexity. To this end, weshow that these problems are poly-time reducible to two syntactic restrictions of Presburger Arithmetic, which are equi-expressive with first-ordermodulo counting theory of (N, <), for which we give optimal quantifier
elimination procedures. In particular, these problems are all shown to be
in PSPACE, which is in sharp contrast to the closely related problem ofmodel checking FO(R) over pushdown processes (with one stack) which
has nonelementary complexity. Finally, we apply our proof method togive a fixed automatic (and so rational) graph whose modal logic theory
has nonelementary complexity, solving a recently posed open question.

1

Introduction

Pushdown automata (PDA) are a natural model for sequential programs withrecursive calls and their model checking problems have been studied extensively.
It is well-known that, over PDA, the problems of model checking first-orderlogic with reachability predicate FO(R) and monadic second-order logic MSO
are decidable in nonelementary recursive time [20]. In fact, PDA (even with
one control state) can easily generate natural numbers (N, +1) with a successor
relation (a.k.a. S1S) and the infinite binary tree with two successor relations(a.k.a. S2S). Since the FO(R) theory of S2S and the MSO theory of S1S havenonelementary complexity [4, 24], the same lower bound can be deduced for PDA.
In contrast, when considering modal and temporal logics — such as EF-logic,
LTL, CTL, and µ-calculus — the complexity of model checking PDA is at most
EXPTIME [3, 5, 27, 28].
One-counter processes (OCPs) are PDA over a singleton stack alphabet (plusa non-removable stack-bottom symbol). The problems of model checking basic
modal logic, EF-logic, and µ-calculus over one-counter processes have been studied, and their complexity are lower than the corresponding problems for general

2

Anthony Widjaja To

PDA [8, 10, 11, 23]. On the other hand, since OCPs can easily generate S1S, it
follows from [24] that model checking MSO over OCPs is nonelementary. The
complexity of model checking FO(R) over OCPs is, however, unknown. Unlike
the case of general PDA, it is easy to show that OCPs cannot generate a graphisomorphic to S2S. Furthermore, the FO theory of S1S with linear order is only
PSPACE-complete [7, 24].
PDA are well-known to be incapable of modeling concurrent programs. One
common way to obtain concurrent behavior from pushdown processes is to consider (finite) products of graphs generated by PDA. An asynchronous productof k PDA P1 , . . . , Pk can be construed as a concurrent system with processes
P1 , . . . , Pk , each behaving independently (i.e. the processes do not interact).
Therefore, reachability for an asychronous product of PDA can trivially be reduced to the reachability problems for each of its components. Note that taking
synchronized products — the most general notion of products — of PDA (resp.
OCPs) easily yield a model that is as powerful as Turing machines (resp. Minsky
counter machines). There are several reasons for studying model checking problems over simple models of concurrent programs such as asynchronous productsof PDA and OCPs. First, Wöhrle and Thomas [29] have recently shown that,when combined with logics such as FO(R) and EF-logic, asynchronous products
are powerful enough for modeling a finite amount of synchronization (synchronization can be embedded in the formulas). Second, asynchronous products of
PDA and OCPs are some of the most basic nontrivial concurrent models thatare subsumed by more complex models such as ground tree rewrite systems [16],PAD [18], automatic graphs [2], and rational graphs [19]. Some open problems
in the more general settings (such as the complexity of model checking EF-logic[18, 26]) seem difficult already in the restricted settings.
In this paper, we consider model checking problems of OCPs, as well as asynchronous products of OCPs (ΠOCPs), with respect to specifications in 1) FO(R),2) the k-variable fragments FOk (R) (k ≥ 2) of FO(R), and 3) EF-logic which is a
fragment of FO2 (R). We also study these logics extended with simple componentwise synchronizing unary predicates testing whether component i and j are thesame elements, which we denote by FOS (R), FOkS (R), and EFS -logic. We givea rather complete picture of their combined complexity (i.e. inputs consist of
systems and specifications), expression complexity (i.e. inputs consist only of
specifications with a fixed system), and data complexity (i.e. inputs consist onlyof systems with a fixed specification).

FO(R)FO2 (R)
EF-logic
FO4 (R)NP
Combined PSPACE PSPACE in P & PNP[log] -hard [8]Expression PSPACE in P
in P [8]DataPHPH in PNP & PNP[log] -hard [8]Table 1. Results for OCPs.

Model checking FO(R) over one-counter processes and beyond

3

FO(R)
FO4 (R) FO2 (R)EF-logic
EFS -logic
FOS (R)
Combined PSPACE PSPACEPSPACEPSPACE
Expression PSPACE in P
in P
PSPACE
Data
PH
PH in PNP & PNP[log] -hard
PH
Table 2. Results for ΠOCPs.

Our results are summarized in Table 1 and Table 2 together with the recent
result from [8]. In particular, all our results are within PSPACE, in contrast to
PDA whose expression complexity for FO(R) is nonelementary [4]. Our upperbounds are shown by first introducing two syntactic restrictions L and L′ of
Presburger Arithmetic, for which we give optimal quantifier elimination procedures, and showing that the ΠOCPs model checking problems are poly-time
reducible to either L or L′ . Note that, to obtain a sharp upper bound, we cannot consider only OCPs (without products) and apply Feferman-Vaught typeof composition methods (e.g. see [17, 22, 29]) as the resulting algorithm will run
in time that is nonelementary in the formula size. Concerning our lower boundresults, in contrast to the result in [8] that model checking EF-logic is in PNP ,data complexity of FO2 (R) over OCPs is already hard for every level of PH.
On the other hand, the expression complexity of FO2 (R) over ΠOCPs is in P.
This generalizes one of the key results in [8] that the expression complexity ofEF-logic over OCPs (without products) is in P. However, for each k > 3, we canshow that the expression complexity of FOk (R) is PSPACE-complete already for
OCPs. Also, notice that the combined complexity of EF-logic becomes PSPACE,
which holds already for products of two OCPs. Finally, notice that adding simple
synchronization relations to EF-logic causes the expression and data complexity
to increase significantly. In fact, we shall use its proof method to give a fixed
automatic (and so rational) graph whose modal logic theory has nonelementarycomplexity, answering a recently posed question in [1, 26].
The paper is organized as follows. We fix some necessary notations and definitions in Section 2. In Section 3 we define two syntactic restrictions L and L′ of
Presburger Arithmetic and prove that model checking problems for OCPs andΠOCPs are poly-time reducible checking formulas in these restricted logics. In
Section 4 we give optimal quantifier elimination procedures for L and L′ anddeduce optimal upper bounds for all problems in Table 1 and Table 2. We prove
our lower bounds results for OCPs and ΠOCPs in Section 5. In Section 6 wegive a fixed automatic graph whose modal logic has nonelementary complexity.
Finally, we conclude in Section 7 with future work. Due to space constraints,
most proofs have been relegated to the full version.

2

Preliminary

General Notations Let Z denote the set of integers. Let N = Z≥0 . For i, j ∈ N,
we use [i, j] to denote {i, i + 1, . . . , j}. As usual, the notations (i, j), (i, j], and4Anthony Widjaja To[i, j) denote the subsets of [i, j] with the appropriate endpoints omitted. We
use a + bN to mean the arithmetic progression {a + bk : k ∈ N}. Given n setsn
S1 , . . . , Sn , their product Πi=1
Si is the set {(s1 , . . . , sn ) : ∀i ∈ [1, n](si ∈ Si )}.
As usual, for a set S, we use S ∗ to denote the set of all finite strings over S. In
the sequel, we use pi to denote the ith prime number, e.g., p1 = 2.
Computational Complexity We assume familiarity with complexity classes
L, P, Σkp , PH, NP, PSPACE and EXPTIME (see [12]). The class PNP (resp. PNP[log] )consists of problems solvable by deterministic poly-time Turing machines withpolynomially (resp. logarithmically) many calls to an NP oracle [13]. As usual,for each n ∈ Z>0 , we use n-EXPTIME to denote the class of problems solvable inn-fold exponential time. A problem is said to be elementary if it is in n-EXPTIME
for some n ∈ Z>0 ; otherwise, it is nonelementary. We assume familiarity withthe alternating Turing machines (ATMs) [12]. Recall that the class of problems
solvable by logspace (resp. poly-time) ATMs coincides with P (resp. PSPACE).
An ATM with not-states (i.e. states that invert the outcome of the run) can be
simulated by one without them without any extra space or time [12].
Graphs Let Σ be a finite set of actions. A Σ-labeled graph is a tuple G =(V, {Ea }a∈Σ ), where V is a set of vertices of G, and each Ea ⊆ V × V is abinary edge relation (a.k.a. transition relation) over V . Whenever Σ is clear
from the context, we shall omit mention of Σ. We also denote Ea by →a , and
′
′
′
write
S v →a v instead of (v, v ∗) ∈→a . For each Σ ⊆ Σ, the transitive closure ofa∈Σ ′ →a is denoted by →Σ ′ . We also write → for →Σ .
Asynchronous products Let Σ1 , . . . , Σr be r pairwise disjoint sets of actions.
Let Σ be their union. For each i ∈ [1, r], let Gi = (Vi , {Ea }a∈Σi ) be a Σi rlabeled graph. An asynchronous product of G1 , . . . , Gr is the graph Πi=1
Gi :=r(V, {E a }a∈Σ ), where V := Πi=1 Vi and, whenever a ∈ Σi , u = (u1 , . . . , ur ),and v = (v1 , . . . , vr ), we have (u, v) ∈ E a iff (ui , vi ) ∈ Ea and uj = vj for
all j 6= i. Intuitively, the product is “asynchronous” as each edge relation inrr
Πi=1
Gi changes at most one component in each vertex of Πi=1
Gi , i.e., causing
no interaction between different components. See [22, 29] for more details.
Other logical structures We define S1S< to be the structure (N, <), i.e.,natural numbers with a (binary) linear order relation <. The structure (N, +)consists of natural numbers with a ternary relation + interpreted as additions
over N. See [12, 25] for more details.
One-counter processes A one-counter process (OCP) over an action alphabetΣ is a tuple O = (Q, δ + , δ 0 ), where Q is a finite set of control states, δ + ⊆ Q×Σ×
Q × {−1, 0, 1} is a finite set of non-zero transitions, and δ 0 ⊆ Q × Σ × Q × {0, 1}
is a finite set of zero transitions. Transitions of the form (q, a, q ′ , −1), (q, a, q ′ , 0),and (q, a, q ′ , 1) are, respectively, called pop transitions, internal transitions, andpush transitions. The size |O| of O is defined as |Q| + |δ 0 | + |δ + |. The OCP O
generates the graph G(O) = (Q × N, {Ea }a∈Σ ), where ((q, n), (q ′ , n + k)) ∈ Ea
iff either n = 0 and (q, a, q ′ , k) ∈ δ 0 , or n > 0 and (q, a, q ′ , k) ∈ δ + .

Model checking FO(R) over one-counter processes and beyond

5

An asynchronous product O of r OCPs is simply a tuple of r OCPs O1 , . . . , Orover pairwise disjoint action alphabets Σ1 , . . . , Σr , whose control states need not
be parwise disjoint. The product O has action labels Σ := Σ1 ∪ . . . ∪ Σr . Then,r
the graph G(O) generated by O is defined to be the Σ-labeled graph Πi=1
G(Oi ).
The system O also defines another graph GS (O), which is simply G(O) expandedwith the “synchronizing” edge relations {=i,j }1≤i6=j≤r that are defined as=i,j := {(c, c) : ci = cj },where c = (c1 , . . . , cr ). In other words, the relation =i,j contains all self-loops in
G(O) restricted to tuples, where ith and jth component agree. The graph GS (O)has action labels Σ ∪ {(i, j)}1≤i6=j≤r .
Logics We assume familiarity with first-order logic FO (see [15]). If the freevariables of φ ∈ FO are amongst x1 , . . . , xn , we may write φ(x1 , . . . , xn ) insteadof φ. Given a graph G = (V, {Ea }a∈Σ ) and a tuple v = (v1 , . . . , vn ) ∈ V n , wewrite G |= φ[v] to mean that φ is true in G over the valuation which assigns vi
to xi . The same notations can be easily defined when dealing with (N, +). The
quantifier rank of φ ∈ FO is the maximum quantifier nesting depth in φ.
The k-variable first-order logic FOk is the restriction of FO to formulas using
at most k variables. Over Σ-labeled graphs, the logic FO(R) (resp. FOk (R)) is
the extension of FO (resp. FOk ) with binary relations RΣ ′ (for each Σ ′ ⊆ Σ)interpreted as the transitive closure relation →∗Σ ′ (see [29]). Denote RΣ by R.
In the sequel, we often use →∗Σ ′ to denote RΣ ′ .
Formulas in the basic modal logic ML over Σ-labeled graphs are built fromthe following grammar: φ, ψ ::= ⊤ | ¬ψ | φ ∨ ψ | haiφ (a ∈ Σ). Given a graph
G = (V, {Ea }a∈Σ ) and each φ ∈ ML, define a set [[φ]]G ⊆ V as follows:(1) [[⊤]]G = V ;(2) [[¬φ]]G = V − [[φ]]G(3) [[φ ∨ ψ]]G = [[φ]]G ∪ [[ψ]]G(4) [[haiφ]]G = {u ∈ V : ∃v ∈ V (u →a v and v ∈ [[φ]]G )}As usual, use ⊥, φ ∧ ψ, and [a]φ to denote ¬⊤, ¬(¬φ ∨ ¬ψ), and ¬hai¬φ, respectively. The logic ML(R) is the extension of ML with reachability modalitieshRΣ ′ i (for each Σ ′ ⊆ Σ), where [[hRΣ ′ iφ]]G := {u ∈ V : ∃v ∈ V (u →∗Σ ′ v and v ∈[[φ]]G )}. For the purpose of this paper, the EF-logic is the logic ML(R). [This isa slightly more general logic than the commonly considered EF-logic, which ismore convenient to work with in our cases. However, all our results will hold aswell for the restricted EF-logic.] There is an easy standard translation (see [15])from formulas in ML (resp. ML(R)) to formulas in FO2 (resp. FO2 (R)) with one
free variable. Over ΠOCPs, we shall use FOS (R), FOkS (R), MLS (R), and the
EFS -logic to denote the logics FO(R), FOk (R), ML(R), and the EF-logic withsynchronizing predicates {=i,j }, interpreted over graphs of the form GS (O).
The model checking problems for any of the above logic L over OCPs (resp.
ΠOCPs) can be defined in the obvious way, i.e., with respect to the graph G(O)generated by the input OCP (resp. ΠOCPs). The input formulas are permitted tohave free variables, which are to be interpreted as configurations in G(O), where
numbers are represented in binary. Also, if L is FOS (R), FOkS (R), MLS (R), or
the EFS -logic, the interpretation is over GS (O).

6

Anthony Widjaja To

The first-order modulo counting logic FOMOD extends FO with the modulo
counting quantifiers ∃p,q , for each q ∈ Z>0 and p ∈ [0, q). In this paper, weconsider FOMOD only over (N, <). The semantics of FOMOD is defined over (N, <)as follows: (N, <) |= ∃p,q xφ(x, b) iff the number l := |{a ∈ N : (N, <) |= φ(a, b)}|is either infinite or finite and l ≡ p (mod q). See [21] for more details.
Alternation rank Given an FO formula φ, push all the negations to atomic
propositions level. The alternation rank AL(φ) of φ is then defined as the maximum number of alternations of operators in {∀, ∧} and operators in {∃, ∨} overall paths from the root to the leaves in the parse tree of φ.
Gödel encoding For the purpose of this paper, we define the Gödel function
G : Z>0 → {0, 1}ω mapping positive integers to infinite binary words as follows:
if n = Πi>0 pji i , where ji ∈ N and pi the ith prime, then define G(n) = j1′ j2′ . . .,where ji′ = 0 if ji = 0 and ji′ = 1 if ji > 0.

3

The logics L and L′

We define our first syntactic restriction L of Presburger Arithmetic, to which wewill reduce the model checking of FO(R) over ΠOCPs.
Definition 1. The syntax of the logic L is as follows. Atomic propositions areof the form:– x ∼ y + c, where ∼∈ {≤, ≥, =},– x ∼ c, where ∼∈ {≤, ≥, =},– x ≡ y + c (mod d), where c ∈ [0, d − 1], and– x ≡ c (mod d), where c ∈ [0, d − 1].
Here, x and y can take any variables, while c and d are constant natural numbers, given in binary representations. We then close the logic under boolean combinations, and existential and universal quantifications. The semantics is given
directly from Presburger Arithmetic. The expression x ≡ y + c (mod d) is to beinterpreted as the Presburger formula ∃z( x = y + c + dz ∨ x + dz = y + c ).
Intuitively, the logic L is the fragment of Presburger Arithmetic that permits
only inequality tests, addition with constants, and modulo tests. We now impose some further syntactic restrictions to our logic L, to which model checking
FO2 (R) over ΠOCPs is still poly-time reducible.
Definition 2. Define the logic L′ as follows. The only variables allowed are xi
and yi , where i ∈ Z>0 . The atomic propositions of L′ are given as follows foreach i ∈ Z>0 :– xi ∼ yi + c and yi ∼ xi + c,
– xi ∼ c and yi ∼ c,
– xi ≡ yi + c (mod d) and yi ≡ xi + c (mod d), and– xi ≡ c (mod d) and yi ≡ c (mod d).

Model checking FO(R) over one-counter processes and beyond

7Here, c and d are constant natural numbers given in binary. We then close thelogic under boolean combinations, and existential and universal quantifications.
The logic L′ allows only two variables xi and yi to be related. In fact, if we only
allow x1 and y1 as variables, then L′ coincides with FO2 fragment of L.
We shall briefly discuss the expressive power of L in terms of subsets of
Nk that can be defined in the logics. It can be shown that L coincides with
the FOMOD theory over (N, <). In fact, [21] shows that FOMOD theory over(N, <) admits a quantifier elimination, when the vocabulary is expanded withcongruence tests. Therefore, L subsumes FOMOD over (N, <). To show that L ⊆FOMOD (N, <), observe that expressions of the form x ∼ y + c can easily be
replaced by equivalent FO formulas over (N, <). Also, the atomic formula x ≡Vd−1
y + c (mod d) can be defined as a=0 (y ≡ a (mod d) ↔ x ≡ a + c (mod d)),and congruence tests x ≡ a (mod d) can be defined in FOMOD over (N, <) as∃a,d y(y < x). The expressive power of FOMOD over (N, <) was shown in [21] tobe strictly in between FO over (N, <) and Presburger Arithmetic. For example,
it was shown that Presburger formulas of the form x = 2y is not definable
in FOMOD over (N, <). Finally, we shall emphasize that the proof in [21] ofquantifier elimination for FOMOD over (N, <) expanded with congruence tests isnonconstructive.
The membership problem of the logic L is as follows: given φ(x) ∈ L, wherex = (x1 , . . . , xn ) and a tuple a ∈ Nn in binary, decide whether N |= φ(a). The
membership problem for L′ can be defined similarly. We now state a proposition,
which can be proved easily (but somewhat tedious) using the result in [8, Lemma
4.6].
Proposition 3. There is a poly-time reduction from the problem of model checking FOS (R) (resp. FO2 (R)) over ΠOCPs to the membership problem for L (resp.
L′ ). Furthermore, the alternation rank of the output formula in L (resp. L′ ) is
the same as the alternation rank of the input formula in FOS (R) (resp. FO2 (R))
up to addition by a small constant.

4

Upper bounds

In this section, we shall show that the combined and data complexity of FOS (R)over ΠOCPs are, respectively, in PSPACE and PH. We then show that the expression complexity of FO2 (R) is in P. To deduce a PNP upper bound for data
complexity of EF-logic over ΠOCPs, it suffices to invoke the Feferman-Vaught
type of composition method for EF-logic [22] and use the PNP algorithm formodel checking EF-logic over OCPs from [8]. Observe that these will give theclaimed upper bounds in Table 1 and Table 2.
4.1

Combined and data complexity of FOS (R)Theorem 4. The combined and data complexity FOS (R) over ΠOCPs are in
PSPACE and in PH, respectively.

8

Anthony Widjaja To

By Proposition 3, to deduce this theorem it suffices to prove the following proposition.
Proposition 5. The membership problem of L-formulas is in PSPACE. Moreover, fixing the alternation rank of input formulas, the problem is in PH.
The proof is done via a quantifier elimination technique (e.g. see [12] for an
overview). Loosely speaking, our proof can be thought of as an extension ofEhrenfeucht-Fraı̈ssé games on linear orders (e.g. see [15]) with modulo tests. We
first define an equivalence relation ≡kp,m on tuples of natural numbers.
Definition 6. Given two (k + 1)-tuples a = (a0 , . . . , ak ), b = (b0 , . . . , bk ) of
natural numbers such that a0 = b0 = 0 and two numbers p, m > 0, we writea ≡kp,m b iff for all i, j ∈ [0, k] the following statements hold:
1. |ai − aj | < pm implies |ai − aj | = |bi − bj |,2. |bi − bj | < pm implies |ai − aj | = |bi − bj |,3. |ai − aj | ≥ pm iff |bi − bj | ≥ pm,
4. ai ≡ bi (mod p),
5. ai ≤ aj iff bi ≤ bj .
It is easy to see that, given m′ ≥ m > 0, we have a ≡kp,m′ b implies a ≡kp,m b.
Similarly, if p|p′ , then a ≡kp′ ,m b implies a ≡kp,m b. The following lemma can beused to eliminate a quantifier.
Lemma 7. Given two (k + 1)-tuples a = (a0 , . . . , ak ), b = (b0 , . . . , bk ) of natural
numbers such that a0 = b0 = 0 and two numbers p, m > 0, if a ≡kp,3m b, then for′
all a′ ∈ N, there exists b′ ∈ N such that a, a′ ≡k+1
p,m b, b .
Let us consider only tuples a = (a0 , . . . , ak ) of natural numbers satisfying′
a0 = 0. Given an ≡kp,3m -equivalence class C and an ≡k+1
p,m -equivalence class C ,′we say that C is consistent with C if there exist a tuple a = (a0 , . . . , ak ) of
natural numbers and a number a′ ∈ N such that a0 = 0, a ∈ C, and (a, a′ ) ∈C ′ . The following lemma shows that we need not consider large numbers wheneliminating a quantifier.
Lemma 8. Let a = (a0 , . . . , ak ) be a tuple of natural numbers and C be its≡kp,3m -equivalence class. Then, every ≡k+1
p,m -equivalence class has a representativein the set {(a, a′ ) : 0 ≤ a′ ≤ max(a) + pm + p}.
Define r(0, m) := m and r(n + 1, m) := 3r(n, m), for n ∈ N. By induction,
we have r(n, m) = 3n m. Let us now define the notion of offsets and periods offormulas in L. If φ are atomic formulas of the form x ∼ y + c, x ∼ c, x ≡ y + c(mod d), or x ≡ c (mod d), then offsets of φ are defined to be the integer c. If φ is
not an atomic formula, then its offset is the largest offset of atomic subformulasof φ. If φ are atomic formulas of the form x ∼ y + c or x ∼ c, then its period
is defined to be 1. If φ are atomic formulas of the form x ≡ y + c (mod d) orx ≡ c (mod d), then its period is defined to be d. Otherwise, if φ is not an atomic
formula, its period is defined to be the least common multiple of the periods ofeach of its atomic subformulas. For p, m ∈ Z>0 , define Lp,m to be formulas inL, whose periods divide p and whose offsets are smaller than m.

Model checking FO(R) over one-counter processes and beyond

9Lemma 9. Let p, m ∈ Z>0 . Suppose a = (a0 , . . . , ak ), b = (b0 , . . . , bk ) are tuplesof natural numbers satisfying a0 = b0 = 0 and a ≡kp,r(n,m) b. Then, given aformula φ(x1 , . . . , xk ) in Lp,m of quantifier rank n,(N, +) |= φ(a1 , . . . , ak ) ⇔ (N, +) |= φ(b1 , . . . , bk ).

We are now ready to prove Proposition 5.
Proof (of Proposition 5). We now give a poly-time ATM M which checks whether(N, +) |= φ(a1 , . . . , an ) for given a formula φ(x1 , . . . , xn ) and a n + 1-tuplea = (a0 , . . . , an ), where a0 = 0. First, push all the negations downward to theatomic propositions level, which can be done easily. Suppose that p and m be,respectively, the period and offset of the input formula. Now if φ is an atomic
proposition (i.e. inequality, or modulo tests), it is easy to see that M can checkit in poly-time. If φ is ψ ∨ ψ ′ (resp. ψ ∧ ψ ′ ), then existentially (resp. universally)guess ψ or ψ ′ and check the guessed formula. If φ is of the form ∃xψ(y, x) (resp.
∀xψ(y, x)) and has quantifier rank k, then M existentially (resp. universally)guesses a number an+1 not exceeding max(a)+pr(k, m)+p ≤ max(a)+p3k m+p
and check whether (N, +) |= ψ(a, an+1 ). The upper bound for an+1 is sufficientdue to Lemma 8.
To analyze the running time of M , notice that the maximum number that
M can guess on any of its run on input φ of quantifier rank h and a tuple a ofhnatural numbers (in binary) is max(a) + Σj=0
(pr(j, m) + p) ≤ max(a) + p(h +h1)3 m + p(h + 1), which can be represented using polynomially many bits. [Notethat p and m are represented in binary and so the guessed number is polynomial
in log(p) and log(m).] This implies that membership of L-formulas is in PSPACE.
Finally, notice that the number of alternations used by M corresponds to thealternation rank of φ. Therefore, considering only formulas of fixed alternation
rank, the membership problem for L-formulas is in PH.
⊓⊔
4.2

Expression complexity of FO2 (R)Theorem 10. The expression complexity of FO2 (R) over ΠOCPs is in P.
Define L′p,m to be the set of all formulas in L′ whose periods divide p and whose
offsets do not exceed m. Let L′p,m (n) to be the set of all formulas in L′p,m thatuse only variables in {x1 , . . . , xn } ∪ {y1 , . . . , yn }. For all fixed p, m, n ∈ Z>0 , themembership problem of L′p,m (n) is as follows: given φ(x, y) ∈ L′p,m (n) and twotuples a, b ∈ Nn of numbers in binary representation, decide whether (N, +) |=φ(a, b). By Proposition 3, Theorem 10 follows from the following proposition.
Proposition 11. For fixed p, m, n ∈ Z>0 , the membership problem of L′p,m (n)is in P.
This proposition can also be proved via quantifier elimination. The intuition that
we can obtain a poly-time algorithm is from a two-pebble Ehrenfeucht-Fraı̈ssé

10

Anthony Widjaja To

games over linear orders (see [15]), which can only distinguish small linear orders(i.e. only linear in the quantifier rank of the FO2 (R) formula). The proof is similar
to the case for FO(R), but is much more tedious.

5

Lower bounds

In order to facilitate our lower bound proofs in this section, we shall define
a 2-player game, called the buffer game, which we shall prove to be PSPACEcomplete. First, let LDIV be the set of quantifier-free L-formulas in 3-CNF (i.e.
in CNF and each clause has exactly three literals) with one free variable x, whose
atomic propositions are of the form x ≡ 0 (mod p) where p is a prime number.
The buffer game is played by Player ∃ and Player ∀. An arena of the buffer
game is a tuple (v, k, φ), where v is a finite and strictly increasing sequence of
positive integers, k is the number of integers in v, and φ a formula of LDIV .
The buffer game with arena (v, k, φ), where v = (v1 , . . . , vk ), has k + 1 rounds
and is played as follows. Each round r defines a positive number mr , which
represents the current buffer value. At round 0, Player ∃ chooses a number m0
to be written to the buffer. Suppose that 0 < r ≤ k, and m0 , . . . , mr−1 are
the buffer values chosen from the previous rounds. At even (resp. odd) roundr, Player ∃ (resp. Player ∀) rewrites the buffer by a number mr ≥ mr−1 of hisvr
vr
pj forpj ), i.e., mr = mr−1 + c Πj=1
choosing such that mr ≡ mr−1 (mod Πj=1
some c ∈ N. In particular, by Chinese remainder theorem, this condition implies
that, for each 1 ≤ j ≤ vr , pj |mr iff pj |mr−1 . In other words, each player is notallowed to “overwrite” some divisibility information in the buffer. Player ∃ wins
if (N, +) |= φ(mk ). Otherwise, Player ∀ wins. The problem BUFFER is defined
as follows: given an arena (v, k, φ) of the buffer game, where each number isrepresented in unary, decide whether Player ∃ has a winning strategy. For eachn ∈ N, we define the problem BUFFERn to be the restriction of the problem
BUFFER which takes only an input arena of the form (v, n, φ).
Lemma 12. The problem BUFFER is PSPACE-complete. The problem BUFFERkp
is Σk+1-complete.
Loosely speaking, by applying Gödel encoding one can encode each truth valuation for boolean formulas into a number. Therefore, boolean formulas canbe reduced to statements about divisibility. Furthermore, a block of ∃ (resp.
∀) quantifers in a quantified boolean formula can be reduced into a choice of
number at a single round in the buffer game for Player ∃ (resp. Player ∀).
We now use the buffer game to prove our first lower bound result for the
problem of model checking OCPs.
Proposition 13. Combined complexity of FO2 (R) on OCPs is PSPACE-hard.
For every k ∈ N, there is a fixed formula φk of FO2 (R) with k + c quantifier
alternations, for some small constant c ∈ N, such that checking φk over OCPs
is Σkp -hard.
To prove this theorem, we first state a standard lemma, whose proof can befound in [8, 11] (similar proof techniques have been used earlier in [14]).

Model checking FO(R) over one-counter processes and beyond

11

Lemma 14. Given a LDIV -formula φ, we can compute in polynomial time an
OCP O with a fixed set Γ of action symbols and an initial state qI such that, foreach positive integer m, it is the case that G(O), (qI , m) |= α iff (N, +) |= φ(m),where α is a small fixed EF formula.
The crucial idea in the proof of the above lemma is that both divisibility andindivisibility tests of the form p|x or p6 |x can be reduced to a certain reachability
question for an appropriate OCP O by embedding a cycle of length p in O.
Proof (sketch of Proposition 13). We give a poly-time reduction from BUFFER.
Given an arena A = (v, k, φ), we compute an FO2 (R) sentence φ′ , and a OCP
O = (Q, δ + , δ 0 ) such that Player ∃ has a winning strategy in A iff G(O) |= φ′ .
Let v = (v1 , . . . , vk ). As we shall see, φ′ depends only on k and has quantifier
rank k + c for some small constant c ∈ N, which by Lemma 12 will prove thedesired lower bound for data complexity.
We now run the algorithm given by Lemma 14 on input φ to compute a OCP
O1 = (D, δ1+ , δ10 ) with initial state qI ∈ D. The key now is to build on top of O1
and the fixed formula α (which can be thought of as an FO2 (R) formula) so as
to encode the initial guessing of numbers.
The structure of our output OCP O can be visualized as
B0 → B1 . . . → Bk → O1 .
The number k + 1 of blocks Bi in O corresponds to the number of rounds playedin the buffer game. The initial state is in block B0 . Our output FO2 (R) formula
will have k + 1 leading (alternating) quantifiers so as to ensure that each player
moves in their designated rounds. One variable will be used for storing the last
buffer value from the previous round, while the other is used for storing thebuffer value after the designated player has made his move. We now describe
how to ensure that at each round i (i > 0) the player can only add numbers thatvi
pj : c ∈ N}. Define the function g : Z>0 → Z>0 as
are in the set Hi := {c Πj=1s
g(s) := Πj=1
pj . Note that g grows exponentially in s, which is why we cannot
simply embed a cycle of length g(vi ) inBi , for each i ∈ [1, k]. On the other hand,
S
S
notice that Hi is Z − Li , where Li :=1≤j≤via∈(0,pj ) a + Npj ∪ Z<0 .
In turn, Li can be characterized as the set of weights of paths in a small finite
graph Gi from a vertex s to a vertex t, where the weight of a path is the sumof the weights of its edges (which we shall allow to be only either -1,0, or 1). In
vifact, Gi will have O(Σj=1
pj ) vertices, which is polynomial in vi . For example,
the set (1 + 2N) ∪ (1 + 3N) ∪ (2 + 3N) ∪ Z<0 corresponds to the weights of s →∗ tpaths in the graph in Figure 1.
Furthermore, the graph Gi can be thought of as an OCP. Adding the selfloop transitions (s, loops , s, 0) and (t, loopt , t, 0) on states s and t, the binary
relation {((s, a), (t, a + b)) : b ∈ Hi } can then be expressed in FO2 (R) as ¬(x →∗y) ∧ Eloops (x, x) ∧ Eloopt (y, y). Therefore, we shall embed the modified OCP Gi
into Bi , where t will be the entry state for block Bi+1 of O. [Bk+1 shall beinterpreted as O1 .]12Anthony Widjaja To

1

s

0

1

0

1
1
0 −1

0
0
10

t

−1

Fig. 1. The s →∗ t path-weights in this graph equals (1+2N)∪(1+3N)∪(2+3N)∪Z<0.

Finally, using this idea, it is not difficult to compute the desired FO2 (R)sentence by mimicking the k + 1 rounds of the game by using at most k + calternating quantifiers (using only the variables x and y). The end buffer valuem, which needs to be checked against φ, can be checked against α instead. ⊓⊔We can also apply Lemma 12 to prove the following lower bound.
Proposition 15. The combined complexity of model checking EF-logic over anasynchronous product of two one-counter processes is PSPACE-hard.
Intuitively, instead of simulating each alternation in the buffer game as values
in the two variables x and y, we can simulate them as values in two different
counters. We can make sure that the divisibility information is not “overwritten”
by encoding it as a non-fixed formula.
We saw in the previous section that the expression complexity of FO2 (R) over
ΠOCPs is in P. In contrast, we can show that this is not the case for FO4 (R)even over OCPs (without products).
Proposition 16. The expression complexity of FO4 (R) (without equality relation) over OCPs is PSPACE-hard.
The fixed graph is in fact (N, <). The proof adapts the technique in [9] of succinctly encoding addition arithmetic on large numbers using the successor relations and linear order < with only four variables.
We already saw that the data complexity of EF-logic over ΠOCPs is PNP . In
contrast, we can show the following proposition.
Proposition 17. For each k ∈ N, there is a fixed EFS -logic formula φk suchthat model checking φk over ΠOCPs is Σkp -hard.
Intuitively, by using the synchronization constraints, one can faithfully simulate
two variables x and y in any given FO2 (R) formula as values of two different
counters. This idea can easily be adapted for showing the following proposition
by appealing to Proposition 16.
Proposition 18. The expression complexity of EFS -logic over ΠOCPs is hardfor PSPACE.

Model checking FO(R) over one-counter processes and beyond

6

13

Modal logic over automatic graphs

Automatic graphs [2] are those graphs G = (V, {Ea }a∈Σ ), where V is a regularsubset of Σ ∗ for some finite alphabet Σ, and each edge relation Ea ⊆ Σ ∗ × Σ ∗ isrecognizable by a synchronous transducer over Σ. We briefly recall the definitionof synchronous transducers — see [2] for more details. A synchronous transducer
R over Σ is a finite word-automaton over the product alphabet Σ⊥ × Σ⊥ , whereΣ⊥ := Σ ∪ {⊥} and ⊥ ∈/ Σ. Given v, w ∈ Σ ∗ where v = a1 . . . an and w =b1 . . . bm , define v⊗w to be the word c1 . . . ck over Σ⊥ ×Σ⊥ , where k = max(n, m)and (ai , bi ) if i ≤ min(n, m),ci = (⊥, bi ) if n < i ≤ m,(ai , ⊥) if m < i ≤ n.
The edge relation definable by R consists of each ordered pair (v, w) ∈ Σ ∗ × Σ ∗such that the word v⊗w is accepted by R (in the usual automata sense). Rationalgraphs [19] are similar to automatic graphs, but use a more general notion oftransducers.
The FO (resp. ML) theories of automatic (resp. rational) graphs are known
to be decidable, e.g., see [2, 1]. In fact, the infinite binary tree S2S with a linear
order is automatic [2], which implies that model checking FO over automatic
graphs is nonelementary. Recently, the authors of [26] and [1] asked whether thecomplexity of model checking ML over, respectively, automatic graphs and rational graphs is nonelementary. We shall show that this is the case in the stronger
sense by establishing a fixed automatic graph whose ML theory is nonelementary.
Since automatic graphs are rational [19], the same can be said about rationalgraphs. Our proof uses the proof method for Proposition 17. Due to space limit,
we shall only define a graph T whose modal logic theory we claim to be nonelementary. Its proof can be found in the full version. Furthermore, one can easily
check that the graph T is automatic.
We denote by S2S< := ({0, 1}∗, succ0 , succ1 , ≺) the infinite binary tree witha descendant relation, i.e., succ0 := {(w, w0) : w ∈ {0, 1}∗}, succ1 := {(w, w1) :w ∈ {0, 1}∗}, and ≺ := {(w, wv) : w, v ∈ {0, 1}∗ }. Although the FO theoryof S2S< was proved to be nonelementary in [4], it is not easy to see whether
FOk suffices from the proof. Nevertheless, one can easily show that FO4 suffices
as follows. Using Stockmeyer’s well-known results [24] that equivalence of starfree regular expressions is nonelementary, one can immediately deduce that FO3
theory over all finite linear orders with a unary predicate is nonelementary, since
there is a linear-time translation from star-free regular expressions to equivalent
FO3 formulas (e.g. see [6]). One may then use the linear-time reduction given in[4] from FO theory of binary strings to FO theory of S2S< , which incurs only an
extra variable. So, we have the following proposition.
Proposition 19. The FO4 theory of S2S< is nonelementary.
Now define the graph
T := h{0, 1}∗ × {0, 1}∗ × {0, 1}∗ × {0, 1}∗;
{succi0 }4i=1 , {succi1 }4i=1 , {≺i }4i=1 , {=i,j }1≤i<j≤4 , {Gi }4i=1 i.

14Anthony Widjaja To

where the edge relations are defined as follows:– succi0 := { w, w′ : wi′ = wi 0 and ∀j 6= i(wj = wj′ )}. This relation takes theith component to its left child.
– succi1 := { w, w′ : wi′ = wi 1 and ∀j 6= i(wj = wj′ )}. This relation takes theith component
 to its right child.
– ≺i := { w, w′ : wi ≺ wi′ and ∀j 6= i(wj = wj′ )}. This relation takes the ith
component to its descendant.
– =i,j := { w, w′ : wi = wj and ∀k(wk = wk′ )}. This relation simply loops if
the ith component
equals the jth component.
– Gi := { w, w′ : ∀j 6= i(wj = wj′ )}. This relation takes the ith component toany other word (i.e. global modality).
Proposition 20. The graph T is automatic and its ML theory is nonelementary.
Theorem 21. There exists a fixed automatic (and so rational) graph whose ML
theory is nonelementary.

7

Future work

We conclude now with several future work. We would like to determine theexpression complexity of FO3 (R) over OCPs and ΠOCPs. Our lower bound proof
for FO4 (R) does not hold since FO3 (R) cannot succinctly encode arithmetic oflarge numbers using only successors and linear orders [9]. We would also like to
study the combined complexity of EF-logic over asynchronous products of PDA.
It is known to be PSPACE-hard [27] and decidable (by applying the compositional
method [22]), but no better upper or lower bound is known. [In fact, it seems notclear how to adapt the proof of PSPACE upper bound for PDA to asynchronous
products.] On the other hand, it follows from the proof of Theorem 21 that model
checking EFS -logic over asynchronous products of PDA is nonelementary.
Acknowledgments: The author thanks Shunichi Amano, Stefan Göller, Leonid
Libkin, and anonymous reviewers for their helpful comments. The author is
supported by EPSRC grant E005039 and ORSAS Award.

References
1. W. Bekker and V. Goranko. Symbolic model checking of tense logics on rational
Kripke models. To appear in proceedings of ILC’07.
2. A. Blumensath and E. Grädel. Automatic structures. In LICS ’00, pages 51–62.
3. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR ’97, pages 135–150.
4. K. J. Compton and C. W. Henson. A uniform method for proving lower bounds onthe computational complexity of logical theories. Ann. Pure Appl. Logic, 48(1):1–
79, 1990.

Model checking FO(R) over one-counter processes and beyond

15

5. J. Esparza, A. Kucera, and S. Schwoon. Model checking LTL with regular valuations for pushdown systems. Inf. Comput., 186(2):355–376, 2003.
6. K. Etessami, M. Y. Vardi, and T. Wilke. First-order logic with two variables andunary temporal logic. Inf. Comput., 179(2):279–295, 2002.
7. J. Ferrante and C. W. Rackoff. The Computational Complexity of Logical Theories,
volume 718. Springer-Verlag, 1979.
8. S. Göller, R. Mayr, and A. W. To. On the computational complexity of verifying
one-counter processes. To appear in LICS, 2009.
9. M. Grohe and N. Schweikardt. The succinctness of first-order logic on linear orders.
Logical Methods in Computer Science, 1(1), 2005.
10. P. Jancar and Z. Sawa. A note on emptiness for alternating finite automata witha one-letter alphabet. Inf. Process. Lett., 104(5):164–167, 2007.
11. P. Jančar, A. Kučera, F. Moller, and Z. Sawa. DP lower bounds for equivalencechecking and model-checking of one-counter automata. Inf. Comput., 188(1):1–19,
2004.
12. D. C. Kozen. Theory of Computation. Springer-Verlag, 2006.
13. M. W. Krentel. The complexity of optimization problems. J. Comput. Syst. Sci.,
36(3):490–509, 1988.
14. A. Kučera. Efficient verification algorithms for one-counter processes. In ICALP’00, pages 317–328.
15. L. Libkin. Elements Of Finite Model Theory (Texts in Theoretical Computer Science. An EATCS Series). SpringerVerlag, 2004.
16. C. Löding. Reachability problems on regular ground tree rewriting graphs. Theory
Comput. Syst., 39(2):347–383, 2006.
17. J. A. Makowsky. Algorithmic uses of the Feferman-Vaught Theorem. Ann. Pure
Appl. Logic, 126(1-3):159–213, 2004.
18. R. Mayr. Decidability of model checking with the temporal logic EF. Theor.
Comput. Sci., 256(1-2):31–62, 2001.
19. C. Morvan. On rational graphs. In FOSSACS ’00, pages 252–266, 2000.
20. D. E. Muller and P. E. Schupp. The theory of ends, pushdown automata, andsecond-order logic. Theor. Comput. Sci., 37:51–75, 1985.
21. P. Péladeau. Logically defined subsets of Nk . Theor. Comput. Sci., 93(2):169–183,
1992.
22. A. Rabinovich. On compositionality and its limitations. ACM Trans. Comput.
Logic, 8(1):4, 2007.
23. O. Serre. Parity games played on transition graphs of one-counter processes. In
L. Aceto and A. Ingólfsdóttir, editors, FoSSaCS, volume 3921 of Lecture Notes in
Computer Science, pages 337–351. Springer, 2006.
24. L. J. Stockmeyer. The complexity of decision problems in automata theory andlogic. PhD thesis, Department of Electrical Engineering, MIT, 1974.
25. W. Thomas. Constructing infinite graphs with a decidable MSO-theory. In MFCS
’03, pages 113–124.
26. A. W. To and L. Libkin. Recurrent reachability analysis in regular model checking.
In LPAR ’08, pages 198–213.
27. I. Walukiewicz. Model checking CTL properties of pushdown systems. In FSTTCS’00, pages 127–138.
28. I. Walukiewicz. Pushdown processes: games and model-checking. Inf. Comput.,
164(2):234–263, 2001.
29. S. Wöhrle and W. Thomas. Model checking synchronized products of infinite
transition systems. Logical Methods in Computer Science, 3(4), 2007.