On the Computational Complexity of Verifying One-Counter Processes
Stefan Göller
Universität Bremen, Germany

Richard Mayr
University of Edinburgh, UK

Abstract—One-counter processes are pushdown systems overa singleton stack alphabet (plus a stack-bottom symbol).
We study the complexity of two closely related verification
problems over one-counter processes: model checking withthe temporal logic EF, where formulas are given as directed
acyclic graphs, and weak bisimilarity checking against finite
systems. We show that both problems are PNP -complete. Thisis achieved by establishing a close correspondence with themembership problem for a natural fragment of Presburger
Arithmetic, which we show to be PNP -complete. This fragment
is also a suitable representation for the global versions of the
problems. We also show that there already exists a fixed EF
formula (resp. a fixed finite system) such that model checking(resp. weak bisimulation) over one-counter processes is hardfor PNP[log] . However, the complexity drops to P if the onecounter process is fixed.
Keywords-Complexity theory, Logic

I. I NTRODUCTION
The state of the art. Pushdown automata (PDA) (orrecursive state machines; RSM) are a natural model forsequential programs with recursive procedure calls, andtheir verification problems have been studied extensively.
The reachability problem for PDA is polynomial [1, 4].
Model checking with the modal μ-calculus was shown to
be EXPTIME-complete in [29], and the global version of
the model checking problem has been considered in [2, 18].
The EXPTIME lower bound for model checking PDA also
holds for the simpler logic CTL and its fragment EG [28],even for a fixed formula. By modifying the construction in[28], it can easily be shown that EXPTIME-hardness evenholds for PDA with a finite control of size 1 (also known
as basic process algebras, BPA for short) and a general EG
formula. On the other hand, model checking PDA with thelogic EF (another natural fragment of CTL) is PSPACEcomplete [28], and again the lower bound still holds if either
the formula or the finite-state control of the PDA is fixed.
Another important aspect is the complexity of checking
semantic equivalences between two pushdown automata
and between pushdown automata and finite-state systems.
Strong- and weak bisimulation equivalence [16] are among
the most important semantic equivalences, since they are
the ones induced by standard temporal logics with strong(resp. weak) modalities. When comparing two pushdown
The first author was supported by the DFG project GELO during his
stay at Universität Leipzig. The third author was supported by EPSRC
grant E005039 and ORSAS Award.

Anthony Widjaja To
University of Edinburgh, UK

automata, weak bisimilarity is undecidable [22], while strong
bisimilarity is decidable [19] and EXPTIME-hard [12].
When comparing pushdown automata with finite-state systems [12, 14], weak- and strong bisimilarity are PSPACEcomplete, and for weak bisimilarity the lower bound evenholds for a fixed finite system. See the survey in [23] forfurther results.
One-counter processes (OCP) are Minsky counter machines with just one counter and action labels on the transitions. They can also be seen as a special case of pushdown
automata with just one stack symbol, plus a non-removablebottom symbol which indicates an empty stack (and thus
allows to test the counter for zero). So far, unlike for PDA,
the picture on the complexity of verification problems for
OCP was incomplete. While all upper complexity bounds
carry over from PDA, it was not clear how much easier
the verification problems are for OCP. Fixed-parametertractability results also take a slightly different meaning forone-counter processes, because (unlike for PDA, which varyin the number of used stack symbols) fixing the finite control
of one-counter processes results in a fixed process.
Model checking OCP with the μ-calculus is PSPACEcomplete. The PSPACE upper bound was shown in [20], anda matching lower bound can easily be shown by a reduction
from emptiness of alternating unary finite automata, which
was shown to be PSPACE-complete in [5, 10]. This lower
bound even holds if either the one-counter process or theformula is fixed. However, the complexity of model checking
OCP with CTL/EF was open. While the PSPACE upperbound carries over from μ-calculus, the best known lower
bound for CTL/EF was DP-hardness [9].
When comparing two one-counter processes, weak bisimilarity is undecidable [15], while strong bisimilarity is decidable [6] and PSPACE-hard [24]. When comparing a onecounter process to a finite-state system, strong bisimilarity
is polynomial [11], but weak bisimilarity was only known
to be in PSPACE and DP-hard [9, 11].
Our contribution. We establish the complexity of two main
open problems by showing them to be PNP -complete.
••

EF logic model checking one-counter processes.
Checking weak bisimilarity of a one-counter process
and a finite-state system.

These tight bounds cannot be shown by a direct applicationof automata theoretic techniques and semilinear sets as inLogicμ-calc.
μ-calc., fixed formula
μ-calc., fixed ctrl.
EFEF, fixed formulaEF, fixed ctrl.
Figure 1.

PDA
EXPTIME
EXPTIME
EXPTIMEPSPACEPSPACEPSPACEOCPPSPACEPSPACEPSPACEPNP (*)
PNP[log] hard (*)
in P (*)

Model checking over PDA and OCP

the case of PDA; instead they require a careful analysis ofa special fragment of Presburger Arithmetic (see below).
By default, we represent EF formulae as a dag (i.e., asa directed acyclic graph, not as a tree) which allows one
to re-use common subformulae efficiently. (Note that the
PSPACE upper bound for EF model checking PDA [28]can easily be extended to formulae in this dag representation.) We establish a close correspondence between the EFmodel checking problem for one-counter processes and themembership problem for a natural fragment of Presburger
Arithmetic, which we show to be PNP -complete. We use
quantifier-free Presburger Arithmetic over one variable withaddition, subtraction, inequalities, tests of divisibility, andmin/max operations. This fragment of Presburger Arithmeticis also shown to be a suitable global representation when one
considers the global model checking problem. A matching
PNP lower bound is shown by a reduction from DSAT forthe case of EF formulae represented as a dag, while the best
lower bound for tree-represented EF formulae is PNP[log] .
In fact, there already exists a fixed EF formula such thatmodel checking one-counter processes is hard for PNP[log] ,i.e., the data-complexity is PNP[log] -hard. However, unlike
for most other model checking problems, the expression
complexity (i.e., the complexity in the size of the formula) is
polynomial. In particular, if the one-counter process is fixed,
then the problem becomes solvable in P.
Checking weak bisimilarity of a one-counter process anda finite-state system is shown to be in PNP by a polynomialtime reduction to the EF model checking problem, using thepolynomial-size characteristic EF formulae (in dag representation) introduced in [8] (for a more accessible presentationof characteristic formulae see [7]). A matching PNP lower
bound is shown by a reduction from DSAT. Analogously
to the model checking problem, there exists a fixed finite
system such that weak bisimulation checking with onecounter processes is hard for PNP[log] . However, if the onecounter process is fixed, checking weak bisimulation withfinite-state systems becomes solvable in P.
Figure 1 summarizes the picture on the complexity ofmodel checking for PDA and OCP, whereas Figure 2
summarizes the complexity of weak (≈) and strong (∼)
bisimulation with finite systems for PDA and OCP. Our
results are marked with (*).
This paper is structured as follows. In Section II we

Bisimulation type≈ finite system≈ fixed finite system
fixed ctrl. ≈ finite system∼ finite system∼ fixed finite system
fixed ctrl. ∼ finite system
Figure 2.

PDA
PSPACEPSPACEP
PSPACEin P
POCP
PNP (*)
PNP[log] hard (*)
in P (*)
P
in P
in P

Bisimulation over PDA and OCP

formally define the considered problems and introduce somebasic notation. In Section III we define our special fragmentof Presburger Arithmetic and establish its fundamental properties. In Section IV we show how to efficiently transform
one-counter processes into a suitable normal form, and in
Section V we describe the construction of the Presburger
formulas which solve the EF model checking problem in
PNP . Lower bounds for model checking EF over OCP are
shown in Section VI. In Section VII we study the problemof checking weak bisimilarity of a one-counter process and afinite-state system. The paper concludes with a brief section
on future work.
II. P RELIMINARIES
General notation: By N = {0, 1, . . .} we denote the natural
numbers. For i, j ∈ N we define [i, j] = {i, i+1, . . . , j} and[j] = [1, j]. Extend the usual arithmetic operations on N tosets of numbers as follows. For each  ∈ {+, −, ·} andA, B ⊆ N, we define A  B = {a  b | a ∈ A, b ∈ B}.
For a ∈ N, we shall also write a  B to mean {a}  B.
An arithmetic progression is any set of numbers of the forma + bN defined as a + b · N for some a, b ∈ N. The number a(resp. b) is said to be the offset (resp. period) of a + bN. By
log we denote the logarithm to base 2. A dag is a directed
acyclic graph.
Computational complexity: We assume familiarity withthe standard complexity classes P, NP, PSPACE, and with
notions of completeness for a complexity class. In thispaper, reductions are always polynomial-time many-to-one
reductions. By PNP (resp. PNP[log] ) we denote the class oflanguages decidable by some deterministic polynomial-timeTuring machine that can invoke some NP oracle (resp. atmost logarithmically many times). Recall thatNP ∪ coNP ⊆ PNP[log] ⊆ PNP ⊆ PSPACE.
Moreover recall that the second level of the polynomial
hierarchy lies between PNP and PSPACE. For more details,
we refer the reader to the textbook [17].
One-counter processes and transition systems: Fix somecountable set Σ of actions. A transition system is a pair
T = (S, {→a | a ∈ Σ}), where S is a set of states and→a ⊆ S × S is a set of a-labeled transitions for each a ∈ Σ.
We write s1 →a s2 to abbreviate (s1 , s2 ) ∈→a . We write

s1 →T s2 whenever s1 →a s
2 for some a ∈ Σ. We define
the size of T as |T | = |S| + a∈Σ | →a |.
A one-counter process is a tuple O = (Q, δ0 , δ>0 ), where
Q is a finite set of control locations, δ0 ⊆ Q×Σ×Q×{0, 1}
is a finite set of zero transitions, and δ>0 ⊆ Q × Σ × Q ×{−1, 0, 1} is a finite set of positive transitions. The size ofa one-counter process is defined as |O| = |Q| + |δ0 | + |δ>0 |.
A one-counter net is a one-counter process that additionallysatisfies δ0 ⊆ δ>0 .
A one-counter process O = (Q, δ0 , δ>0 ) defines a transition
system T (O) = (Q × N, {→a | a ∈ Σ}), where (q, n) →a(q  , n + k) if and only if either n = 0 and (q, a, q  , k) ∈ δ0 ,or n > 0 and (q, a, q  , k) ∈ δ>0 . If (q1 , n1 ) →a (q2 , n2 ) forsome a ∈ Σ, we also write (q1 , n1 ) →O (q2 , n2 ).
EF logic and weak bisimulation: An EF dag-formula
is a finite sequence of definitions ϕ = (ϕi )i∈[l] for somel ∈ N, where for each i ∈ [l] the definition ϕi is exactly
one of the following, either: ϕi = true, ϕi = ¬ϕj forsome j ∈ [i − 1], ϕi = ϕj ∧ ϕk for some j, k ∈ [i − 1],
ϕi = a ϕj for some a ∈ Σ and some j ∈ [i − 1], or
ϕi = EFϕj for some j ∈ [i − 1]. For each i ∈ [l], we= log idefine the size |ϕi | = 1 if ϕi = true and |ϕi |lotherwise. The size of ϕ is defined as |ϕ| =i=1 |ϕi |.
Define the partial order ≺ϕ ⊆ [l] × [l] as (j, i) ∈≺ϕ if andonly if ϕj appears in the definition of ϕi . If j ≺+ϕ i, we saythat ϕj is a subformula of ϕi . Note that i is minimal withrespect to ≺+ϕ whenever ϕi = true. Observe that ([l], ≺ϕ )is a dag. We call ϕ an EF tree-formula if moreover ([l], ≺ϕ )is a directed tree. Next, we define the semantics. For this,let T = (S, {→a | a ∈ Σ}) be a transition system. Let us
define [[ϕi ]]T ⊆ S for each i ∈ [l] by induction on ≺+ϕ asfollows: [[true]]T = S, [[¬ϕj ]]T = S \ [[ϕj ]]T , [[ϕj ∧ ϕk ]]T =[[ϕj ]]T ∩ [[ϕk ]]T , [[ a ϕj ]]T = {s ∈ T | ∃t ∈ [[ϕj ]]T : s →a t},
and [[EFϕj ]]T = {s ∈ S | ∃t ∈ [[ϕj ]]T : s →∗T t}. We
define [[ϕ]]T = [[ϕl ]]T . We also write (T, s) |= ϕi whenevers ∈ [[ϕi ]]T . We deal with the model checking problem for
EF over one-counter processes defined as follows.
M ODEL CHECKING
Instance: A one-counter process O, a state (q, n) of T (O)with n given in binary, and an EF dag/treeformula ϕ.
Question: (T (O), (q, n)) |= ϕ?
We also consider global model checking in this paper,
which asks to compute a function mapping each control
location q of O to a representation of all n ∈ N such that
(T (O), (q, n)) |= ϕ.
We recall the definition of weak bisimulation [7]. Let T =(S, {→a | a ∈ Σ}) be a transition system and assume somedistinguished internal symbol τ ∈ Σ. Define the extended
transition relation ⇒a ⊆ S × S for each a ∈ Σ as s ⇒at if and only if either a = τ and there exist s , t ∈ Ssuch that s →∗τ s →a t →∗τ t, or a = τ and s →∗τ t.
Given two transition systems T = (S, {→a | a ∈ Σ}) andT  = (S  , {→a | a ∈ Σ}), a relation R ⊆ S × S  is a wbisimulation if it is nonempty, and whenever (s, s ) ∈ R,
then for every a ∈ Σ the following two conditions hold(i) if s →a t for some t ∈ S, then s ⇒a t for somet ∈ S  such that (t, t ) ∈ R, and (ii) if s →a t for somet ∈ S  , then s ⇒a t for some t ∈ S such that (t, t ) ∈ R.
For every s ∈ S and every s ∈ S  , we say that s ands are w-bisimilar, written s ≈ s , whenever there exists
a w-bisimulation R ⊆ S × S  such that (s, s ) ∈ R. We
now define w-bisimilarity checking of one-counter processes
against finite systems as follows.
W-B ISIMILARITY C HECKING
Instance: A one-counter process O, a state (q, n) of T (O)with n given in binary, a finite system T , and astate t of T.
Question: (q, n) ≈ t?
III. A SUITABLE QUANTIFIER - FREE LOGICIn this section we introduce a suitable representation of natural numbers in terms of a logic that we call MMA for MinMax Arithmetic. In fact, the sets definable in MMA equal thesets definable in Presburger Arithmetic with one free variable
or equivalently the one-dimensional semilinear sets. MMA
can be seen as a syntactic variant of Presburger Arithmetic
that is tailored towards having a fairly low complexity (PNP )of the membership problem. Moreover, MMA is a suitableformalism for representing solutions of global EF model
checking and global w-bisimilarity checking against finite
state systems over one-counter processes.
Formally, an MMA dag-formula is a sequence of definitions α = (αi )i∈[l] for some l ≥ 1, where for each i ∈ [l]the definition αi is precisely one of the following, wherej, k ∈ [i − 1] and where ∼∈ {≤, ≥}:(1) ≡ m mod n, where n > 0 and m ∈ Z/nZ,(2) ∼ n, where n ∈ N,(3) ¬αj(4) αj ∧ αk ,(5) ∼ min αj ,(6) n ∼ min αj , where n ∈ N,(7) ∼ max(αj , n), where n ∈ N, or(8) m ∼ max(αj , n), where m, n ∈ N.
We call αi atomic in case it is of type (1) or (2). We will
introduce usual abbreviations <, >, and = as expected. We
formally put min ∅ = ∞, max ∅ = −1. Moreover we put
k ≤ ∞ and k ≥ ∞, k ≤ −1, and k ≥ −1 for each k ∈ N.
Define the binary relation ≺α ⊆ [l]×[l] as j ≺α i if and only
if αj occurs in the definition of αi for each i, j ∈ [l]. Notethat ([l], ≺α ) is a dag and hence ([l], ≺+α ) is a strict partial
order. Recall that i is minimal with respect to ≺+α if and only
if αi is atomic. We say α is a MMA tree-formula if ([l], ≺α )is a directed tree. Let us now define the semantics of MMA
dag-formulas. For each αi we define the set [[αi ]] ⊆ N by
induction on i w.r.t. ≺+α as follows:(1) [[≡ m mod n]] = {k ∈ N | k ≡ m mod n},(2) [[∼ n]] = {k ∈ N | k ∼ n},(3) [[¬αj ]] = N \ [[αj ]],(4) [[αj ∧ αk ]] = [[αj ]] ∩ [[αk ]],∈ N | k ∼ min[[αj ]]},
(5) [[∼ min αj ]] = {kN if n ∼ min[[αj ]](6) [[n ∼ min αj ]] =,∅otherwise(7) [[∼ max(αj , n)]] = {k ∈ N | k ∼ max([[αj ]] ∩ [0, n])},(8)N if m ∼ max([[αj ]] ∩ [0, n])[[m ∼ max(αj , n)]] =∅ otherwise.
Observe that MMA can be seen as a fragment of Presburger
Arithmetic. We define [[α]] = [[αl ]]. We call α valid if[[α]] = N, for example ≥ 0 is valid. Define the size |αi |by case distinction as follows: | ≡ m mod n| = | ∼ n| =log n , |¬αj | = log j , |αj ∧ αk | = log j + log k ,| ∼ min αj | = log j , |n ∼ min αj | = log n + log j ,| ∼ max(αj , n)| = log j + log n , and finally |m ∼max(αj , n)|= log m + log j + log n . Define the size of
α as |α| = i∈[l] |αi |. For better readability, we will allow
more complex definitions such as e.g. αi = ¬αj ∧ (x ≡ 3
mod 5).
Syntactic sugar - Extended MMA : In order to ease our
reduction from model checking OCP to evaluating MMA
formulas, we introduce extended MMA formulas. Extended
MMA formulas allow definitions of the kind αi = αj − 1and αi = αj + 1. For  ∈ {+, −}, the semantics is definedas [[αj  1]] = [[αj ]]  1. Observe that, in general, the two
operators cannot be interchanged, i.e. we generally do nothave [[(α − 1) + 1]] = [[(α + 1) − 1]]. But observe that [[α]] =[[(α + 1) − 1]]. Define the size of |αj + 1| = |αj − 1| =log j + 1. For each natural k define αj  k to be theabbreviation for(· · · (αj 1) · · · )  1k many times

for each  ∈ {−, +}.
Let α = (αi )i∈[l] be an extended MMA dag-formula.
Define νi to be maximal number n such that αj is ∼ nor ∼ max(αj , n) for some j ∈ [i]. Define Li to be the least
common multiple of all n > 0 such that the definition of αjis ≡ m mod n for some j ∈ [i − 1] and some m ∈ Z/nZ,
and 1 if no such formula exists. Observe that i < j implies
Li |Lj and moreover Li ∈ exp(|α|), thus polynomially (in|α|) many bits suffice to represent each Li . For extended
MMA , we now state a simple but important periodicity
lemma.
Lemma 1 (Periodicity Lemma for extended MMA) Leti ∈ [l] and assume n1 , n2 > i · Li + νi . Then the following
implication holds:
n1 ≡ n2 mod Li⇒(n1 ∈ [[αi ]] ⇔ n2 ∈ [[αi ]])Proof: We prove the lemma by induction on ≺+α.
For the induction base, assume i is minimal with respect to≺+
α , i.e. αi is atomic.
Case αi is ≡ m mod n for some n > 0 and somem ∈ Z/nZ. Observe that the implication holds since Li
is a multiple of n by definition.
Case αi is ∼ n, where ∼∈ {≤, ≥} and where n ∈ N. By
definition we have νi ≥ n. The implication clearly holds
since natural numbers exceeding n are either all containedin [[αi ]] or are all not contained in [[αi ]].
For the induction step, assume that i is not minimal withrespect to ≺+α . For this, we make a case distinction according
to αi .
Case αi = ¬αj for some j ∈ [i − 1]. The required
implication holds trivially due to induction hypothesis andthe fact that j · Lj + νj ≤ i · Li + νi and Li = Lj .
Case αi = αj ∧ αk for some j, k ∈ [i − 1]. First, we havethat both Lk and Lj divide Li . Second, both j · Lj + νjand k · Lk + νk are at most i · Li + νi . Now let n1 , n2 >i · Li + νi and assume n1 ≡ n2 mod Li . Then we haven1 ∈ [[αi ]] if and only if n1 ∈ [[αj ]] and n1 ∈ [[αk ]]. By
induction hypothesis, the latter is equivalent to n2 ∈ [[αj ]]and n2 ∈ [[αk ]] which is in turn equivalent to n2 ∈ [[αi ]].
Case αi is ∼ min αj for some ∼∈ {≤, ≥} and for somej ∈ [i − 1]. We claim that the implication holds for i by
distinguishing if [[αj ]] is empty or not. In case [[αj ]] = ∅,(recall min ∅ = ∞), then [[αi ]] either equals N or ∅,depending on ∼. The implication obviously holds in thiscase. In case [[αj ]] = ∅, then there exists some n ∈ [[αj ]] withn ≤ j·Lj +νj +Lj by induction hypothesis. Observe that thelatter is less than or equal to (i−1)·Li +νi +Li = i·Li +νi .
Again, depending on ∼, all naturals exceeding n (in particular naturals exceeding i · Li + νi ) are either all in [[αi ]] or
are all not in [[αi ]]. Thus, the implication holds.
Case αi = n ∼ min αj for some n ∈ N, some ∼∈ {≤, ≥},and some j ∈ [i − 1]. Since [[αi ]] either equals N or ∅, theimplication trivially holds.
Case αi is ∼ max(αj , n) for some ∼∈ {≤, ≥}, somej ∈ [i − 1], and some n ∈ N. First observe that n ≤ νiby definition. Second, all naturals exceeding n (in particular
those exceeding νi ) either all satisfy αi or all do not,depending on ∼. Thus, the implication holds.
Case αi is m ∼ max(αj , n) for some ∼∈ {≤, ≥}, somej ∈ [i − 1], and some m, n ∈ N. Since [[αi ]] either equals Nor ∅, the implication holds trivially.
Case αi = αj  1 for some j ∈ [i − 1] and some  ∈{+, −}. The implication follows directly from j · Lj + νj +1 ≤ (i − 1) · Li + νi + Li = i · Li + νi and induction
hypothesis.
It turns out that extended MMA formulas are neither more
expressive nor more succinct than MMA formulas.

Lemma 2 The following problem is computable in polynomial time:
INPUT: An extended MMA dag-formula α.
OUTPUT: A MMA dag-formula β such that [[α]] = [[β]].

Proposition 4 The following problem is PSPACE-complete:
INPUT: An extended MMA dag-formula α, where offsets
are given in binary.
QUESTION: 0 ∈ [[α]]?

By a bottom-up computation and combining Lemma 1 andLemma 2, we can deduce a PNP upper bound for themembership problem for extended MMA .

IV. S ATURATING ONE - COUNTER PROCESSES AND

Proposition 3 The following problem is in PNP :INPUT: n0 ∈ N in binary and an extended MMA dagformula α.
QUESTION: n0 ∈ [[α]]?
Proof: First, it is easy to see that if α is an MMA dagformula with no occurrence of min and max then checking
whether n0 ∈ [[α]] can be done is polynomial time. We shallmake use of this basic fact in the proof. In a first step,
we apply Lemma 2 and compute in polynomial time an
MMA dag-formula formula β such that [[β]] = [[α]]. Assume
β = (βi )i∈[l] . In a second step, we eliminate min and max
operators that occur in β inductively on ≺+β.
For this, let i ∈ [l] be minimal with respect to ≺+β suchthat the definition βi contains either min or max. In case
βi is ∼ min βj , we know that for each n1 , n2 > j · Lj + νjwith n1 ≡ n2 mod Lj we have n1 ∈ [[βj ]] if and only
if n2 ∈ [[βj ]] by Lemma 1. This implies that min[[βj ]] ∈[0, (j + 1) · Lj + νj ] ∪ {∞}. Moreover, observe that (j +1) · Lj + νj can represented using polynomially many bits in|β|. Furthermore, note that we can decide deterministicallyin polynomial time whether, for a given m given in binary,
we have m ∈ [[βj ]], since neither the definition of βj nor thedefinition of βk contains min or max, for each k ≺+β j. Viaa binary search method, we can compute
μ = min{m ∈ [0, (j + 1) · Lj + νj ] | m ∈ [[βj ]]}by some deterministic polynomially time bounded Turingmachine that has access to an NP oracle. After that, we“symbolically” modify β by replacing βi ’s previous definition ∼ min βj by ∼ μ.
The cases when βi = n ∼ min βj , βi =∼ max(βj , n), or
βi = m ∼ max(βj , n) can be dealt with analogously.
We repeat this replacement process until β does not containany min or max operator. Finally, we check if n0 ∈ [[β]] in
polynomial time.
Observe that we can think of extended MMA to be MMA
enhanced with the usage of “offsets” of the kind αj ± k,
where k is a natural that is given in unary. The question
arises, why one does not extend MMA more generally, byallowing offsets to be given in binary. However, this yields
a logic with a PSPACE-complete membership problem.

COMPUTING SMALL ARITHMETIC PROGRESSIONSFor the rest of this section, let us fix some one-counter
process O = (Q, δ0 , δ>0 ). For technical reasons, we add
a new transition label λ ∈ Σ that does not previously occur
in δ0 ∪ δ>0 and which we fix for the rest of this section. Our
goal is to “saturate” O with λ-labeled transitions so that weonly have to consider normalized paths, i.e. paths, where
the sequence of counter values of the involved states are
first non-increasing and then non-decreasing. Let O denote
the resulting OCP after saturation. Our saturation construction has the following motivation: (1) We can compute inpolynomial time all information needed for representing
normalized paths in T (O ) in terms of few small arithmetic
progressions. (2) For every EF dag-formula ϕ in which λdoes not occur we have (T (O), s) |= ϕ if and only if(T (O ), s) |= ϕ for every state s ∈ Q × N.
A path in T (O) is a non-empty finite sequence of states
π = (q1 , n1 ) →O (q2 , n2 ) · · · →O (qk , nk ). We call π
mountain, if n1 = nk and ni ≥ n1 for each i ∈ [k]. We
call π zero, if ni = 0 for some i ∈ [k], otherwise we call
π positive. Let (q1 , n1 ), (q2 , n2 ) ∈ Q × N be states. Then,we write (q1 , n1 ) ↓O (q2 , n2 ) (resp. (q1 , n1 ) ↑O (q2 , n2 ))whenever (q1 , n1 ) →O (q2 , n2 ) and n2 ≤ n1 (resp. andn2 ≥ n1 ). We now present a saturation construction thatallows us to shortcut mountain paths by adding λ-transitions.
Choosing control locations q, q  ∈ Q and δ ∈ {δ0 , δ>0 },we now present rules (R1) to (R4) that can be applied only
if (q, λ, q  , 0) ∈ δ. In this case, we can add the transition(q, λ, q  , 0) to δ if at least one of the following conditions
holds:(R1) (q, a, q  , 0) ∈ δ for some a ∈ Σ.
(R2) (q, a1 , q1 , +1) ∈ δ and (q1 , a2 , q  , −1) ∈ δ>0 for someq1 ∈ Q and some a1 , a2 ∈ Σ.
(R3) (q, a1 , q1 , +1) ∈ δ, (q1 , λ, q2 , 0) ∈ δ>0 , and(q2 , a2 , q  , −1) ∈ δ>0 for some q1 , q2 ∈ Q and some
a1 , a2 ∈ Σ.
(R4) (q, λ, q1 , 0) ∈ δ and (q1 , λ, q  , 0) ∈ δ for some q1 ∈ Q.
Formally, let O = (Q, δ0 , δ>0) denote the unique onecounter process that we obtain from O by applying rules(R1)–(R4) until it is no longer possible.
Lemma 5 Let s, t ∈ Q × N be states. Then, the following
three statements are equivalent:(1) s →∗O t.
(2) s →∗O t.
(3) There exists some state u ∈ Q × N such that s ↓∗O u
and u ↑∗O t.

Observe that if (q1 , n1 ) ↑∗O (q2 , n2 ) and n1 > 0, then also
(q1 , n1 + i) ↑∗O (q2 , n2 + i) for each i ∈ N. Similarly, if(q1 , n1 ) ↓∗O (q2 , n2 ) and n2 > 0, then also (q1 , n1 + i) ↓∗O
(q2 , n2 + i) for each i ∈ N. This motivates us to define, foreach q1 , q2 ∈ Q, the following set of differences of countervalues of monotone positive paths:∗
Δ>0↑ (q1 , q2 ) = {d ∈ N | (q1 , 1) ↑O  (q2 , d + 1)}∗
Δ>0↓ (q1 , q2 ) = {d ∈ N | (q1 , d + 1) ↓O  (q2 , 1)}

Analogously, we collect the set of differences of countervalues of monotone zero paths:∗
Δ=0↑ (q1 , q2 ) = {d ∈ N | (q1 , 0) ↑O  (q2 , d)}∗
Δ=0↓ (q1 , q2 ) = {d ∈ N | (q1 , d) ↓O  (q2 , 0)}

A theorem due to Chrobak [3] and Martinez [13] statesthat from a nondeterministic finite automaton over a unaryalphabet one can compute in polynomial time an at mostquadratically larger equivalent one that is in a certain normal
form (Chrobak normal form). However, both papers containa subtle flaw that was recently fixed in [25]. The following
lemma will use this result.
>0
Lemma 6 Each of the sets Δ>0↑ (q1 , q2 ), Δ↓ (q1 , q2 ),=0=0Δ↑ (q1 , q2 ), Δ↓ (q1 , q2 ) is equivalent to a union of
O(|Q|2 ) arithmetic progressions with offsets bounded by
O(|Q|2 ) and periods bounded by O(|Q|) that are moreovercomputable in polynomial time.

Let q1 , q2 ∈ Q be control locations. Note that if (q1 , n) ↓∗O
(q3 , 1) ↑∗O (q2 , n) for some q3 ∈ Q, then also (q1 , n+i) ↓∗O
(q3 , 1 + i) ↑∗O (q2 , n + i). Therefore, we define ∇(q1 , q2 ) ∈N ∪ {∞} to bemin{n > 0 | ∃q3 ∈ Q : (q1 , n) ↓∗O (q3 , 1) ↑∗O (q2 , n)}.
Observe that ∇(q, q) = 1 for every q ∈ Q.
Lemma 7 Either ∇(q1 , q2 ) = ∞ or ∇ ∈ O(|Q|2 ). Moreover ∇(q1 , q2 ) can be computed in polynomial time.

V. A TRANSLATION TO MMA
For the rest of this section, let us fix a one-counter process
O = (Q, δ0 , δ>0 ) and an EF dag-formula ϕ = (ϕi )i∈[l] .
Assume that Q = {q1 , . . . , qk }. Due to technical simplicity,
we will confuse each element (qi , j) ∈ Q × [l] with thecorresponding natural number i + (j − 1) · k ∈ [k · l]. The
goal is to present a polynomial time algorithm to computean extended MMA formula α = (α(q,j) )(q,j)∈Q×[l] suchthat [[α(q,j) ]] = {n ∈ N | (T (O), (q, n)) |= ϕj } for each(q, j) ∈ Q × [l].
First, we saturate O in the sense of Section IV in polynomial
time. Then, we apply Lemma 6 and compute in polyno>0=0mial time the sets Δ>0↓ (q, q ), Δ↑ (q, q ), Δ↓ (q, q ), and=02Δ↑ (q, q ), which are each unions of O(|Q| ) arithmetic
progressions with offsets bounded by O(|Q|2 ) and periods
bounded by O(|Q|) for each q, q  ∈ Q. By applying Lemma
9 we compute in polynomial time ∇(q, q  ) ∈ [n∇ ] ∪ {∞}for each q, q  ∈ Q, where n∇ ∈ O(|Q|2 ).
Let us now present the computation of α =(α(q,j) )(q,j)∈Q×[l] . We will do this by induction on j withrespect to ≺+ϕ and simultaneously for each q ∈ Q.
Base. Assume j is minimal with respect to ≺+ϕ . Thenϕj = true and we put α(q,j) = (≥ 0) for each q ∈ Q.
Step.
Assume ϕj = ¬ϕj  for some j  ∈ [j − 1]. Then we putα(q,j) = ¬α(q,j  ) for each q ∈ Q.
Assume ϕj = ϕj1 ∧ ϕj2 for some j1 , j2 ∈ [j − 1]. Then weput α(q,j) = α(q,j1 ) ∧ α(q,j2 ) for each q ∈ Q.
Assume ϕj = a ϕj  for some a ∈ Σ and some j  ∈ [j − 1].
By induction hypothesis, we haveα(q ,j  ) = {n ∈ N | (q  , n) |= ϕj  }for each q  ∈ Q. By putting + = − and − = +, we defineα(q,j) as the conjunction of⎞⎛⎜(= 0) → ⎝α(q ,j  ) − 1 ∨q  ∈Q:(q,a,q  ,+1)∈δ0

The next lemma characterizes zero paths.

⎟α(q ,j  ) ⎠q  ∈Q:(q,a,q  ,0)∈δ0

and




Lemma 8 There is a zero path from (q, n) to (q , n ) in
=0  T (O ) if and only if n ∈ Δ=0↓ (q, q ) and n ∈ Δ↑ (q , q )for some q ∈ Q.
The next lemma characterizes positive paths.
Lemma 9 Assume n ≤ n . Then there exists a positive pathin T (O ) from (q, n) to (q  , n ) if and only if n ≥ ∇(q, q  ) and n − n ∈ Δ>0↑ (q , q ) for some q ∈ Q.
Assume n ≥ n . Then there exists a positive path from (q, n)to (q  , n ) in T (O ) if and only if n ≥ ∇(q  , q  ) and n−n ∈


Δ>0
↓ (q, q ) for some q ∈ Q.

⎞⎛⎜(> 0) → ⎜⎝α(q ,j  ) 1 ∨q  ∈Q,∈{−,+}:(q,a,q  ,1)∈δ>0⎟α(q ,j  ) ⎟⎠.

q  ∈Q:(q,a,q  ,0)∈δ>0

Finally, assume ϕj = EFϕj  for some j  ∈ [j − 1]. Let us
first fix control locations q, q  ∈ Q. By induction hypothesis[[α(q ,j  ) ]] = {n ∈ N | (q  , n) |= ϕj  }.
By Lemma 1 we know that for each n1 , n2 ∈ N which
exceed a threshold t(q ,j  ) such that n1 ≡ n2 mod L(q ,j  ) we

have n1 ∈ [[α(q ,j  ) ]] if and only if n2 ∈ [[α(q ,j  ) ]]. Note that
this implies that [[α(q ,j  ) ]] is infinite if and only if there exists
some n ∈ [[α(q ,j  ) ]] such that t(q ,j  ) < n ≤ t(q ,j  ) +L(q ,j  ) .
Let us now fix an arithmetic progression a+bN with b > 0>0that is a subset of some of the sets Δ>0↓ (q, q ),Δ↑ (q, q ),
=0

=0

Δ↓ (q, q ), or Δ↑ (q, q ). Moreover, let c ∈ Z/bZ besome residue class. We aim at defining an MMA formulainf(q  , j  , c, b) that is valid if and only if there are infinitely
many naturals that satisfy α(q ,j  ) and that are congruent
c modulo b. Now observe that the latter is the case exactly whenever there exists some n ∈ [[α(q ,j  ) ]] such thatt(q ,j  ) < n ≤ t(q ,j  ) + L(q ,j  ) and moreover n ≡ c
mod gcd(b, L(q ,j  ) ). Let us define the auxiliary MMA
formulaψ(q  , j  , c, b) = α(q ,j  ) ∧ (≡ c mod gcd(b, L(q ,j  ) ))and finally inf(q  , j  , c, b) ast(q ,j  ) < max(ψ(q  , j  , b, c), t(q ,j  ) + L(q ,j  ) ).
Next, we aim at defining the set{n ∈ N | ∃n ∈ N : (q, n) →∗O (q  , n ), (q  , n ) |= ϕj  }in terms of an extended MMA formula. For this, assume
that there is a path π from (q, n) to (q  , n ) in T (O) suchthat (q  , n ) |= ϕj  , where n ∈ N. We distinguish three(not necessarily distinct) cases. Either (1) π is positive andn ≤ n , (2) π is positive and n ≥ n , or (3) π is zero. We willrealize each of these cases by corresponding extended MMA
dag-formulas β1 (q, q  ), β2 (q, q  ), and β3 (q, q  ) respectively.
Let us consider case (1), i.e. π is positive and n ≤ n . Then n ≥ ∇(q, q  ) and n − n ∈ Δ>0↑ (q , q ) for some q ∈ Q
by Lemma 9. Thus, (n − n) ∈ a + bN for some arithmetic
 
progression a + bN ⊆ Δ>0↑ (q , q ). Furthermore, let c ∈Z/bZ be the residue class of n modulo b. So altogether, we
will fix the witnesses q  , a + bN, and c in the following.
Let us first assume that b > 0. We now distinguish thecases when there are either (i) infinitely or (ii) finitely manyn ∈ N such that n ≡ c mod b and (q  , n ) |= ϕj  .
Case (i) is expressed by the formula γ(q  , a, b, c)∞ which
is defined asinf(q  , j  , c, b) ∧ ≥ ∇(q, q  ) ∧ ≡ (c − a) mod b.
Case (ii) can be realized by saying that the maximal such n
is reachable from n via the arithmetic progression a + bN.
For this, let the formula γ(q  , a, b, c)<∞ be defined as the
conjunction of






¬ inf(q , j , c, b) ∧ ≥ ∇(q, q )andThe case when b = 0 can easily be realized by puttingγ(q  , a) = ≥ ∇(q, q  ) ∧ (α(q ,j  ) − a).
Altogether, we put
β1 (q, q  )γ(q  , a)=q  ∈Qγ(q  , a, b, c)∞ ∨ γ(q  , a, b, c)<∞ .

∨a+bN⊆Δ>0 (q,q  )↑b>0,c∈Z/bZ

Let us now consider case (2), i.e. when π is positive andn ≥ n . Then n ≥ ∇(q  , q  ) and n − n ∈ Δ>0↓ (q, q ) for
some q ∈ Q by Lemma 9. Hence, n − n ∈ a + bN for
some a + bN ⊆ Δ>0↓ (q, q ).
Firstly, let us assume that b > 0. Recall that c ∈ Z/bZ is theresidue class of n . Now the simple observation is that thewitness n can be replaced by the minimal n ∈ N such thatn ≡ n ≡ c mod b, n ≥ ∇(q  , q  ), and (q  , n ) |= ϕj  .
We realize this by the formula θ(q  , a, b, c) defined as the
conjunction of ≡ c + a mod b and ≥ min (≥ ∇(q , q ) ∧ α(q ,j  ) ∧ ≡ c mod b) + a .
Secondly, let us assume that b = 0. This case is realized by
the formulaθ(q  , a) = ≥ (∇(q  , q  ) + a) ∧ (α(q ,j  ) + a).
Altogether, we define β2 (q, q  ) to beθ(q  , a, b, c)q  ∈Q a+bN⊆Δ>0(q,q  )↓The last conjunct guarantees that n + a ≤ n , which isnecessary since we have to have that n ∈ n + a + bN.

∨

θ(q  , a).


a+0N⊆Δ>0↓ (q,q )b>0,c∈Z/bZ

Finally, let us consider case (3), i.e. when π is zero. For
each q  ∈ Q, define the predicate ∃m ∈ N : m ∈ Δ=0↑ (q , q ) ∧ (q , m) |= ϕj  .
In other words, case (3) can be rephrased as n ∈ Δ=0↓ (q, q )and π(q ) for some q ∈ Q by Lemma 8. Now check thatthe predicate π(q  ) can be expressed as

0 ≤ max(≡ a mod b∧α(q ,j  ) , t(q ,j  ) +L(q ,j  ) )a+bN⊆Δ=0 (q  ,q  )↑b>0

a = min((α(q ,j  ) − a) + a).

∨ 
a+0N⊆Δ=0↑ (q ,q )Define β3 (q, q  ) =q  ∈Q π(q) ∧ ρ(q  ), where ρ(q  ) is(≡ a mod b) ∨
a+bN⊆Δ=0↓ (q,q )≡ (c − a) mod b ∧ ≤ max(α(q ,j  ) − a, t(q ,j  ) ).


a+0N⊆Δ>0↑ (q,q )We finally put α(q,j) =(= a).


a+0N⊆Δ=0↓ (q,q )q  ∈Q β1 (q, q )∨β2 (q, q )∨β3 (q, q ).

This concludes the definition of α. It is straightforward to
see that α can be computed in time polynomially in |O|+|ϕ|.

By additionally applying Lemma 2, we obtain the following
theorem.
Theorem 10 From a given one-counter process O and agiven EF dag-formula ϕ, we can compute in polynomial
time for each control location q of O an MMA dag-formulaα(q) such that [[α(q)]] = {n ∈ N | (T (O), (q, n)) |= ϕ}.
By combining Theorem 10 with Proposition 3 we obtain thefollowing corollary.
Corollary 11 The following problem is in PNP :INPUT: A one-counter process O = (Q, δ0 , δ>0 ), a state(q, n) ∈ Q × N with n given in binary, and an EF dagformula ϕ.
QUESTION: (T (O), (q, n)) |= ϕ?
A more precise analysis our translation allows us to derive
the following polynomial time upper bound, when the onecounter process is fixed.
Theorem 12 For every fixed one-counter process O =(Q, δ0 , δ>0 ) the following problem is in P:
INPUT: A state (q, n) ∈ Q×N, where n is given in binary
and an EF dag-formula ϕ.
QUESTION: (T (O), (q, n)) |= ϕ?
VI. L OWER BOUNDS ON MODEL CHECKING
In this section we give two results concerning lower bounds
for EF model checking. We first prove a matching PNP lower
bound for model checking EF logic dag-formulas. Then we
prove a PNP[log] lower bound for model checking with afixed EF formula (in this case, tree or dag representations
make no difference). Both results hold even over one-counter
nets. First, we prove a PNP lower bound for the problem ofmodel checking EF logic dag-formulas. The problem wewill reduce from is the well-known PNP -complete problem
DSAT [17], which takes the following input: a sequenceof boolean formulas F1 , . . . , Fn with variables x1 , . . . , xn
and sets of variables Z1 , . . . , Zn such that the formula
Fi can take only variables from {x1 , . . . , xi−1 } and Zi .
The goal is to decide whether there exists an assignment
σ : {x1 , . . . , xn } → {0, 1} that sets xn to 1 such that thefollowing are satisfied for all i ∈ [n]:σ(xi ) = 1⇔∃Zi Fi (x1 , . . . , xi−1 , Zi ).

(1)

Notice that imposing the constraint in (1) ensures that there
exists a unique assignment σ. The only question is whether
this assignment satisfies σ(xn ) = 1.
Theorem 13 The problem of model checking EF logic dagformulas over one-counter nets is PNP -hard.

Proof Sketch.: The reduction is from DSAT. Givena sequence of boolean formulas F1 , . . . , Fn with variables
x1 , . . . , xn and sets Z1 , . . . , Zn of variables, we constructa one-counter net O and an EF dag-formula ϕ that mimic
the structure of the given sequence of formulas. By using
a well-known Gödel encoding technique that was also usedin [9, 11], we can view each natural m ∈ N as the truth
assigment αm : {x1 , . . . , xn } → {0, 1}, where αm (xi ) is
assigned to 1 if the i-th prime number pi divides m and0 otherwise. Checking divisibility by pi can be easily doneby looping through a cycle of length pi . Now, both O andϕ consist of n “levels”, where each level can refer only
to lower levels. Testing satisfiability of Fi is replaced bydivisibility tests and satisfiability of appropriate Fj s, wherej < i. Since a variable xi might be referred to several times
in the sequence F1 , . . . , Fn , we need to use EF dag-formulas
to avoid an exponential blowup.
We proceed to the model checking problem with theformula fixed. First, define the problem INDEX-ODD fromwhich our reduction is performed: given a list F1 , . . . , Fn ofboolean formulas in 3-CNF, does there exist an odd indexi ∈ [n] s.t. F1 , . . . , Fi are all satisfiable and Fi+1 , . . . , Fn
are all unsatisfiable? This problem is PNP[log] -complete. A
PNP[log] upper bound is immediate by a simple binary searchin the list F1 , . . . , Fn by invoking an NP oracle at eachstep to determine the rightmost satisfiable formula Fi . The
lower bound is also immediate from Wagner’s sufficientconditions for PNP[log] -hardness [27, Theorem 5.2] (see also[21, Lemma 7]). The reduction for the following theorem canbe achieved via Gödel encoding as in the proof of Theorem
13.
Theorem 14 There exists a fixed EF formula ϕ such thatmodel checking ϕ over one-counter nets is PNP[log] -hard.
It is worth observing that the above lower bounds imply
that the membership problem of MMA dag-formulas of fixednesting depth of both min and max operators is hard for
PNP[log] . The reason for this is that the min and max nesting
depth of the resulting MMA formula in the translation of
the previous section depends only on the size of the given
EF formula not on the size of the one-counter process.
On the other hand, our best upper bound of determining
only the parity of the minimal (resp. maximal up to somegiven threshold) natural number satisfying a given MMA
formula that is both min-free and max-free is PNP . Thisis basically the reason why we cannot improve the upperbound of EF over OCP when the formula is fixed.
VII. E QUIVALENCE CHECKING
In this section, we study the complexity of the w-bisimilarity
checking problem. We show that the general problem is PNP complete. We then proceed by showing that the problem issolvable in P for each fixed one-counter process. Finally, weshow that that there exists a fixed finite system for which thew-bisimilarity checking problem is already PNP[log] -hard.
We extend our EF logic with the following operator
EF τ ∗ , which we will also abbreviate as EF . The meaningis that for a transition system T = (S, {→a | a ∈ Σ}) and astate s ∈ S we have T, s |= EF ϕ if and only if there existss ∈ S such that s ⇒τ s and T, s |= ϕ. Note that our PNP
upper bound easily carries over to this extended EF logic bysimply restricting ourselves to τ -transitions when we haveEF operators. The following is a well-known result from[8] (and a more recent presentation can be found in [7]).
1Lemma 15 ([8]) Let T1 = (S1 , {→a | a ∈ Σ}) be a2transition system and T2 = (S2 , {→a | a ∈ Σ}) be a
finite transition system with k states. Then, given any states2 ∈ S2 , we can construct a dag-formula ϕs2 ,T2 in theextended EF logic in polynomial time (in k) such that, forevery state s1 ∈ S1 , it is the case that s1 ≈ s2 if and only
if (T1 , s1 ) |= ϕs2 ,T2 .
In other words, Lemma 15 implies that the w-bisimulation
checking problem is polynomial-time reducible to the problem of model checking extended EF dag-formulas. Combining this lemma with our results in the previous sections, thefollowing theorem can easily be derived.
Theorem 16 The w-bisimilarity checking problem is solvable in PNP . The problem becomes solvable in P when the
one-counter process is fixed.
We now consider the problem of computing a symbolic
representation of the w-bisimulation relation for the wbisimilarity checking problem, i.e., a function mapping eachstate t in the given finite system and each control location
q of the one-counter process to a representation of alln ∈ N such that (q, n) ≈ t. If we are allowed to represent
subsets of N as MMA formulas, it also follows that such
representations can be computed in polynomial time.
We now proceed to lower bounds. We can show thatw-bisimilarity checking is PNP -hard, even for one-counter
nets. Our result can be seen as a substantial improvement of
Kučera’s DP lower bound proof [11] for the w-bisimilarity
checking problem. (The complexity class DP is located in
the second level of the boolean hierarchy, which in turnis subsumed in PNP[log] ; see [17].) In the following, we
use a standard way of describing w-bisimulations using
simple pebble games between Attacker and Defender (e.g.
see [7, 15]). Such games are nothing but Ehrenfeucht-Fraı̈ssé
games for the extended EF logic in which Defender attempts
to show that two transition systems are w-bisimilar, while
Attacker tries to show otherwise.
Theorem 17 The problem of checking weak-bisimulation

between a given one-counter net and a given finite system
is hard for PNP .
Proof Sketch.: The proof of Theorem 17 uses similar
techniques as the proof of Theorem 13, but is substantiallymore involved. We reduce DSAT to the w-bisimulation
checking problem by constructing a suitable one-counter net
and a finite system. The finite system contains (among manyothers) states P1 and P2 , and the one-counter net contains
control locations qi for i ∈ [n] such that the following
statements are equivalent:• F1 , . . . , Fi ∈ DSAT.
• P1 ≈ (qi , l) for all l ∈ N.
• P2 is not w-bisimilar to (qi , l) for some l in N.
In the particular case of i = n, this is the reduction weare looking for. The idea is that checking the truth of every
subformula ∃Zi Fi (x1 , . . . , xi−1 , Zi ) of the DSAT problem
is encoded into a complex w-bisimulation game for P1 ≈(qi , l). In this game, the defender player gets to choose (byτa long ⇒ move) a natural number l which is stored in the
one-counter net. This number encodes (by Gödel encoding)the assignment of values to the boolean variables in the block
Zi . Later in the game, these values can be tested by special
counter-decreasing loops, which implement divisibility tests
on l . The variables xk are treated differently, because they
depend on other subformulae Fk with smaller index numbers
k < i. If the value of some xk (for k < i) needs to be tested,
then the w-bisimulation game jumps to some subgame whichtests either P1 ≈ (qk , l ) or P2 ≈ (qk , l ), depending onwhether the value of xk is claimed as true or false. Thisefficient way of re-using subgames for smaller indices k < ias building blocks corresponds to an efficient way of reusing sub-formulae in the dag-representation of EF-formulaein the proof of Theorem 13.
The main technical difficulty of the proof is to restrict
the freedom of the players in the w-bisimulation game, sothat they exactly make the choices needed in the verification
game for the formula ∃Zi Fi (x1 , . . . , xi−1 , Zi ) in the rightstep, and do not make a move that is reserved for the otherplayer. This is tricky, because of the asymmetry of the twocompared systems, one infinite-state one-counter process
and a finite system. In particular, isomorphic copies of thefinite system are replicated in the control locations of the
one-counter net.
In contrast to Kučera’s DP lower bound [11] which holds
for a fixed one-counter net, our proof of Theorem 17 requiresthat the finite system is not fixed. Nevertheless, we can showthat the w-bisimilarity checking problem for fixed finite
systems is harder than DP.
Theorem 18 There exists a fixed finite system for which thew-bisimilarity checking problem is hard for PNP[log] even for
one-counter nets.

Proof Sketch.: The proof is done by a reduction fromINDEX-ODD, which uses a construction from [11] as a
subroutine.

[9] P. Jančar, A. Kučera, F. Moller and Z. Sawa. DP Lowerbounds for equivalence-checking and model-checking of onecounter automata. Inf. Comput. 188(1): 1–19 (2004).

VIII. F UTURE WORK[10] P. Jančar and Z. Sawa. A note on emptiness for alternating
finite automata with a one-letter alphabet. IPL 104(5):164–
167 (2007).

As mentioned in the introduction, model checking the modal
μ-calculus over one-counter processes is in PSPACE by[20]. PSPACE-hardness can both be shown when fixing theone-counter process and when fixing the μ-calculus formula.
The latter follows quite immediately from PSPACE-hardnessof the emptiness problem for alternating finite automata overa unary alphabet [5, 10]. However, the precise complexity
for the temporal logic CTL, extending EF logic and being a
fragment of the modal μ-calculus, seems to be worth investigating, lying somewhere between PNP[log] and PSPACE.
Another interesting extension of EF-logic could be the firstorder logic FO(R) with reachability operator and its twovariable fragment. It was recently shown [26] that these
extensions are both PSPACE-complete. We would also liketo investigate the precise complexity of model checking
EF-logic over one-counter processes when formulas are
represented as trees (or additionally when they are fixed).
Our results imply that it is between PNP[log] and PNP . The
same complexity gap remains for weak bisimilarity of onecounter processes against fixed finite systems.
ACKNOWLEDGMENT
We thank Dietrich Kuske, Leonid Libkin, Markus Lohrey,
and Christian Mathissen for their comments.
R EFERENCES[1] A. Bouajjani, J. Esparza and O. Maler. Reachability analysis
of pushdown automata: application to model checking. In
CONCUR’97, pages 135–150.
[2] T. Cachat. Uniform Solution of Parity Games on PrefixRecognizable Graphs. ENTCS 86(6): (2002).
[3] M. Chrobak. Finite Automata and Unary Languages, Theor.
Comput. Sci. 47(3):149–158 (1986).
[4] J. Esparza, D. Hansel, P. Rossmanith and S. Schwoon. Efficient Algorithms for Model Checking Pushdown Systems. In
CAV’00, pages 232–247.
[5] M. Holzer. On emptiness and counting for alternating finite
automata. In DLT’95, pages 88-97.
[6] P. Jančar. Decidability of Bisimilarity for One-Counter
Processes. Inf. Comput. 158(1): 1–17 (2000).
[7] P. Jančar and A. Kučera. Equivalence Checking on InfiniteState Systems: Techniques and Results. TPLP 6(3):227–264(2006).
[8] P. Jančar, A. Kučera and R. Mayr. Deciding BisimulationLike Equivalences with Finite-State Processes. TCS 258(1–2):409–433 (2001).

[11] A. Kučera. Efficient Verification Algorithms for One-Counter
Processes. In ICALP’00, pages 317–328.
[12] A. Kučera and R. Mayr. On the Complexity of Semantic
Equivalences for Pushdown Automata and BPA. In MFCS’02,
pages 433-445.
[13] A. Martinez. Efficient computation of regular expressions
from unary NFAs. In DCFS’02, pages 216–230.
[14] R. Mayr. On the Complexity of Bisimulation Problems for
Pushdown Automata. In IFIP TCS’00, pages 474–488.
[15] R. Mayr. Undecidability of Weak Bisimulation Equivalence
for 1-counter Processes. In ICALP’03, pages 570–583.
[16] R. Milner. Communication and Concurrency. Prentice, 1989.
[17] C. H. Papadimitriou. Computational Complexity. AddisonWesley, 1994.
[18] N. Piterman and M. Y. Vardi. Global Model-Checking ofInfinite-State Systems. In CAV’04, pages 387–400.
[19] G. Sénizergues. The Bisimulation Problem for Equational
Graphs of Finite Out-Degree. SIAM J. Comput. 34(5):1025–
1106 (2005).
[20] O. Serre. Parity games played on transition graphs of onecounter processes. In FOSSACS’06, pages 337–351.
[21] H. Spakowski and J. Vogel. Θ2p -Completeness: A ClassicalApproach for New Results. In FSTTCS’00, pages 348–360.
[22] J. Srba. Undecidability of Weak Bisimilarity for Pushdown
Processes. In CONCUR’02, pages 579–593.
[23] J. Srba. Roadmap of Infinite results. Bulletin of the EATCS
78:163–175 (2002). http://www.brics.dk/˜srba/roadmap[24] J. Srba. Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation. In CSL’06, pages 89–
103.
[25] A. W. To. Unary finite automata vs. arithmetic progressions.
Tech. report EDI-INF-RR-1306, Univ. of Edinburgh, 2008.
[26] A. W. To. Model checking FO(R) over one-counter processes
and beyond. To appear in CSL’09.
[27] K. W. Wagner. More complicated questions about maxima
and minima, and some closures of NP. Theor. Comput. Sci.
51(1–2):53–80 (1978).
[28] I. Walukiewicz. Model checking CTL Properties of Pushdown
Systems. In FSTTCS’00, pages 127–138.
[29] I. Walukiewicz. Pushdown Processes: Games and ModelChecking. Inf. Comput. 164(2):234–263 (2001).