Concurrency Makes Simple Theories Hard
Stefan Göller1 and Anthony Widjaja Lin2
1
2

Fachbereich Informatik, University of Bremen, Germany
Department of Computer Science, Oxford University, United Kingdom

Abstract
A standard way of building concurrent systems is by composing several individual processes by productoperators. We show that even the simplest notion of product operators (i.e. asynchronous products) suffices to increase the complexity of model checking simple logics like Hennessy-Milner (HM) logic andits extension with the reachability operator (EF-logic) from PSPACE to nonelementary. In particular, thisnonelementary jump happens for EF-logic when we consider individual processes represented by pushdown systems (indeed, even with only one control state). Using this result, we prove nonelementary lower
bounds on the size of formula decompositions provided by Feferman-Vaught (de)compositional methodsfor HM and EF logics, which reduce theories of asynchronous products to theories of the components. Finally, we show that the same nonelementary lower bounds also hold when we consider the relativizationof such compositional methods to finite systems.
1998 ACM Subject Classification F.4.1 Mathematical Logic, F.4.2 Grammars and Other Rewriting
Systems
Keywords and phrases Modal Logic, Model Checking, Asynchronous Product, Pushdown Systems,
Feferman-Vaught, Nonelementary lower bounds

1

Introduction

Concurrent systems are systems which consist of multiple processes that are simultaneously executedand possibly interacting with each other. A standard way of designing concurrent systems is tocompose together several individual processes by taking some “product” operators. Various productoperators have been introduced in concurrency theory and verification ranging from synchronizedproducts (the strongest form of products) to asynchronous products (the weakest form of products).
From the point of view of system design, synchronized products are the most suitable form ofcompositional operators. Unfortunately, from the point of view of system verification, they are
known to be too powerful. For example, while reachability is NL-complete for finite transition
systems, it becomes PSPACE-complete when the same problem is considered over synchronizedproducts of finite transition systems (a.k.a. communicating finite-state machines). In the case of
infinite-state systems, we see a more drastic change: while reachability is decidable in polynomial
time for pushdown systems (PDS), the same problem becomes undecidable when considered oversynchronized products of two PDS (note: these subsume Minsky’s counter machines).
In order to circumvent the problem of high complexity and undecidability in verifying concurrent
systems composed from individual processes via synchronized products, various weaker notions of
products were introduced. Apart from asynchronous products which prohibit the processes to communicate, stronger product operators were introduced by restricting the types of synchronization that areallowed among the processes. Several such restrictions include bounded context switches [14], andfinite synchronization [19]. These restricted product operators can serve as good underapproximationsof synchronized products. For example, a recent study of concurrency bugs conducted by the authorsof [11] reveal that many real-world concurrency bugs can be detected within a small number of context
switches. In addition, such restrictions also lead to decidability or lower computational complexity in© Stefan Göller and Anthony W. Lin;
licensed under Creative Commons License NC-ND
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

2Concurrency Makes Simple Theories Hardmodel checking. For example, checking reachability over communicating finite-state machines andcommunicating pushdown systems with bounded context switches are both NP-complete [14].
When we consider logic model checking, the situation is not as simple. Asynchronous products
do not make model checking easier than synchronized products when we use logics like LTL andCTL (and, in fact, even their restrictions to LTL(F,X) and the logic EG). Intuitively, the reason
is that synchronization is easily embedded in such logics. Consequently, reachability of 2-stack
pushdown systems, which is well-known to be undecidable, easily reduces to model checking
any of aforementioned logics over asynchronous products of two PDS. In contrast, the situation
is substantially better when we consider simpler logics like Hennessy-Milner (HM) Logic andits extension with the reachability operator (i.e. EF-logic). In fact, powerful (Feferman-Vaught)
compositional methods (e.g. [12, 15, 19]), which reduce model checking of product structures
to model checking of their components, can be used for obtaining decidability or better uppercomplexity bounds of model checking HM-logic and EF-logic. We now state the most basic form ofsuch compositional methods from [15].
I Theorem 1 ([15]). For each HM/EF formula ϕ over the action labels A = A1 ∪ . . . ∪Ak , for nonempty disjoint sets A1 , . . . , Ak , one can compute k finite sets of HM/EF formulas{ψi1 }i∈I1 , . . . , {ψik }i∈Ik over A1 , . . . , Ak respectively, and a positive boolean formula (i.e. no negations) β with variables {x1i }i∈I1 , . . . , {xki }i∈Ik such that for all transition systems T1 , . . . , Tk withQk
initial states s1 , . . . , sk we have ( i=1 Ti , s̄) |= ϕ if and only if β[µ] is true, where s̄ = (s1 , . . . , sk )and µ assigns the variables of β as follows: µ(xji ) = 1 if and only if (Tj , sj ) |= ψij .
Actually, a stronger version of Theorem 1 was proven in [15] (e.g. with atomic propositions). In thestatement of Theorem 1, the k sets of formulas and the positive boolean formula β are referred toas the decomposition of ϕ. To give some concrete illustrations of the power of this compositional
theorem, Theorem 1 can be used to show that model-checking fixed EF formulas (i.e. the complexity
is only measured the size of the system) is: NL-complete for asynchronous products of finite
systems (c.f. PSPACE-completeness of communicating finite-state systems), PSPACE-complete forasynchronous products of PDS [16], and P-complete for asynchronous products of Basic Process
Algebras (equivalently, one-state PDS).
Despite the aforementioned usefulness of Feferman-Vaught compositional methods, the techniqueyields algorithms with nonelementary complexity in the size of the formula (see [15]), which is notdesirable from both theoretical and practical viewpoints. In fact, it was recently shown that when we
consider stronger logics like first-order logic, where Feferman-Vaught compositional methods arealso available (e.g. see [12]), this nonelementary complexity is unavoidable [6]. It is natural to ask
whether this nonelementary complexity is avoidable when we consider simpler logics like HM-logic
or EF-logic. In fact, this open question has been posed in the literature (e.g. [7, 15]).
This open question actually brings us to a more fundamental open question: how do asynchronous
products affect the complexity of model checking of HM-logic and EF-logic? This open question has
manifested itself in the literature in various concrete forms. As an example, take the result that model
checking EF-logic over pushdown systems is PSPACE-complete [21]. Over asynchronous productsof two pushdown systems, the best algorithm for model checking EF-logic runs in nonelementary
time [16]. In fact, the same nonelementary gap is currently present for asynchronous products of
two BPAs. Failing to answer this open question is also the reason for the existing nonelementarycomplexity gaps for several verification problems for PA-processes [13], which are an extension ofasynchronous products of BPAs with process creations.
Contributions. In this paper, we provide answers to the above open questions. A main contributionof this paper is to show that, for each integer k > 0, there exists an asynchronous product of two BPAs
whose EF-logic theory requires k-fold exponential time to solve. This means that model checking

S. Göller and A. W. Lin

EF-logic over the class of asynchronous products of two BPAs requires nonelementary time, which isin stark contrast to PSPACE-completeness of EF model checking over BPAs [21]. As an upshot of
our result, it follows that model checking EF-logic over PA-processes requires nonelementary time,
which solves the open question posed by R. Mayr [13].
We also show that similar results hold for HM-logic. More precisely, we prove that for each
integer k > 0 there exists an asynchronous product of two prefix-recognizable systems (an extension
of BPAs introduced by Caucal [5] by allowing infinitely many rewrite rules compactly represented byregular languages) whose HM-logic theory requires k-fold exponential time to solve. This means thatmodel checking HM-logic over the class of asynchronous products of two prefix-recognizable systems
requires nonelementary time, which is in stark contrast to PSPACE-completeness of HM-logic model
checking over prefix-recognizable systems (which easily follows1 from the result of [21]).
An important corollary of our two aforementioned results is that there is no elementary algorithm
for computing decompositions of formulas in HM-logic and EF-logic in the sense of Theorem 1.
We go one step further to show that no decompositions of formulas in HM-logic and EF-logicof elementary size even exist in general. In other words, both descriptional and computational
complexity of compositional methods of HM-logic and EF-logic in the sense of Theorem 1 areinherently nonelementary. Incidentally, this also entails the same nonelementary lower bounds forcompositional methods provided in [7] since they generalize Theorem 1.
So far, our nonelementary lower bounds for compositional methods for HM-logic and EF-logic
require the use of infinite-state systems. This still leaves the possibility that Theorem 1 could holdwhen we restrict the transition systems under consideration to be finite-state. Questions of this form
are of particular interests in finite model theory (e.g. see [10]) and in verification of finite-statesystems. We show, however, that the same nonelementary lower bounds relativize to the class ofasynchronous products of finite systems.
Organization. We fix notations and definitions in Section 2. We present nonelementary lower bounds
for the classes of asynchronous products of BPAs and prefix-recognizable systems in Section 3. In
Section 4, we use results from Section 3 to prove nonelementary lower bounds for compositional
methods for HM-logic and EF-logic over all transition systems, as well as over all finite transition
systems. We conclude in Section 5 with future work.

2

Preliminaries

General: By N = {0, 1, . . .} we denote the set of nonnegative integers. For each i, j ∈ N, we define
the interval [i, j] = {i, i + 1, . . . , j}. Let f : N → N be a function. We write f (n) = poly(n) if
there is some polynomial p(n) such that f (n) ≤ p(n) for all n ∈ N. We write f (n) = exp(n) if
there is some polynomial p(n) such that f (n) ≤ 2p(n) for all n ∈ N. We define the standard Tower
function Tower : N × N → N inductively as Tower(0, n) = n and Tower(k, n) = 2Tower(k−1,n) , foreach k > 0 and each n ∈ N.
Automata: A deterministic finite automaton (DFA) is a tuple A = (Q, Σ, q0 , δ, F ), where Q is a
finite set of states, Σ is a finite alphabet, q0 ∈ Q is the initial state, δ : Q × Σ → Q is the transition
function, and F ⊆ Q is the set of final states. By L(A) = {w ∈ Σ∗ | A accepts w} we denote thelanguage of A. The size of A is defined as |A| = |Q|.
Systems: Let us fix a countable set of action labels Act. A transition system is tuple T =a(S, A, {−→| a ∈ A}), where S is a set of states, A ⊆ Act is a finite set of action labels, and wherea−→⊆ S × S is a set of transitions for each a ∈ A. We say T is finite if S is finite. A pointed

1

On the same note, even µ-calculus over prefix-recognizable systems is only EXP-complete [9]34Concurrency Makes Simple Theories Hardatransition system is a pair (T , s), where T is a transition system and s is state of T . We write s −→ tato abbreviate (s, t) ∈−→. We apply similar abbreviations for other binary relations over S. For eachSΓaΓ ⊆ A, we define −→= a∈Γ −→.
aaGiven k ≥ 1 transition systems T1 = (S1 , A1 , {−→1 | a ∈ A1 }), . . . , Tk = (Sk , Ak , {−→k |Qka ∈ Ak }), where the Ai ∩ Aj = ∅ for each i 6= j, we define its asynchronous product i=1 Ti =Qk
Ska
(S, A, {−→| a ∈ A}), where S = i=1 Si , A = i=1 Ai , and where for each a ∈ A we haveaa(s1 , . . . , sk ) −→ (s01 , . . . , s0k ) if and only if si −→i s0i for some i ∈ [1, k] with a ∈ Ai and sj = s0j
for each j ∈ [1, k] \ {i}.
Logic: Formulas of EF-logic over a finite set A ⊆ Act of labels are given by the following grammar,
where Γ ⊆ A:ϕ::=
> | ¬ϕ | ϕ ∧ ϕ | hΓiϕ | hΓ∗ iϕ
We introduce the usual abbreviations ⊥ = ¬>, ϕ1 ∨ ϕ2 = ¬(¬ϕ1 ∧ ¬ϕ2 ), ϕ1 → ϕ2 = ¬ϕ1 ∨ ϕ2 ,ϕ1 ↔ ϕ2 = (ϕ1 → ϕ2 ) ∧ (ϕ2 → ϕ1 ), [Γ]ϕ = ¬hΓi¬ϕ, and [Γ∗ ]ϕ = ¬hΓ∗ i¬ϕ. We also writehΓin (resp. [Γ]n ) as an abbreviation for a sequence of n consecutive hΓi’s (resp. [Γ]’s). By |ϕ|we denote the size of each EF formula |ϕ| defined as usually. Hennessy-Milner logic (HM) is thesyntactic fragment of EF that one obtains by forbidding formulas of the kind hΓ∗ iϕ. Since we allow
formulas of the form hΓ∗ iϕ for subsets Γ of the action labels (instead of only hA∗ i), our version of
EF is slightly more general than the standard definition of EF-logic. However, our results easily carryover to the standard definition of EF-logic.
a
For each transition system T = (S, A, {−→| a ∈ A}) and each EF-formula ϕ (over A) define
the set of states [[ϕ]]T ⊆ S that satisfy ϕ by induction on the structure of ϕ as follows:Γ[[>]]T=S[[hΓiϕ]]T={s ∈ S | ∃t ∈ [[ϕ]]T : s −→ t}[[¬ϕ]]T[[ϕ1 ∧ ϕ2 ]]T==

S \ [[ϕ]]T[[ϕ1 ]]T ∩ [[ϕ2 ]]T[[hΓ∗ iϕ]]T={s ∈ S | ∃t ∈ [[ϕ]]T : s −→ t}Γ ∗We also write (T , s) |= ϕ whenever s ∈ [[ϕ]]T or simply s |= ϕ when T is clear from the context.
Infinite-state models: A pushdown system (PDS) is a tuple P = (Σ, A, ∆), where Σ is a finite setof process constants, A ⊆ Act is a finite set of action labels and ∆ is a finite set of rewrite rulesof the form u 7→a v, where a ∈ A, u ∈ Σ∗ and v ∈ Σ∗ . A basic process algebra (BPA) is PDA
P = (Σ, A, ∆), where for each u 7→a v ∈ ∆ we have |u| = 1. The associated transition system T (P)aais defined as T (P) = (Σ∗ , A, {−→| a ∈ A}), where −→= {(uw, vw) | u 7→a v ∈ ∆, w ∈ Σ∗ } forP
each a ∈ A. The size of a PDS is defined as |P| = |Σ| + |A| + u7→a v∈∆ (|u| + |v|).

3

Hardness of asynchronous productWe start by proving a nonelementary lower bound for the problem of model checking EF on BPA×BPA:
given two BPAs P = (Σ, A, ∆), P 0 = (Σ0 , A0 , ∆0 ) with A ∩ A0 = ∅, a pair of process constants
hX, X 0 i ∈ Σ × Σ0 , and an EF formula ϕ over A ∪ A0 , check whether (T (P) × T (P 0 ), hX, X 0 i) |= ϕ.
I Theorem 2. Model checking EF on BPA×BPA is nonelementary.
We then show that this lower bound implies a nonelementary lower bound for model checking
HM-logic over the class of asynchronous products of two prefix-recognizable systems (a precise
definition is given below).

3.1

Proof of Theorem 2

The structure of the proof of Theorem 2 is as follows. We first show how to encode large counters as
EF formulas evaluated over the class of asynchronous products of two BPAs. Such large counters are

S. Göller and A. W. Lin

enforced by the two stacks in the two BPAs, which alternately “guess” an encoding of a counter and“check” the correctness of the encoding. As we will see later, this encoding of large counters can beused to encode memberships of Tower(k, cn) space-bounded Turing machines for any fixed k > 0.
Large counters: The following encoding of large numbers is from [20, 3]. In the following, thenotations n and ` will range over N. We define the alphabets Ω` = {0` , 1` } and the values val(0` ) = 0
and val(1` ) = 1 for each ` ≥ 0.
A (1, n)-counter is a word from Ωn0 . The value val(c) of some (1, n)-counter c = σ0 · · · σn−1
Pn−1 in
is defined as val(c) =i=0 2 · val(σi ) ∈ [0, 2 − 1]. So the set of values val(c) for (1, n)ncounters c equals [0, 2 − 1] = [0, Tower(1, n) − 1]. An (`, n)-counter with ` > 1 is a wordc = c0 σ0 c1 σ1 . . . cm σm , where m = Tower(` − 1, n) − 1, each ci is an (` − 1, n)-counter withPmval(ci ) = i and σi ∈ Ω`−1 for each i ∈ [0, m]. We define val(c) = i=0 2i · val(σi ). Observe thatval(c) ∈ [0, Tower(`, n) − 1] and the length of each (`, n)-counter is uniquely determined by ` and n.
S`
In the following, we define Ω0` = {00` , 10` } to be a fresh copy of Ω` ; moreover define Σ` = i=0 ΩiS`and analogously Σ0` = i=0 Ω0i .
Definition of the two BPAs: For each integer ` > 0, let us define the following simple BPAs
P` = (Σ` , L` , ∆` ), whereL` = Σ` ∪ Σ` , where Σ` = {σ | σ ∈ Σ` } is a dual copy of Σ` .
∆` = {τ 7→σ στ | σ, τ ∈ Σ` } ∪ {σ 7→σ ε | σ ∈ Σ` }.
The transition system T (P` ) has a fairly regular behavior. The set of states is Σ∗` . Executing anaction σ ∈ Σ` from a state u ∈ (Σ` )∗ allows to remove exactly this leftmost symbol σ from u if ubegins with σ, otherwise σ cannot be executed from u. Dually, from every nonempty state u ∈ (Σ` )+of T (P` ) we can execute every action σ ∈ Σ` yielding the state σu; the only state from which theσ ∈ Σ` are not executable is the empty word ε. We define the BPA P`0 analogously to P` but bypriming every symbol. Formally, P`0 = (Σ0` , L0` , ∆0` ), where
L0` = Σ0` ∪ Σ0` , where Σ0` = {σ 0 | σ 0 ∈ Σ0` } is a dual copy of Σ0` .
∆0` = {τ 0 7→σ0 σ 0 τ 0 | σ 0 , τ 0 ∈ Σ0` } ∪ {σ 0 7→σ0 ε | σ 0 ∈ Σ0` }.
Note that the set of states of T (P` ) × T (P`0 ) is (Σ` )∗ × (Σ0` )∗ . Given a state s = (u, u0 ) ∈(Σ` )∗ × (Σ0` )∗ , we call u the left stack of s and u0 the right stack of s. So we treat the words u and
u0 as stacks with their left-most symbols being the top of the stack. Recall that every (`, n)-counteris in particular a word over Σ`−1 . We extend this notion to words over Σ0`−1 in the usual way. So
each (`, n)-counter will in particular be either a word over Σ`−1 or over Σ0`−1 , depending on whether
we address the left stack or the right stack. Note that if some word over Σk (resp. over Σ0k ) has an(`, n)-counter as a prefix, then the length of this prefix is uniquely determined by ` and n, namely
Tower(` − 1, n). An extended (`, n)-counter is either a string cσ, where either c ∈ Σ∗`−1 is an(`, n)-counter and σ ∈ Ω` , or a string c0 σ 0 , where c0 ∈ (Σ0`−1 )∗ is an (`, n)-counter and σ 0 ∈ Ω0` .
Next, we define some EF formulas (with primed counterparts for the right stack) for each `, n ∈ N:
1. countσ(`,n) for each σ ∈ Ω` such that (T (P` ) × T (P`0 ), (u, u0 )) |= countσ(`,n) if and only if forsome (`, n)-counter c we have cσ is a prefix of u.
00
2. countσ(`,n) for each σ 0 ∈ Ω` such that (T (P` ) × T (P`0 ), (u, u0 )) |= countσ(`,n) if and only if forsome (`, n)-counter c0 we have c0 σ 0 is a prefix of u0 .
3. xcount(`,n) such that (T (P` ) × T (P`0 ), (u, u0 )) |= xcount(`,n) if and only if some extended(`, n)-counter cσ (for σ ∈ Ω` ) is a prefix of u.
4. xcount0(`,n) such that (T (P` ) × T (P`0 ), (u, u0 )) |= xcount0(`,n) if and only if some extended(`, n)-counter c0 σ 0 (for σ 0 ∈ Ω0` ) is a prefix of u0 .
5. first(`,n) (resp. first0(`,n) ) such that (T (P` ) × T (P`0 ), (u, u0 )) |= first(`,n) (resp. (T (P` ) ×
T (P`0 ), (u, u0 )) |= first0(`,n) ) if and only if some extended (`, n)-counter cσ (resp. c0 σ 0 ) withval(c) = 0 (resp. val(c0 ) = 0) is a prefix of u (resp. u0 ).

5

6

Concurrency Makes Simple Theories Hard

6. last(`,n) (resp. last0(`,n) ) such that (T (P` ) × T (P`0 ), (u, u0 )) |= last(`,n) (resp. (T (P` ) ×
T (P`0 ), (u, u0 )) |= last0(`,n) ) if and only if some extended (`, n)-counter cσ (resp. c0 σ 0 ) withval(c) = Tower(`, n) − 1 (resp. val(c0 ) = Tower(`, n) − 1) is a prefix of u (resp. u0 ).
7. eq(`,n) such that (T (P` ) × T (P`0 ), (u, u0 )) |= eq(`,n) if and only if there exist extended (`, n)counters cσ ∈ (Σ`−1 )∗ Ω` and c0 σ 0 ∈ (Σ0`−1 )∗ Ω0` such that (i) cσ is a prefix of u, (ii) c0 σ 0 is aprefix of u0 , and (iii) val(c) = val(c0 ).
8. inc(`,n) (resp. inc0(`,n) ) such that (T (P` ) × T (P`0 ), (u, u0 )) |= inc(`,n) (resp. (T (P` ) × T (P`0 ),(u, u0 )) |= inc0(`,n) ) if and only if there exist extended (`, n)-counters cσ ∈ (Σ`−1 )∗ Ω` and c0 σ 0 ∈(Σ0`−1 )∗ Ω0` such that (i) cσ is a prefix of u, (ii) c0 σ 0 is a prefix of u0 , and (iii) val(c) + 1 = val(c0 )(resp. val(c0 ) + 1 = val(c)).
9. succ(`,n) (resp. succ0(`,n) ) such that (T (P` ) × T (P`0 ), (u, u0 )) |= succ(`,n) (resp. (T (P` ) ×
T (P`0 ), (u, u0 )) |= succ0(`,n) ) if and only if there are extended (`, n)-counters c1 σ1 and c2 σ2 (resp.
c01 σ10 and c02 σ20 ) with σ1 , σ2 ∈ Ω` (resp. σ10 , σ20 ∈ Ω0` ) such that c1 σ1 c2 σ2 is a prefix of u andval(c1 ) + 1 = val(c2 ) (resp. val(c01 ) + 1 = val(c02 )).
The formulas that we will define will be exponential in ` and polynomial in n (represented inunary). This definition will be given by induction on `. We will start with the following simple
WW
0
observations: xcount(`,n) = σ∈Ω` countσ(`,n) , and xcount0(`,n) = σ0 ∈Ω0 countσ(`,n) . We will now`
construct several formulas ϕ that we evaluate on T (P` ) × T (P`0 ) expressing properties of the left
stack. Without making them explicit, we can construct corresponding analogs ϕ0 expressing therespective property on the right stack.
Let us proceed by defining the above formulas for the case of ` = 1. We define countσ(1,n) and0

countσ(1,n) as follows:countσ(1,n) = Ω0

n

hσi>

and

D En
0
countσ(1,n) = Ω00 hσ 0 i>

We put first(1,n) = h00 in hΩ1 i>. The definition of last(1,n) is analogous. We also define eq(1,n) as
Vn−1
Vxcount(1,n) ∧ xcount0(1,n) ∧ i=0 hΩ0 ii hΩ00 ii ∧ σ∈Ω0 (hσi> ↔ hσ 0 i>). The definitions of inc(1,n)
and succ(1,n) are analogous.
Let us now proceed to the case of ` > 1. We start by defining the formula countσ(`,n) for
each σ ∈ Ω` . We will achieve this, by making use of the formulas first(`−1,n) , last(j,n) withj ∈ [1, ` − 1], xcount(`−1,n) , and succ(`−1,n) . The first two conjuncts of the definition of countσ(`,n)
are self-explanatory,

h
i

∗
countσ(`,n) = first(`−1,n) ∧ Σ`−1
xcount(`−1,n) → last(`−1,n) ∨ succ(`−1,n)∧ addσ ,whereas the formula addσ will express that the symbol σ follows after the top-most (`, n)-counter.
σ
Formally we put addσ = ψ`−1
, whereh ∗ iσ Σj
if j > 1last(j,n) → ψj−1
ψjσ = h ∗ in Σlast(1,n) → 10 h11 ih12 i · · · h1`−2 ihΩ`−1 ihσi> if j = 1.
1
σIntuitively, the formula ψ`−1
jumps to last extended (1, n)-counter of the last extended (2, n)-counter. . . of the last extended (` − 1, n)-counter and expresses that the correct sequence follows from thisposition. We now define first(`,n) as follows:hi∗first(`,n) = xcount(`,n) ∧ Σ`−1Ω`−1 > → 0`−1 > .

The definition of last(`,n) is similar.

S. Göller and A. W. Lin

7

We now express eq(`,n) , for each ` > 1, as the conjunction of xcount(`,n) ∧ xcount0(`,n) and



h
i
D
E
∗
∗
Σ`−1 xcount(`−1,n) →  Σ0`−1 eq(`−1,n) ∧


^

0
.
(hΣ∗`−2 ihσi> ↔ hΣ0∗`−2 ihσ i>)σ∈Ω`−1

Let us give some intuition on the formulas eq(`,n) for each ` ∈ [2, k]: Whenever we pop from the left
stack some string from (Σ`−1 )∗ until on top of the left stack there is some extended (` − 1, n)-countercσ, one can remove from the right stack a string from (Σ0`−1 )∗ yielding an extended (` − 1, n) counterc0 τ 0 on top of the right stack such that val(c) = val(c0 ) and moreover σ = τ holds.
In analogy to eq(`,n) one can define the formula inc(`,n) . Finally, let us define succ(`,n) . We put
succ(`,n) = hΣ0` i (Σ0`−1 )∗



D

E
∗
Σ` inc0(`,n)
eq(`,n) ∧ Σ`−1

Intuitively, we the formula succ(`,n) pushes onto the right stack some string that it checks to be a copyof the topmost extended (`, n)-counter of the left stack via eq(`,n) , then pops the topmost extended(`, n)-counter of the left stack and then invokes the formula inc0(`,n) .
It is easy to see that the formulas given above express the desired properties. Furthermore, wenote that the size of each formula is exponential in ` and polynomial in n.
By using standard arguments (e.g. see the proof of PSPACE-hardness of EF model checking
over pushdown systems in [2]), we can now complete the proof of Theorem 2. In the following,
we shall only provide a sketch. For each integer k > 0, there exists a fixed Turing machine M
operating with Tower(k − 1, cn) space (for a constant c) whose membership problem is complete
for SPACE(Tower(k − 1, poly(n))). Each such membership problem can easily be reduced to EFmodel checking over the class of asynchronous products of two BPAs in polynomial time as follows.
For an input word w of M of length n one can construct formulas xcount(k,cn) and the pair of0
BPAs Pk+1 and Pk+1
in time poly(n). Each computation of M can be viewed as a sequence ofconfigurations (each being a (k, cn)-counters), which when considered together is also a (k + 1, cn)counter, satisfying the transition conditions of M (e.g. two consecutive configurations respect thetransition function of M). One can express the computation of M on w by an EF formula of the kindhΣ∗k+1 iϕ, where hΣ∗k+1 i aims at pushing a sequence onto the left stack and where ϕ expresses that
this sequence expresses the desired properties.
We will make use of the following lemma in Section 4.
I Lemma 3. Every DFA accepting the regular language
L`,n = {u ∈ Σ∗` | ∃u0 ∈ (Σ0` )∗ : (T (P` ) × T (P`0 ), (u, u0 )) |= xcount(`,n) }has at least Tower(` − 1, n) + 1 states.
Proof. Recall that every extended (`, n)-counter has length exactly Tower(` − 1, n) + 1. We haveL`,n = {cσw | w ∈ Σ∗` , cσ is some extended (`, n)-counter}. The corollary now follows from thefollowing simple observation: Every DFA A over some alphabet Σ with L(A) = U · Σ∗ for some
∅ ( U ⊆ Σm has at least m states.
J

3.2

Lower bounds for HM-logic

We conclude this section by showing how Theorem 2 implies a nonelementary lower bound for model
checking HM on the asynchronous product of two prefix-recognizable systems. A prefix-recognizable
system is a tuple R = (Σ, A, ∆), where Σ is finite set of process constants, A ⊆ Act is a finite

8

Concurrency Makes Simple Theories Hardset of action labels and ∆ is a finite set of rewrite rules of the form U 7→a V , where a ∈ A, andwhere U, V ⊆ Σ∗ are regular languages given as DFAs, say. The associated transition system isaa
T (R) = (Σ∗ , A, {−→| a ∈ A}), where −→= {(uw, vw) | u ∈ U, v ∈ V, w ∈ Σ∗ for some rule
U 7→a V ∈ ∆} for each a ∈ A.
Remark: One can construct from a given pair of BPAs P = (Σ, A, ∆) and P 0 = (Σ0 , A0 , ∆0 ) anda given EF formula ϕ over A ∪ A0 a pair of prefix-recognizable systems R = (Σ, A, ∆R ) and
R0 = (Σ0 , A0 , ∆0R ) and some HM formula ϕe such that [[ϕ]]T (P)×T (P) = [[ϕ]]e T (R)×T (R0 ) as follows:
00
By [4] one can compute for each Γ ⊆ A (analogously for each Γ ⊆ A ) a pair regular languages
UΓ and VΓ (resp. UΓ0 and VΓ0 ) each accepted by DFAs of at most exponential size such that the∗Γ ∗Γ0e = {(uw, vw) | u ∈relation −→ over Σ∗ × Σ∗ (resp. −→ over (Σ0 )∗ × (Σ0 )∗ ) is exactly R(Γ)∗
0 e0UΓ , v ∈ VΓ , w ∈ Σ } (resp. R (Γ ) = {(uw, vw) | u ∈ UΓ0 , v ∈ VΓ0 , w ∈ (Σ0 )∗ }). The latter iseven shown for PDAs in [4]. Hence we can define the HM formula ϕe to emerge from ϕ by replacing∗0 ∗eeach occurence of hΓ i by hΓi and each occurrence of h(Γ ) i by hΓe0 i.
Theorem 2 and the previous remark immediately imply the following corollary.
I Corollary 4. Model checking HM on the asynchronous product of two prefix-recognizable systems
is nonelementary.
We remark that model checking HM on a single prefix-recognizable system is only PSPACE-complete;
the upper bound can be shown via reduction to EF model checking pushdown systems, which is in
PSPACE by [21].

4Lower bounds for compositional methods for HM and EF logics

We start by proving nonelementary lower bounds for Feferman-Vaught type of compositional methodsfor HM and EF logics (i.e. Theorem 1) already over the the class of asynchronous products of two
transition systems. In Section 4.2 we will then show how our lower bounds can be relativized to theclass of all asynchronous products of two finite transition systems.
Let us briefly recall decompositions following Theorem 1 for EF logic of asynchronous productsof two transition systems. Analogously HM can be dealt with. A decomposition of the asynchronous
product of two transition systems, the first component being defined over action labels A and thesecond one over A0 (we assume that any two such sets A and A0 are non-empty and disjoint for the
rest of this section) is a triple D = (Ψ, Ψ0 , β), where Ψ = {ψi }i∈I and Ψ0 = {ψj0 }j∈J for index sets
I and J, where β is a positive boolean formula with variables ranging over {xi }i∈I ∪ {x0j }j∈J , eachψ ∈ Ψ (resp. each ψ 0 ∈ Ψ0 ) is an EF formula that is interpreted on the first (resp. second) component,
i.e. over A (resp. A0 ). Recall that such a decomposition has the property that for every pointed
transition system (T , s) over A and every pointed transition system (T 0 , s0 ) over A0 and every EF
formula ϕ over A ∪ A we have((T × T 0 ), (s, s0 )) |= ϕ⇔β[µ] is true,

where µ(xi ) = 1 if and only if (T , s) |= ψi and where µ(x0j ) = 1 if and only if (T 0 , s0 ) |= ψj0 . As
P
P
expected, the size of such a decomposition is defined as |D| = ψ∈Ψ |ψ| + ψ0 ∈Ψ0 |ψ 0 | + |β| .
I Theorem 5. The size of decompositions for EF (resp. HM) formulas in the sense of Theorem 1
cannot be bounded by an elementary function. More precisely, there is a family of EF (resp. HM)
formulas {ϕ` | ` ≥ 1} where ϕ` is defined over some action labels A` ∪ A0` , such that |ϕ` | = exp(`),
and such that for every elementary function f : N → N there is some h ∈ N such that every

S. Göller and A. W. Lin

9decomposition D for ϕh on the class of all asynchronous products of two transition systems over,respectively, Ah and A0h satisfies |D| > f (h).

4.1

Proof of Theorem 5

The proof idea for Theorem 5 for the case of EF-logic is as follows (we will remark how to adapt
it for HM-logic later). We consider the sequence of pairs of BPAs {(P` , P`0 )}`≥1 defined in theprevious section, where the set of states of T (P` ) (resp. T (P`0 )) is Σ∗` (resp. (Σ0` )∗ ). We will showthat if a small (i.e. of elementary size) decomposition for EF-formulas exists in general, then there
is a family of DFAs A` of size elementary in ` with L(A` ) = L`,` for each `, clearly contradicting
Lemma 3. To this end, we invoke the result from [2] about the sizes of automata expressing the sets ofconfigurations of BPAs satisfying EF formulas combined with standard constructions from automatic
structures.
We first recall the following proposition from [2] about the size of DFAs representing the set of
configurations of BPAs satisfying EF formulas.
I Proposition 6 ([2]). Given an EF formula ϕ and a BPA P = (Σ, A, ∆), there exists a DFA Aϕ ofsize double exponential in |P| + |ϕ| with L(Aϕ ) = [[ϕ]]T (P) , i.e. Aϕ accepts the set of states u ofT (P) with (T (P), u) |= ϕ.
Actually, in [2], the authors construct alternating finite automata with polynomially many states,
which can be translated to DFAs of double exponential size (e.g. see [18]).
Define {ϕ` | ` ≥ 1} as ϕ` = xcount(`,`) over the action labels A` = L` and A0` = L0` , whererecall that L` (resp. L0` ) are the action labels of the BPA P` (resp. P`0 ) defined in the previous section.
To prove Theorem 5, assume to the contrary that the there exist decompositions for EF formulas
ϕ whose sizes can be bounded from above by an elementary function, say by Tower(r, |ϕ|) forsome fixed r ∈ N. Let h ∈ N be a sufficiently large number for the following arguments to work.
Let us fix a smallest possible decomposition D = (Ψ, Ψ0 , β) for the EF formula ϕh = xcount(h,h)
over Lh ∪ L0h . Thus by assumption |D| ≤ Tower(r, |ϕh |). Let Ψ = {ψi }i∈I and Ψ0 = {ψj0 }j∈J .
Recall that each ψi ∈ Ψ is an EF formula over Lh , and each ψj0 ∈ Ψ0 is an EF formula over L0h .
Moreover β is a positive boolean formula over the variables {xi }i∈I ∪ {x0j }j∈J such that for every
state (u, u0 ) ∈ (Σh )∗ × (Σ0h )∗ of T (Ph ) × T (Ph0 ), it is the case that
(T (Ph ) × T (Ph0 ), (u, u0 )) |= ϕh⇐⇒β[µ] is true,

where µ is the assignment to β where we have µ(xi ) = 1 if and only if (T (Ph ), u) |= ψi andµ(x0j ) = 1 if and only if (T (Ph0 ), u0 ) |= ψj0 .
Next, we will use Proposition 6 and the small decomposition given by the assumption to constructa DFA for the language Lh,h = {u ∈ Σ∗h | ∃u ∈ (Σ0h )∗ : (T (Ph ) × T (Ph0 ), (u, u0 )) |= ϕh } withless than Tower(h − 1, h) + 1 states, which will contradict Lemma 3. To do so, we first make thefollowing simple observation that relates the decomposition D of ϕh and the formula ϕh itself.
Define the EF formula βe over Lh ∪ L0h to be obtained from the boolean formula β by replacing
each variable xi by ψi and each variable x0j by ψj0 . Then, since all formulas ψi and ψj0 are also
formulas over Lh ∪ L0h , the EF formula βe is also a formula over Lh ∪ L0h . Moreover, it is easy to seee T (P )×T (P 0 ) . In fact, the latter immediatelythat by assumption we have [[ϕh ]]T (Ph )×T (Ph0 ) = [[β]]hhfollows from the fact that[[ψi ]]T (Ph )×T (Ph0 )[[ψj0 ]]T (Ph )×T (Ph0 )=[[ψi ]]T (Ph ) × (Σ0h )∗ ,=Σ∗h × [[ψj0 ]]T (Ph0 )

and

(1)
(2)

which can easily be proven by induction on the structure of the formulas ψi and ψj0 since no action
labels of Ph (resp. Ph0 ) occur in the action labels of ψj0 (resp. ψi ). Thus, the goal to obtain a

10Concurrency Makes Simple Theories Hard

contradiction will be to show that we can find a small DFA fore = {u ∈ Σ∗ | ∃u0 ∈ (Σ0 )∗ : (T (Ph ) × T (P 0 ), (u, u0 )) |= β}.
eL1 (β)hhhUsing Proposition 6 we obtain DFAs for [[ψi ]]T (Ph ) (for each i ∈ I) and [[ψj0 ]]T (Ph0 ) (for each j ∈ J)
each of size double exponential in, respectively, |ψi |+|Ph | and |ψj |+|Ph0 |. To obtain a small DFA fore from these DFAs, we will now perform some simple constructions from automatic structures
L1 (β)(e.g. see [17]). We first briefly recall the notion of (binary) automatic relations. Fix a nonempty finite
alphabet Σ. A pair of words (u, w) = (a1 · · · am , b1 · · · bn ) ∈ Σ∗ × Σ∗ can be represented as a wordu ⊗ w = c1 · · · ck of length k = max(m, n) in the new alphabet Σ⊥ × Σ⊥ , where Σ⊥ = Σ ∪ {⊥}with a “padding” symbol ⊥ ∈/ Σ, and
if i ≤ m, i ≤ n
 (ai , bi )ci =(a , ⊥)
if i ≤ m, i > n i(⊥, bi )if i > m, i ≤ n.
A (binary) relation R ⊆ Σ∗ × Σ∗ is said to be automatic if the language {u ⊗ v | (u, v) ∈ R} ⊆(Σ⊥ × Σ⊥ )∗ can be accepted by a DFA (i.e. is regular). We also write π1 (R) to be the projection of
R to the first component, i.e., π1 (R) = {u ∈ Σ∗ | ∃w : (u, w) ∈ R}. The following proposition isstandard (e.g. see [17]):
I Proposition 7. Given two automatic relations R1 , R2 accepted by DFAs A1 and A2 , respectively,
the following statements hold:
The relation R1 ∩ R2 can be accepted by a DFA of size at most |A1 | · |A2 |.
The relation R1 ∪ R2 can be accepted by a DFA of size at most |A1 | · |A2 |.
The language π1 (R1 ) ⊆ Σ∗ can be accepted by a DFA of size 2O(|A1 |) .
Observe now that [[ψi ]]T (Ph )×T (Ph0 ) (for each i ∈ I) and [[ψj0 ]]T (Ph )×T (Ph0 ) (for each j ∈ J)
is an automatic relation over the alphabet Σ = Σh ∪ Σ0h that can be accepted by DFAs of size
double exponential in, respectively, |ψi | + |Ph | + |Ph0 | and |ψj0 | + |Ph | + |Ph0 | by Proposition 6. Thee can be done in a bottom-up fashion withconstruction of a small DFA A for the language L1 (β)
respect to βe using Proposition 7 by firstly taking unions and intersections from the DFAs recognizing[[ψi ]]T (Ph )×T (Ph0 ) (for each i ∈ I) and [[ψj0 ]]T (Ph )×T (Ph0 ) (for each j ∈ J), and at the end projecting
to the first component. All in all, there are constants c1 , c2 with c1 < c2 (both independent of h) suchthat
|A| ≤ Tower(c1 , |ϕh | + |Ph | + |Ph0 |) ≤ Tower(c2 , h).

(3)The latter inequality follows from the fact that |Ph | + |Ph0 | = poly(h) and |ϕh | = exp(h). On thee T (P )×T (P 0 ) and Lemma 3, we must haveother hand, due to [[ϕh ]]T (Ph )×T (Ph0 ) = [[β]]hh|A| ≥ Tower(h − 1, h) + 1.

(4)

It is clear that if we choose h sufficiently large, then inequalities (3) and (4) cannot hold at the sametime, a contradiction.
Remark. The proof above can be easily adapted to the case of HM-logic by taking prefix-recognizable^
systems and the HM formulas of the form xcount(`,`) defined in the remark given at the end of previous
section instead of BPAs and EF formulas of the form xcount(`,`) .

4.2

Restricting to finite transition systems

Theorem 5 gives a nonelementary lower bound for decompositions over asynchronous products of
two general transition systems. This still leaves the possibility that better upper bounds might be

S. Göller and A. W. Lin

11

possible when we consider only asynchronous products of finite transition systems, i.e., the version ofTheorem 1 when transition systems under consideration are finite. The following theorem shows that
this is not the case.
I Theorem 8. The size of decompositions for EF (resp. HM) formulas in the sense of Theorem 1
cannot be bounded by an elementary function when restricted to the class of finite transition systems.
Roughly speaking, this theorem can be proven by combining Theorem 5 and the fact that HM andEF logics satisfy “finite model property with respect to a finite set of formulas”: a logic L is said tosatisfy the finite model property with respect to a finite set of formulas whenever, for every finite setΞ of L-formulas and every pointed transition system (T , s) there exists a finite pointed transition
system (TΞ , sΞ ) such that for all ψ ∈ Ξ we have (T , s) |= ψ if and only if (TΞ , sΞ ) |= ψ.
It simple to check that when restricted to logics that are closed under boolean operations the finite
model property with respect to a finite set of formulas is equivalent to the the finite model property(for single formulas). To prove Theorem 8, the following technical lemma suffices.
I Lemma 9. Let ϕ be an HM (resp. EF) formula over the action labels A ∪ A0 for nonempty
disjoint sets A and A0 . Then, every decomposition of ϕ over all asynchronous products of two finite
systems over A and A, respectively, is also a decomposition of ϕ over all asynchronous products of
two general transition systems over A and A0 , respectively.
Observe that Theorem 5 and the above lemma immediately imply Theorem 8. We shall give the proof
of Lemma 9 for EF-logic. In fact, HM-logic can be dealt with completely analogously. We note that
EF (analogously HM) has the finite model property with respect to a finite set of formulas owing to
the same property for Propositional Dynamic Logic (of which EF-logic is a sublogic). The latter canbe proven e.g. via filtration (e.g. see [8]).
Let us now proceed to the proof of Lemma 9. Let fix an arbitrary EF-formula ϕ. Let C = (Φ, Φ0 , α)be a decomposition of ϕ over the class asynchronous products of two finite transition systems over
A and A0 , respectively. Let us assume Φ = {ϕk }k∈K and Φ0 = {ϕ0m }m∈M for index sets K and
M . We assume here that α is a boolean formula over the variables {xk }k∈K and {x0m }m∈M . It is
important to note here that we may only assume here that C is a decomposition for ϕ on the class ofasynchronous products of two finite transition systems over A and A0 , respectively.
In addition, we apply Theorem 1 to obtain a decomposition D = (Ψ, Ψ0 , β) of ϕ over the class ofasynchronous products of two general transition systems, where Ψ = {ψi }i∈I and Ψ0 = {ψj }j∈J .
We assume that β is a boolean formula over the variables {yi }i∈I and {yj0 }j∈J .
Let us define the finite set of formulas Ξ = Φ ∪ Ψ over A and Ξ0 = Φ0 ∪ Ψ0 over A0 . Let us fix
an arbitrary pointed transition system (T , s) over A and an arbitrary transition system (T 0 , s0 ) overA0 . Let us moreover fix some finite pointed transition systems (TΞ , sΞ ) over A and (TΞ0 0 , s0Ξ0 ) over A0
witnessing the finite model property with respect to Ξ and Ξ0 , respectively. To prove to lemma wewill show that already C is a decomposition, so we will show (T × T 0 , (s, s0 )) |= ϕ if and only if α
is true, if xk = ((T , s) |= ϕk ) and x0m = ((T 0 , s0 ) |= ϕ0m ). The latter follows from the following
equivalences:(T × T 0 , (s, s0 )) |= ϕ⇔β is true if yi = ((T , s) |= ψi ) and yj0 = ((T 0 , s0 ) |= ψj0 ).

⇔β is true if yi = ((TΞ , sΞ ) |= ψi ) and yj0 = ((TΞ0 0 , s0Ξ0 ) |= ψj0 ).

⇔(TΞ × TΞ0 0 , (sΞ , s0Ξ0 )) |= ϕ.

⇔α is true if xk = ((TΞ , sΞ ) |= ϕk ) and x0m = ((TΞ0 0 , s0Ξ0 ) |= ϕ0m ).

⇔α is true if xk = ((T , s) |= ϕk ) and x0m = ((T 0 , s0 ) |= ϕ0m ).

Hence, C is a decomposition over all (both finite and infinite) transition systems, completing theproof of Lemma 9.

12Concurrency Makes Simple Theories Hard

5

Future work

One possible future work concerns model checking HM-logic and EF-logic over the class of asynchronous products of finite systems. As we mentioned, compositional methods for these logics (i.e.
Theorem 1) yield polynomial-time model checking algorithms when the formula is fixed, albeit at thecost of nonelementary constant in the size of the formula. Is this nonelementary complexity in thesize of the formula inherent when the algorithm runs in time polynomial in the size of the systems?
Another open question is whether better upper bounds can be obtained for compositional methods for
HM-logic and EF-logic if we relativize the theorems to asynchronous products of finite trees.
Acknowledgements Anthony Lin thanks EPSRC (EP/H026878/1) for their support.
References
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

P. Blackburn, M. de Rijke, Y. Venema. Modal Logic. Cambridge University Press, 2001.
A. Bouajjani, J. Esparza, O. Maler. Reachability Analysis of Pushdown Automata: Applications toModel-Checking. In CONCUR’97, p. 135–150.
T. Cachat, I. Walukiewicz. The Complexity of Games on Higher Order Pushdown Automata. In
arxiv http://arxiv.org/abs/0705.0262
D. Caucal. On the Regular Structure of Prefix Rewriting In CAAP’90, p. 87–102.
D. Caucal. On infinite transition graphs having a decidable monadic theory. In ICALP’96, p. 194–
205.
A. Dawar, M. Grohe, S. Kreutzer, N. Schweikardt. Model Theory Makes Formulas Large. In
ICALP’07, p. 913–924.
I. Felscher, W. Thomas. Compositionality and Reachability with Conditions on Path Lengths. Int.
J. Found. Comput. Sci. 20(5): 851–868 (2009)
D. Harel, D.Kozen, J. Tiuryn. Dynamic Logic. MIT Press, 2000.
O. Kupferman, N. Piterman, M. Y. Vardi. Model checking linear properties of prefix-recognizable
systems. In CAV’02, p. 371–385.
L. Libkin. Elements of Finite Model Theory. Springer, 2004.
S. Lu, S. Park, E. Seo, Y. Zhou. Learning from mistakes: a comprehensive study on real worldconcurrency bug characteristics. In ASPLOS’08, p. 329–339.
J. A. Makowsky. Algorithmic uses of the Feferman-Vaught Theorem. Ann. Pure Appl. Logic
126(1–3): 159–213 (2004)
R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD
thesis, TU München, 1998.
S. Qadeer, J. Rehof. Context-Bounded Model Checking of Concurrent Software. In TACAS’05, p.
93–107.
A. Rabinovich. On compositionality and its limitations. ACM TOCL 8(1): (2007)
A. W. To. Model Checking FO(R) over One-Counter Processes and Beyond. In CSL’09, p. 485–
499.
A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD thesis,
University of Edinburgh, 2010.
M. Vardi An Automata-Theoretic Approach to Linear Temporal Logic In Banff Higher Order
Workshop ’95, p. 238-266.
S. Wöhrle, W. Thomas. Model Checking Synchronized Products of Infinite Transition Systems.
LMCS 3(4): (2007)
I. Walukiewicz. Difficult Configurations - On the Complexity of LTrL In ICALP ’98, p. 140–151.
I. Walukiewicz. Model Checking CTL Properties of Pushdown Systems. In FSTTCS’00, p. 127–138.