Internal Report  TCS-97-4

September, 1997

Message-Passing Automata and Asynchronous Communication

(Preliminary Version)

Madhavan Mukund^{1}

Jaikumar Radhakrishnan^{2} K Narayan Kumar^{1} Milind Sohoni^{3}

Abstract

This paper is a step towards developing a new automata-theoretic framework for describing distributed finite-state systems with asynchronous communication. If we assume that messages can be delayed arbitrarily in transit, it is reasonable to model the global behaviour of such systems in terms of finite-state automata equipped with blind counters—that is, counters which cannot be tested for zero.

We analyse the languages accepted by such automata and show that it is decidable whether the language of such an automaton is empty. We also develop a variety of pumping lemmas which can be used to show that certain languages are not accepted by these automata.

Our main result is that the subclass of languages accepted by these automata which is closed under complementation is precisely the class of regular languages. In the context of asynchronous protocols, our result implies that robust finite-state protocols use bounded buffers. In other words, messages are used only for handshaking—that is, for coordinating the interaction between different processes and the environment.

It is well known that automata with blind counters are closely related to Petri nets. However, our definition of languages is more appropriate for reasoning about asynchronous communication and is different from the definition used in the theory of Petri nets.

1SPIC Mathematical Institute, 92 G.N. Chetty Road, Madras 600 017, India. E-mail:

{madhavan,kumar}@smi.ernet.in

2Computer Science Group, Tata Institute of Fundamental Research, Homi Bhabha Road, Bombay 400 005, India. E-mail: jaikumar@tcs.tifr.res.in

3Dept of Computer Sc. and Engg., Indian Institute of Technology, Bombay 400 076, India. E-mail:

sohoni@cse.iitb.ernet.in

1 Introduction

Today, distributed systems which use asynchronous communication are ubiquitous—the Internet is a prime example. However, there has been very little work on studying the finite-state behaviour of such systems. In particular, this area lacks a satisfactory automata-theoretic framework. In contrast, automata theory for systems with synchronous communication is well developed via Zielonka’s asynchronous automata [Z87] and the connections to Mazurkiewicz trace theory [M78].

This paper is a step towards developing an automata-theoretic framework for describing distributed finite-state systems with asynchronous communication. Earlier attempts at defining such models of asynchronous systems deal primarily with infinite-state systems—for instance, the port automaton model of Panangaden and Stark [PS88] and the I/O automaton model of Lynch and Tuttle [LT87]. Also, earlier work has focussed on issues far removed from those which are traditionally considered in the study of finite-state systems.

The setting for our work is as follows. Consider a system in which a collection of finite-state machines communicate by sending messages via buffered channels. Suppose that there are only finitely many different kinds of messages. Messages may experience arbitrary delays in transit, though they always eventually reach their recipient. At an abstract level, Internet protocols such as the SMTP mail protocol fit into this paradigm. Another example is the protocol used in a banking network to exchange information between ATMs and the bank’s distributed databases.

Since messages may get reordered in transit, the state of such a system is completely described by the state of the components and the number of messages of each kind which have been sent but are as yet undelivered. Thus, at a global level, such systems can be treated as finite-state automata equipped with a finite number of counters, one for each type of message. The only operations permitted on the counters are increment and decrement (corresponding to sending and receiving the appropriate type of message respectively). The automaton cannot test if a counter’s value is zero—this restriction captures the intuition that it is not practical for a component to make a decision based on the assumption that another process has not sent a message, since messages may be delayed arbitrarily.

With this motivation, we define counter automata and study the languages they accept. Each move of a counter automaton consists of either reading a letter from the input or manipulating a counter. Reading from the input represents the interaction of the underlying distributed system with its environment. We study the languages (over the input alphabet) accepted by these automata.

Our main concern is when such a language is regular. An automaton which accepts a regular language represents a communication protocol whose interaction with the environment is regular. Such a protocol essentially uses only bounded buffers. Our main result is that a language L accepted by a counter automaton is regular if and only if the complement of L is also accepted by a counter automaton. In the context of asynchronous protocols, our result implies that robust finite-state protocols use only bounded buffers. In other words, messages are used only for hand-shaking, to coordinate the interaction between different processes and the environment. Along the way, we develop a variety of tools and techniques for reasoning about counter automata, including a number of pumping lemmas which are useful for showing when languages are not recognisable by counter automata.

The automata we consider are closely related to automata with blind counters, studied by Greibach [G78]. In turn, these automata are closely related to Petri nets [J86a, J86b]. Some of the techniques we develop are analogous to well-known results in Petri net theory, such as the covering tree construction of Karp and Miller [KM69]. However, our definition of languages is more appropriate for reasoning about asynchronous communication and is different from the definition used in Petri net theory. Towards the end of the paper, we discuss the connection between our framework and Petri net languages.

Recently, Abdulla and Jonsson have also studied decision problems for distributed systems with asynchronous communication [AJ93, AJ94]. However, they work in a setting where messages are delivered in the order in which they are sent. This means that the channels are unbounded, fifo buffers. With such a strong model, most interesting questions become undecidable. The results of [AJ93] show that the fifo model can be made tractable by assuming that messages may be lost in transit. With lossy channels, questions such as reachability of configurations and equivalence with respect to finite-state automata can be decided, though certain other questions remain undecidable [AJ94]. While their results are incomparable with ours, since the two models are orthogonal, we remark that all their positive results hold for our model as well.

The paper is organised as follows. In the next section we define counter automata and prove some basic results about them. In Section 3 we prove a Contraction Lemma which leads to decidability of the emptiness problem and the fact that the languages accepted by counter automata are not closed under complementation. Section 4 develops a family of pumping lemmas which are exploited in Section 5 to prove our main result concerning the regularity of languages accepted by counter automata. In the final section, we discuss in detail the connection between our results and those in Petri net theory and point out directions for future work.

2 Counter Automata

Natural numbers and tuples As usual, ℕ denotes the set {0, 1, 2, …} of natural numbers. If i, j ∈ ℕ, [i..j] denotes the set {i, i+1, …, j} with the convention that [i..j] = ∅ if i > j. We compare k-tuples of natural numbers component-wise: let \overline{m} = ⟨m_{1}, m_{2}, …, m_{k}⟩ and \overline{n} = ⟨n_{1}, n_{2}, …, n_{k}⟩ be k-tuples of natural numbers. Then \overline{m} ≤ \overline{n} iff m_{i} ≤ n_{i} for each i ∈ [1..k].

Counter automata A counter automaton A is a tuple (Q, Σ, Γ, T, q_{in}, F), where:

• Q is a finite set of states, with initial state q_{in} and accepting states F ⊆ Q.

• Σ is a finite input alphabet.

• Γ is a finite set of counters. We use C, C′, … to denote counters. With each counter C, we associate two symbols, C^{+} and C^{−}. We write Γ^{+} for the set {C^{+}|C ∈ Γ}, Γ^{−} for {C^{−}|C ∈ Γ} and Γ^{±} for Γ^{+} ∪ Γ^{−}.

• T ⊆ Q × (Σ ∪ Γ^{±}) × Q is the transition relation.

Configurations A configuration of A is a pair (q, f) where q ∈ Q and f : Γ → ℕ is a function which records the values stored in the counters. If the counters are C_{1}, C_{2}, …, C_{k} then we represent f by an element ⟨f(C_{1}), f(C_{2}), …, f(C_{k})⟩ of ℕ^{k}. By abuse of notation, the k-tuple ⟨0, 0, …, 0⟩, representing the function which assigns 0 to all counters, is uniformly denoted \overline{0}, for all values of k.

The function f dominates the function f′, written f ≥ f′, if f(C) ≥ f′(C) for every counter C. The function f strictly dominates the function f′, written f > f′, if f ≥ f′ and there is a counter C such that f(C) > f′(C).

We use χ to denote configurations. If χ = (q, f), Q(χ) denotes q and F (χ) denotes f. Further, for each counter C, C(χ) denotes the value f(C).

Moves The automaton moves from configuration χ to configuration χ′ on d ∈ Σ ∪ Γ^{±} if (Q(χ), d, Q(χ′)) ∈ T and one of the following holds:

• d ∈ Σ and F (χ) = F (χ′).

• d = C^{+}, C(χ′) = C(χ) + 1 and C′(χ) = C′(χ′) for every C′ ≠ C.

• d = C^{−}, C(χ′) = C(χ) − 1 ≥ 0 and C′(χ) = C′(χ′) for every C′ ≠ C.

Such a move is denoted χ ⟶^{(q,d,q′)} χ′—in other words, transitions are labelled by elements of T rather than elements of Σ ∪ Γ^{±}. Given a sequence of transitions t_{1}t_{2} … t_{n} = (q_{1}, d_{1}, q_{2})(q_{2}, d_{2}, q_{3}) … (q_{n}, d_{n}, q_{n+1}), the corresponding sequence of letters d_{1}d_{2} … d_{n} from Σ ∪ Γ^{±} is denoted α(t_{1}t_{2} … t_{n}).

Computations, runs and languages A computation of A is a sequence χ_{0} ⟶^{t_{1}} χ_{1} ⟶^{t_{2}} … ⟶^{t_{n}} χ_{n}. We also write χ_{0} ⟹^{t_{1}t_{2}...t_{n}} χ_{n} to indicate that there is a computation labelled t_{1}t_{2} … t_{n} from χ_{0} to χ_{n}. Notice that χ_{0} and t_{1}t_{2} … t_{n} uniquely determine all the intermediate configurations χ_{1}, χ_{2}, …, χ_{n}. If the transition sequence is not relevant, we just write χ_{0} ⟹ χ_{n}. As usual, χ ⟹^{t_{1}t_{2}...t_{n}} denotes that there exists χ′ such that χ ⟹^{t_{1}t_{2}...t_{n}} χ′ and χ ⟹ denotes that there exists χ′ such that χ ⟹ χ′.

For K ∈ ℕ, a K-run of A is a computation χ_{0} ⟹ χ_{n} where C(χ_{0}) ≤ K for each C ∈ Γ.

If δ is a string over Σ ∪ Γ^{±}, δ↾_{Σ} denotes the subsequence of letters from Σ in δ. Let w = a_{1}a_{2} … a_{k} be a string over Σ. A run of A over w is a 0-run χ_{0} ⟹^{t_{1}t_{2}...t_{n}} χ_{n} where Q(χ_{0}) = q_{in} and α(t_{1}t_{2} … t_{n})↾_{Σ} = w. The run is said to be accepting if Q(χ_{n}) ∈ F. The string w is accepted by A if A has an accepting run over w. The language accepted by A, denoted L(A), is the set of all strings over Σ accepted by A.

A language over Σ is said to be counter recognisable if there is a counter automaton with input alphabet Σ that accepts this language.

Example 2.1 Let L_{ge} ⊆ {a, b}^{∗} be given by {a^{m}b^{n} | m ≥ n}. This language is counter recognisable. Here is an automaton for L_{ge}. The initial state is indicated by ⇓ and the final states have an extra circle around them.

a C^{+}  b  C^{−} b ⇓

2.1 Non-determinism versus determinism

Deterministic Counter Automata A counter automaton A = (Q, Σ, Γ, T, q_{in}, F) is said to be deterministic if the following two conditions hold:

• If (q, d_{1}, q_{1}), (q, d_{2}, q_{2}) ∈ T, with d_{1}, d_{2} ∈ Σ, then d_{1} = d_{2} implies q_{1} = q_{2}.

• If (q, d_{1}, q_{1}), (q, d_{2}, q_{2}) ∈ T, with d_{1} ∈ Γ^{±}, then d_{1} = d_{2} and q_{1} = q_{2}.

Though this notion of determinism seems rather strong, it is easy to see that any relaxation of the definition will allow deterministic automata to simulate non-deterministic automata in a trivial manner.

For instance, suppose we naïvely define a deterministic automaton to be one in which no state has two outgoing transitions with the same label. This definition would permit a deterministic automaton to choose between a counter move and another transition (which may or may not be a counter move). We can then simulate a choice between two transitions t_{1} = (q, d, q_{1}) and t_{2} = (q, d, q_{2}) with the same label by adding a dummy counter C. Instead of choosing directly between t_{1} and t_{2}, the new automaton will first choose between t_{1} and a move (q, C^{+}, q′) leading to a new state q′. We can then simulate t_{2} by adding a transition (q′, d, q_{2}). Thus, the original choice between t_{1} and t_{2} is replaced by a cascaded choice involving the dummy counter C.

It is interesting to observe that a similar strong definition of determinism is used in the study of Petri net languages [J86a].

We have the following characterisation of languages accepted by deterministic counter automata.

Proposition 2.2 Let A be a deterministic counter automaton. Then, either L(A) is regular or there exists a word w ∉ L(A) such that every extension of w also does not belong to L(A).

Proof: Let A be a deterministic counter automaton. For each input word w, either A admits no run over w or it admits a unique sequence of runs ρ_{1}, ρ_{2}, …, (which may be infinite) over w such that for each i ≥ 1, ρ_{i+1} extends ρ_{i} by one transition involving a counter operation.

A word w is said to be blocked in the automaton A if A does not permit an infinite sequence of runs ρ_{1}, ρ_{2}, …, over w. If w is blocked, there exists a unique state where A “gets stuck” when processing w. We denote this state q_{w}.

Since A is deterministic, we know that if q_{w} has any outgoing transitions, either the set of outgoing transitions at q_{w} is labelled by distinct letters from Σ or there is only a single outgoing transition labelled by an element of Γ^{±}. In the latter case, it must be that the transition is labelled C^{−}, for some C ∈ Γ, because a move labelled C^{+} is always enabled. We say that w is Γ-blocked in A if w is blocked in A and q_{w} has an outgoing transition labelled C^{−}, for some C ∈ Γ.

Returning to the statement to be proved, if L(A) = Σ^{∗}, then L(A) is regular. Thus, the interesting case is when \overline{L(A)} = Σ^{∗} \ L(A) is non-empty.

Case 1: If there exists w in Σ^{∗} \ L(A) which is Γ-blocked, then any extension of w must also be Γ-blocked. Thus all extensions of w also lie outside L(A).

Case 2: Suppose that no word w in \overline{L(A)} is Γ-blocked. Then, from A we can construct a finite-state automaton A′ over the alphabet Σ which has ε-transitions. The automaton A′ has the same set of states, initial state and final states as A. For each transition t of the form (q, d, q′) in A, we have a corresponding transition t′ = (q, d′, q′) in A′, where d′ = d if d ∈ Σ and d′ = ε if d ∈ Γ^{±}.

Since A is deterministic, at each state of A′ which has outgoing transitions, either the set of outgoing transitions is labelled by distinct letters from Σ or there is a single outgoing transition labelled ε. In other words, for every word w, either A′ does not admit a run over w or A′ admits a unique sequence of runs ρ_{1}, ρ_{2}, …, over w such that for each i ≥ 1, ρ_{i+1} extends ρ_{i} by a transition labelled ε.

We claim that L(A′) = L(A) and hence L(A) is regular. It is easy to see that

each computation χ_{0} ⟶^{t_{1}} χ_{1} ⟶^{t_{2}} ⋯ ⟶^{t_{n}} χ_{n} of A can be simulated by a run Q(χ_{0}) ⟶^{t′_{1}}

Q(χ_{1}) ⟶^{t′_{2}} ⋯ ⟶^{t′_{n}} Q(χ_{n}) of A′, where for each i ∈ [1..n], t′_{i} is the transition corresponding to t_{i} as described above. Since the initial and final states of A′ are the same as those of A, it follows that L(A) ⊆ L(A′).

To see that L(A′) ⊆ L(A), assume that there is a word w ∈ L(A′) \ L(A). Then, A′

admits an accepting run ρ′ : q_{in} ⟶^{t′_{1}} q_{1} ⟶^{t′_{2}} ⋯ ⟶^{t′_{n}} q_{n} over w, with q_{n} a final state. From

our construction of A′, it follows that there is a maximal prefix σ′ : q_{in} ⟶^{t′_{1}} q_{1} ⟶^{t′_{2}} ⋯ ⟶^{t′_{k}} q_{k} of ρ′, with k < n, such that A admits a 0-run σ : χ_{0} ⟶^{t_{1}} χ_{1} ⟶^{t_{2}} ⋯ ⟶^{t_{k}} χ_{k} over w with the following properties:

• Q(χ_{0}) = q_{in}.

• For each i ∈ [1..k], Q(χ_{i}) = q_{i} and t′_{i} is the transition corresponding to t_{i} as specified in the construction of A′.

• w is blocked in A and q_{w} = q_{k}.

Since σ cannot be extended in A while σ′ can be extended in A′, it must be the case that t_{k+1} corresponds to a move of the form C^{−} for a counter C whose value at χ_{k} is 0. This implies that w is Γ-blocked in A, which is a contradiction.

Hence, L(A′) = L(A) and L(A) is regular.

□

Corollary 2.3 Non-deterministic counter automata are strictly more powerful than deterministic counter automata.

Proof: Consider the language L ⊆ {a, b}^{∗} given by

L = {w | w = w_{1}a^{m}b^{n}aw_{2}, where w_{1}, w_{2} ∈ {a, b}^{∗} and m ≥ n ≥ 1}.

It is not difficult to transform the automaton which accepts L_{ge} = {a^{m}b^{n} | m ≥ n} into a non-deterministic counter automaton which accepts L. We argue that L cannot be accepted by any deterministic counter automaton. L is clearly not regular. Thus, by the previous proposition, for L to be accepted by a deterministic automaton, it must be the case that there is a word w ∉ L such that every suffix of w is also not in L. However, for any word w ∉ L, we can always find an extension of w in L—for instance, waba ∈ L for all w ∈ {a, b}^{∗}. □

Observe, however, that even deterministic counter automata are strictly more powerful than normal finite-state automata. For instance, the language L_{ge} of Example 2.1 is not regular but the automaton accepting the language is deterministic.

2.2 Some useful results

The following observations are basic to analysing the behaviour of counter automata. We first need the following terminology: a sequence \overline{n}_{1}, \overline{n}_{2}, … of k-tuples of natural numbers is said to be non-decreasing if \overline{n}_{1} ≤ \overline{n}_{2} ≤ · · ·.

Proposition 2.4 Every infinite sequence of k-tuples of natural numbers has an infinite non-decreasing subsequence.

Proof: The proof is by induction on k.

Basis: When k = 1, we have a sequence of natural numbers. If the sequence is bounded then some value appears infinitely often (by the pigeon-hole principle). On the other hand, if the sequence is unbounded, it is obvious that it contains a strictly increasing infinite subsequence.

Induction step: If we project the sequence of k-tuples onto its first k−1 components, we can apply the induction hypothesis to extract an infinite subsequence which is nondecreasing in these k−1 coordinates. We look at the corresponding subsequence in our original sequence of k-tuples and examine the kth coordinate of each element in the sequence. By an argument similar to the basis case, there must be an infinite subsequence which is non-decreasing on the kth coordinate as well.

□

Corollary 2.5 There is no infinite set of k-tuples of natural numbers that is pairwise incomparable.

Lemma 2.6 Let T be a finitely branching infinite tree whose nodes are labelled by k-tuples from ℕ. For each i ∈ ℕ there is a number μ_{i} such that along any path of length μ_{i} starting at the root of T, the corresponding sequence of labels n_{1}, n_{2}, …, n_{μ_{i}} has a nondecreasing subsequence of length i.

Proof: Suppose there exists i ∈ ℕ for which there is no such μ_{i}. In other words, for each j ∈ ℕ there is a path of length j starting at the root whose labels n_{1}, n_{2}, …, n_{j} do not contain a non-decreasing subsequence of length i.

Call a node t in T bad if the labels along the unique path from the root to t do not have a non-decreasing subsequence of length i. Clearly the parent of a bad node is also bad. Thus the set of bad nodes forms a subtree of T. By our assumption that there is no μ_{i} corresponding to i, there must be bad nodes at each level in the tree. Hence the set of bad nodes forms an infinite subtree of T.

By König’s Lemma there is an infinite path in T all of whose nodes are bad. The labels along this path do not have any non-decreasing subsequence of length greater than or equal to i. This contradicts Proposition 2.4. □

Lemma 2.7 Let A be a counter automaton with M states and N counters and let K ∈ ℕ. Then, there exists ℓ ∈ ℕ, such that for any K-run χ_{0} ⟶^{t_{1}} χ_{1} … ⟶^{t_{ℓ}} χ_{ℓ} of A, there are two configurations χ_{i} and χ_{j}, 0 ≤ i < j ≤ ℓ, such that Q(χ_{i}) = Q(χ_{j}) and F (χ_{i}) ≤ F (χ_{j}).

Proof: Construct a tree T whose nodes are labelled by ℕ^{N} as follows.

• The root x_{0} is labelled ⟨\overline{0}⟩.

• For each vector \overline{v} = ⟨m, \overline{n}⟩ where m ∈ [1..M] and \overline{n}(i) ≤ K for all i ∈ [1..N], construct a child x_{0}^{v} of the root labelled by \overline{n}.

• Let x be a node labelled ⟨m, \overline{n}⟩. For each vector v = ⟨m′, \overline{n}′⟩ where m′ ∈ [1..M] and \overline{n}′ differs from \overline{n} in at most one coordinate by at most 1, construct a child x^{v} of x labelled v.

Clearly, T is a finitely branching tree. Hence, by Lemma 2.6, for each natural number p there is a number μ_{p} such that, if x_{0}x_{1} … x_{p} ⟶^{t_{1}} χ_{1} ⟶^{t_{2}} ⋯ ⟶^{t_{μp}} χ_{μ_{p}} is a K-run of A then the sequence F (χ_{0}), F (χ_{1}), …, F (χ_{μ_{p}}) has a non-decreasing subsequence of length p.

Thus, if χ_{0} ⟹ χ_{μ_{M+1}} is any run of A, then there are positions 0 ≤ k_{1} < k_{2} < … < k_{M+1} ≤ μ_{M+1} such that F (χ_{k_{1}}) ≤ F (χ_{k_{2}}) … ≤ F (χ_{k_{M+1}}). By the pigeon-hole principle, there are positions k_{r} and k_{s}, 1 ≤ r < s ≤ M+1, such that Q(χ_{k_{r}}) = Q(χ_{k_{s}}). To prove the lemma, set ℓ = μ_{M+1}, χ_{i} = χ_{k_{r}} and χ_{j} = χ_{k_{s}}.

□

Weak pumping constant Notice that the bound ℓ established in the preceding lemma depends only on the values M, N and K and is independent of the actual structure of the automaton. Let π_{M,N,K} denote the bound ℓ. We refer to π_{M,N,K} as the weak pumping constant for (M, N, K). It is easy to see that if ⟨M′, N′, K⟩ ≤ ⟨M, N, K⟩, then π_{M′,N′,K′} ≤ π_{M,N,K}.

3 A Contraction Lemma

Lemma 3.1 (Contraction) For every counter automaton A, there is a constant k such that if χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} is a computation of A, with m > k, then there exist i and j,

m−k ≤ i < j ≤ m, such that χ′_{0} ⟹^{t_{1}...t_{i}t_{j+1}...t_{m}} χ′_{m−(j−i)} is also a computation of A, with

with χ′_{ℓ} = χ_{ℓ} for ℓ ∈ [0..i] and Q(χ_{ℓ}) = Q(χ′_{ℓ−(j−i)}) for all ℓ ∈ [j..m].

Proof: Let A have M states and N counters. We show that k can be chosen to be π_{M,N,0}.

Let χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} be a computation of A, with m > π_{M,N,0}. We define a sequence f_{m}, f_{m−1}, …, f_{0} of N-tuples of natural numbers as follows:

f_{m}(n) = 0, for all n ∈ [1..N]
For i ∈ [0..m−1], f_{i}(n) = \{ \begin{matrix}f_{i+1}(n) & if α(t_{i+1}) ∉ \{C_{n}^{+}, C_{n}^{−}\} \\ f_{i+1}(n)+1 & if α(t_{i+1}) = C_{n}^{−} \\ max(0, f_{i+1}(n)−1) & if α(t_{i+1}) = C_{n}^{+} \end{matrix}

We next show that the function f_{i} represents the minimum counter values required to execute the transition sequence t_{i+1}t_{i+2} … t_{m}.

Claim: ∀i ∈ [1..m], (Q(χ_{i}), f) ⟹^{t_{i+1}t_{i+2}...t_{m}} iff f ≥ f_{i}.

Proof of Claim: By induction on m−i.

Basis: If i = m there is nothing to prove.

Induction step:

By the induction hypothesis, (Q(χ_{i+1}), f′) ⟹^{t_{i+2}t_{i+3}...t_{m}} iff f′ ≥ f_{i+1}.

Suppose that f ≥ f_{i}. We have to show that (Q(χ_{i}), f) ⟹^{t_{i+1}t_{i+2}...t_{m}}. We first argue that there is a move (Q(χ_{i}), f) ⟶^{t_{i+1}} (Q(χ_{i+1}), f′). Since we know that (Q(χ_{i}), t_{i+1}, Q(χ_{i+1})) is a transition of A, the only reason for forbidding such a move is that α(t_{i+1}) = C_{n}^{−} for some counter C_{n} and f(n) = 0. However, if α(t_{i+1}) = C_{n}^{−}, we know that f_{i}(n) = f_{i+1}(n) + 1 ≥ 1. Since f ≥ f_{i}, f(n) ≥ 1 as well.

Consider the function f′. We shall show that f′ ≥ f_{i+1}. From the induction hypothesis, it then follows that (Q(χ_{i}), f) ⟶^{t_{i+1}} (Q(χ_{i+1}), f′) ⟹^{t_{i+2}t_{i+3}...t_{m}},

whereby (Q(χ_{i}), f) ⟹^{t_{i+1}t_{i+2}...t_{m}}.

To check that f′ ≥ f_{i+1}, we consider all possible values for α(t_{i+1}).

(i) α(t_{i+1}) ∈ Σ: Then f′ = f ≥ f_{i} = f_{i+1}.

(ii) α(t_{i+1}) ∈ {C_{n}^{−}, C_{n}^{+}}: Then

• For ℓ ≠ n, f′(ℓ) = f(ℓ) ≥ f_{i}(ℓ) = f_{i+1}(ℓ).

• If α(t_{i+1}) = C_{n}^{−}, then f′(n) = f(n) − 1 ≥ f_{i}(n) − 1 = f_{i+1}(n).

• If α(t_{i+1}) = C_{n}^{+}, then f′(n) = f(n)+1 ≥ f_{i}(n)+1 = max(1, f_{i+1}(n)) ≥ f_{i+1}(n).

Thus, for each ℓ ∈ [1..n], f′(ℓ) ≥ f_{i+1}(ℓ).

Conversely, suppose that (Q(χ_{i}), f) ⟹^{t_{i+1}t_{i+2}...t_{m}}. We have to establish that

f ≥ f_{i}. We know that (Q(χ_{i}), f) ⟶^{t_{i+1}} (Q(χ_{i+1}), f′) ⟹^{t_{i+2}t_{i+3}...t_{m}} and, by the

induction hypothesis, f′ ≥ f_{i+1}. As before, we examine all possible values of α(t_{i+1}).

(i) α(t_{i+1}) ∈ Σ: Then f = f′ ≥ f_{i+1} = f_{i}.

(ii) α(t_{i+1}) ∈ {C_{n}^{−}, C_{n}^{+}}: Then

• For ℓ ≠ n, f(ℓ) = f′(ℓ) ≥ f_{i+1}(ℓ) = f_{i}(ℓ).
• If α(t_{i+1}) = C_{n}^{−}, then f(n) = f′(n) + 1 ≥ f_{i+1}(n) + 1 = f_{i}(n).
• If α(t_{i+1}) = C_{n}^{+}, then f(n) = f′(n)−1 ≥ f_{i+1}(n)−1. Since f(n) ≥ 0
and f_{i}(n) = max(0, f_{i+1}(n) − 1), f(n) ≥ f_{i}(n).
Thus, for each ℓ ∈ [1..n], f(ℓ) ≥ f_{i}(ℓ).

Corollary to Claim: For each counter C_{n} and for each position i ∈ [1..m], C_{n}(χ_{i}) ≥ f_{i}(n).

Consider the sequence f_{m}, f_{m−1}, … f_{0}. Since its length exceeds π_{M,N,0}, by Lemma 2.7 there exist positions i and j, m ≥ j > i ≥ m−π_{M,N,0} such that f_{j} ≤ f_{i} and Q(χ_{j}) = Q(χ_{i}). By the Corollary to Claim, for each counter C_{n}, C_{n}(χ_{i}) ≥ f_{i}(n) ≥ f_{j}(n). Thus,

χ_{i} ⟹^{t_{j+1}t_{j+2}...t_{m}} whereby χ_{0} ⟹^{t_{1}t_{2}...t_{i}} χ_{i} ⟹^{t_{j+1}t_{j+2}...t_{m}} χ′_{m−(j−i)} is a valid computation of A for some

configuration χ′_{m−(j−i)}. Since Q(χ_{j}) = Q(χ_{i}) and the computations χ_{j} ⟹^{t_{j+1}t_{j+2}...t_{m}} χ_{m} and

χ_{i} ⟹^{t_{j+1}t_{j+2}...t_{m}} χ′_{m−(j−i)} are labelled by the same sequence of transitions, it follows that Q(χ_{ℓ}) = Q(χ′_{ℓ−(j−i)}) for each ℓ ∈ [j..m], as required.

□

Corollary 3.2 A counter automaton A with M states and N counters has an accepting computation iff it has an accepting computation whose length is bounded by π_{M,N,0}.

In the Appendix, we give a constructive proof of Lemma 2.7 which provides an explicit upper bound for π_{M,N,K} for all values of M, N, and K. This fact, coupled with the preceding observation, yields the following result.

Corollary 3.3 The emptiness problem for counter automata is decidable.

We remark, however, that a result of Lipton [L76] from the theory of Petri net languages implies that the emptiness problem for counter recognisable languages is EXPSPACEhard.

Corollary 3.4 Counter recognisable languages are not closed under complementation.

Proof: We saw earlier that L_{ge} = {a^{m}b^{n} | m ≥ n} is counter recognisable. Let A be an automaton which accepts L_{ge}. We can easily extend A to accept L′_{ge} = L_{ge} ∪ {w | w is not of the form a^{m}b^{n}}. The complement of the language L′_{ge} is the language L_{lt} = {a^{m}b^{n} | m < n}.

Suppose that L_{lt} were counter recognisable. Let A_{lt} be an automaton which accepts L_{lt}. Let M be the number of states in A_{lt} and N the number of counters used by A_{lt}. Consider the string w = a^{J}b^{J+1} where J = π_{M,N,0} and let ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{n}} χ_{n} be an accepting run of A_{lt} on w. By applying the Contraction Lemma (repeatedly, if necessary) to ρ, we can obtain an accepting run ρ′ of A_{lt} over a word of the form a^{J}b^{K}, where K ≤ J, thus contradicting the assumption that L(A_{lt}) = L_{lt}. (The reason we may need to use the Contraction Lemma more than once to obtain a suitable ρ′ is that when we apply the Lemma once, the sequence of moves deleted may fail to contain any transition labelled b. However, if this happens, the resulting run will continue to have a suffix containing π_{M,N,0} + 1 moves labelled b, so we can apply the Contraction Lemma repeatedly until at least one transition labelled b is deleted.) □

4 A Collection of Pumping Lemmas

Change vectors For a string w over a set X and a symbol x ∈ X, #_{x}(w) denotes the number of times x occurs in w. Let v be a sequence of transitions. Recall that α(v) denotes the corresponding sequence of letters. For each counter C, define Δ_{C}(v) to be #_{C^{+}}(α(v)) − #_{C^{−}}(α(v)). The change vector associated with v, denoted Δv, is given by ⟨Δ_{C}(v)⟩_{C∈Γ}.

Proposition 4.1 Let A = (Q, Σ, Γ, T, q_{in}, F) be a counter automaton.

(i) For any computation χ ⟹^{v} χ′ of A and any counter C ∈ Γ, |Δ_{C}(v)| ≤ |v|.

(ii) For any configuration χ and sequence of transitions v, χ ⟹^{v} iff for each prefix u of v and each counter C ∈ Γ, C(χ) + Δ_{C}(u) ≥ 0.

(iii) Let χ ⟹^{u} χ′ ⟹^{v} with Q(χ) = Q(χ′) and n ∈ ℕ such that, for every counter C ∈ Γ, either Δ_{C}(u) ≥ 0 or C(χ) ≥ n|u| + |v|. Then, χ ⟹^{u^{n}v}.

Proof:

(i) This follows from the fact that each move can change a counter value by at most 1.

(ii) This follows immediately from the definition of a computation.

(iii) The proof is by induction on n.

Basis: For n = 0, there is nothing to prove.

Induction step: Let n > 0 and assume the result holds for n−1. We will show that

χ ⟹^{u} χ′ ⟹^{u^{n−1}v}.

From the assumption, we know that χ ⟹^{u} χ′. To show that χ′ ⟹^{u^{n−1}v}, we examine the value of each counter C at χ′. If Δ_{C}(u) < 0, then C(χ) ≥ n|u| + v. Since C(χ′) = C(χ′) + Δ_{C}(u) and |Δ_{C}(u)| ≤ |u|, it follows that C(χ′) ≥ (n−1)|u| + v. From the induction hypothesis, we can then conclude that χ′ ⟹^{u^{n−1}v}.

□

Pumpable decomposition Let A be a counter automaton with N counters and let

ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} be a computation of A. A decomposition χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} χ_{i_{2}} ⟹^{v_{2}}

χ_{j_{2}} ⟹^{u_{3}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}} χ_{m} of ρ is said to be pumpable if it satisfies the following conditions:

(i) n ≤ N. (ii) For each k ∈ [1..n], Q(χ_{i_{k}}) = Q(χ_{j_{k}}). (iii) For each v_{k}, k ∈ [1..n], Δv_{k} is non-zero and has at least one positive entry. (iv) Let C be a counter and k ∈ [1..n] such that Δ_{C}(v_{k}) is negative. Then, there exists

ℓ < k such that Δ_{C}(v_{ℓ}) is positive. We refer to v_{1}, v_{2}, …, v_{n} as the pumpable blocks of the decomposition. If C is a counter such that Δ_{C}(v_{i}) > 0 for some pumpable block v_{i}, we say that C is a pumpable counter. Proposition 4.2 Let A be a counter automaton and ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} be a computation

of A. Consider a pumpable decomposition χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}}

χ_{m} of ρ. Then, for r ∈ [1..n], χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} ⋯ ⟹^{u_{r}} χ_{i_{r}} ⟹^{v_{r}} χ_{j_{r}} ⟹^{u_{r+1}} χ_{i_{r+1}} is a

pumpable decomposition of ρ_{r} : χ_{0} ⟹^{u_{1}v_{1}...u_{r}v_{r}u_{r+1}} χ_{i_{r+1}}.

Proof: Immediate, from the definition of pumpable decompositions. □

Lemma 4.3 (Counter Pumping) Let A be an automaton and ρ a K-run of A, K ∈ ℕ, with a pumpable decomposition of the form

χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} χ_{i_{2}} ⟹^{v_{2}} χ_{j_{2}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}} χ_{m}.

Then, for any I, J ∈ ℕ, with I ≥ 1, there exist ℓ_{1}, ℓ_{2}, …, ℓ_{n} ∈ ℕ and a K-run ρ′ of A of the form

χ′_{0} ⟹^{u_{1}} χ′_{i′_{1}} ⟹^{v_{1}^{ℓ_{1}}} χ′_{j′_{1}} ⟹^{u_{2}} χ′_{i′_{2}} ⟹^{v_{2}^{ℓ_{2}}} χ′_{j′_{2}} ⋯ ⟹^{u_{n}} χ′_{i′_{n}} ⟹^{v_{n}^{ℓn}} χ′_{j′_{n}} ⟹^{u_{n+1}} χ′_{p}

such that ρ′ satisfies the following properties:

(i) χ_{0} = χ′_{0}. (ii) Q(χ′_{p}) = Q(χ_{m}). (iii) For i ∈ [1..n], ℓ_{i} ≥ I. (iv) For every counter C, C(χ′_{p}) ≥ C(χ_{m}).

(v) Let Γ_{pos} be the set of pumpable counters in the pumpable decomposition of ρ. For each counter C ∈ Γ_{pos}, C(χ′_{p}) ≥ J.

Proof: The proof is by induction on n, the number of pumpable blocks in the decomposition.

Basis: If n = 0, there is nothing to prove.

Induction step: Let n > 0 and assume the lemma holds for all decompositions with n−1 pumpable blocks. For each counter C, let J_{C} = max(J, C(χ_{m})).

By the induction hypothesis, for all I′, J′ ∈ ℕ, I′ ≥ 1, we can transform the prefix

σ : χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} ⋯ ⟹^{v_{n−1}} χ_{j_{n−1}} ⟹^{u_{n}} χ_{i_{n}} of ρ into a K-run σ′ : χ′_{0} ⟹^{u_{1}} χ′_{i′_{1}} ⟹^{v_{1}^{ℓ_{1}}}

χ′_{j′_{1}} ⟹^{u_{2}} ⋯ ⟹^{v_{n−1}^{ℓ_{n−1}}} χ′_{j′_{n−1}} ⟹^{u_{n}} χ′_{i′_{n}} satisfying the conditions of the lemma. We shall choose I′ and J′ so that the transition sequence v_{n}^{ℓ_{n}}u_{n+1} can be appended to σ′ to yield the run claimed by the lemma.

To fix values for I′ and J′, we first estimate the value of ℓ_{n}, the number of times we need to pump v_{n} to satisfy all the conditions of the lemma. Let Γ_{pos}^{n} = {C | Δ_{C}(v_{n}) > 0}. It is sufficient if the number ℓ_{n} is large enough for each counter C ∈ Γ_{pos}^{n} to exceed J_{C} at the end of the new computation. For a counter C ∈ Γ_{pos}^{n} to be above J_{C} at the end of the computation, it is sufficient for C to have the value J_{C} + |u_{n+1}| after v_{n}^{ℓ_{n}}. By the induction hypothesis, the value of C before v_{n}^{ℓ_{n}} is at least C(χ_{i_{n}}). Hence, it would take ⌈\frac{J_{C}+|u_{n+1}|−C(χ_{in})}{Δ_{C}(v_{n})}⌉ iterations of v_{n} for C to reach the required value after v_{n}^{ℓ_{n}}. On the other hand, we should also ensure that ℓ_{n} ≥ I. Thus, it is safe to set ℓ_{n} to be the maximum of I and max_{C∈Γ_{pos}^{n}}⌈\frac{J_{C}+|u_{n+1}|−C(χ_{in})}{Δ_{C}(v_{n})}⌉.

We set I′ = I and estimate a value for J′ such that χ′_{i′_{n}} ⟹^{v_{n}^{ℓn}u_{n+1}} χ′_{p} with each counter C ∈ (Γ \ Γ_{pos}^{n}) achieving a value of at least C(χ_{m}) at χ′_{p} and each counter C ∈ (Γ_{pos} \ Γ_{pos}^{n}) achieving a value of at least J_{C} at χ′_{p}.

By the induction hypothesis, Q(χ′_{i′_{n}}) = Q(χ_{i_{n}}) and F (χ′_{i′_{n}}) ≥ F (χ_{i_{n}}). Since χ_{i_{n}} ⟹^{v_{n}u_{n+1}},

it follows that χ′_{i′_{n}} ⟹^{v_{n}u_{n+1}}. By Proposition 4.1 (iii), to ensure that χ′_{i′_{n}} ⟹^{v_{n}^{ℓn}u_{n+1}} χ′_{p}, it is sufficient to raise each counter C with Δ_{C}(v_{n}) < 0 to a value of at least ℓ_{n}|v_{n}| + |u_{n+1}| at χ′_{i′_{n}}. If Δ_{C}(v_{n}) < 0 then, by the definition of pumpable decompositions, Δ_{C}(v_{i}) > 0 for some i ∈ [1..n−1], so C gets pumped above J′ in σ′.

Any counter C such that Δ_{C}(v_{n}) ≥ 0 will surely exceed C(χ_{m}) at χ′_{p}. On the other hand, a counter C such that Δ_{C}(v_{n}) < 0 can decrease by at most ℓ_{n}|v_{n}| + |u_{n+1}| after χ′_{i′_{n}}.

Putting these two facts together, it suffices to set J′ to ℓ_{n}|v_{n}|+|u_{n+1}|+max_{{C|Δ_{C}(v_{n})<0}}J_{C}.

Let ρ′ : χ′_{0} ⟹^{u_{1}} χ′_{i′_{1}} ⟹^{v_{1}^{ℓ_{1}}} χ′_{j′_{1}} ⟹^{u_{2}} ⋯ ⟹^{u_{n}} χ′_{i′_{n}} ⟹^{v_{n}^{ℓn}} χ′_{j′_{n}} ⟹^{u_{n+1}} χ′_{p}. By the induction

hypothesis, we know that χ′_{0} = χ_{0} and for i ∈ [1..n−1], ℓ_{i} ≥ I. By construction, ℓ_{n} ≥ I as well. We have also ensured that for every counter C, C(χ′_{p}) ≥ C(χ_{m}) and for every counter C ∈ Γ_{pos}, C(χ′_{p}) ≥ J. The fact that Q(χ′_{p}) = Q(χ_{m}) follows from the fact that each v_{n} loop brings the automaton back to Q(χ′_{i′_{n}}) = Q(χ_{i_{n}}), and the fact that both ρ and ρ′ go through the same sequence of transitions u_{n+1} at the end of the computation.

□

The preceding lemma shows that all the pumpable counters in a pumpable decomposition are simultaneously unbounded. This is analogous to a well-known result of Karp and Miller in the theory of vector addition systems [KM69]. They show how to associate a finite object called a covering tree with each vector addition system. The covering tree can be used to decide whether a set of coordinates of the vector addition system is simultaneously unbounded. See Section 6 for a more detailed discussion of the connection of our work to vector addition systems.

Corollary 4.4 Let A be an automaton and ρ a K-run of A, K ∈ ℕ, with a pumpable decomposition of the form

χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} χ_{i_{2}} ⟹^{v_{2}} χ_{j_{2}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}} χ_{m}.

(i) For any I ∈ ℕ, with I ≥ 1, there exist ℓ_{1}, ℓ_{2}, …, ℓ_{n−1} ∈ ℕ and a K-run ρ′ of A of the form

χ′_{0} ⟹^{u_{1}} χ′_{i′_{1}} ⟹^{v_{1}^{ℓ_{1}}} χ′_{j′_{1}} ⟹^{u_{2}} χ′_{i′_{2}} ⟹^{v_{2}^{ℓ_{2}}} χ′_{j′_{2}} ⋯ ⟹^{u_{n−1}} χ′_{i′_{n−1}} ⟹^{v_{n−1}^{ℓ_{n−1}}} χ′_{j′_{n−1}} ⟹^{u_{n}} χ′_{i′_{n}} ⟹^{v_{n}^{I}} χ′_{j′_{n}} ⟹^{u_{n+1}} χ′_{p}

such that χ_{0} = χ′_{0}, Q(χ′_{p}) = Q(χ_{m}) and F (χ′_{p}) ≥ F (χ_{m}).

(ii) For any I ∈ ℕ, with I ≥ 1 and any k ∈ [1..n], there exist ℓ_{1}, ℓ_{2}, …, ℓ_{k−1} ∈ ℕ and a K-run ρ′ of A of the form

χ′_{0} ⟹^{u_{1}} χ′_{i′_{1}} ⟹^{v_{1}^{ℓ_{1}}} χ′_{j′_{1}} ⟹^{u_{2}} ⋯ ⟹^{u_{k−1}} χ′_{i′_{k−1}} ⟹^{v_{k−1}^{ℓ_{k−1}}} χ′_{j′_{k−1}} ⟹^{u_{k}} χ′_{i′_{k}} ⟹^{v_{k}^{I}} χ′_{j′_{k}} ⟹^{u_{k+1}v_{k+1}...u_{n}v_{n}u_{n+1}} χ′_{p}

such that χ_{0} = χ′_{0}, Q(χ′_{p}) = Q(χ_{m}) and F (χ′_{p}) ≥ F (χ_{m}).

Proof: The first statement follows by setting J = 0 when defining ℓ_{n} in the proof of the Counter Pumping Lemma. The second result is then immediate. We omit the details. □

We have shown that all counters which increase within the pumpable blocks of a pumpable decomposition can be simultaneously raised to arbitrarily high values. We next describe a sufficient condition for a K-run to admit a non-trivial pumpable decomposition.

Strong pumping constant For each M, N, K ∈ ℕ, we define the strong pumping constant Π_{M,N,K} by induction on N as follows (recall that π_{M,N,K} denotes the weak pumping constant for (M, N, K)):

\begin{aligned}∀M, K ∈ ℕ. & Π_{M,0,K} & = & 1 \\ ∀M, N, K ∈ ℕ. & Π_{M,N+1,K} & = & Π_{M,N,π_{M,N+1,K}+K} + π_{M,N+1,K} + K \end{aligned}

Lemma 4.5 (Decomposition) Let A be an automaton with M states and N counters and let K ∈ ℕ. Let ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{m}} χ_{m} be any K-run of A. Then, there is a pumpable decomposition

χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} χ_{i_{2}} ⟹^{v_{2}} χ_{j_{2}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}} χ_{m}

of ρ such that for every counter C, if C(χ_{j}) > Π_{M,N,K} for some j ∈ [0..m], then there exists k ∈ [1..n], such that Δ_{C}(v_{k}) is positive.

To prove this lemma, we need the following result.

Proposition 4.6 Let A be a counter automaton with M states and N counters and let ρ : χ_{0} ⟹ χ_{n} be a K-run of A in which some counter value exceeds π_{M,N,K} + K. Then, there is a prefix σ : χ_{0} ⟹ χ_{s} of ρ such that:

• For each m ∈ [0..s] and every counter C, C(χ_{m}) < π_{M,N,K} + K.

• There exists r ∈ [0..s−1], such that σ : χ_{0} ⟹ χ_{r} ⟹ χ_{s}, Q(χ_{r}) = Q(χ_{s}) and F (χ_{r}) < F (χ_{s}).

Proof: Suppose that the lemma does not hold. Let ρ : χ_{0} ⟹^{t_{1}t_{2}...t_{n}} χ_{n} be a computation of minimum length which fails to satisfy the lemma. Since the initial counter values in ρ are bounded by K and some counter value exceeds π_{M,N,K} + K in ρ, it must be the case that the length of ρ is at least π_{M,N,K}.

By the definition of π_{M,N,K}, there exist i and j, i < j ≤ π_{M,N,K} such that Q(χ_{i}) = Q(χ_{j}) and F (χ_{i}) ≤ F (χ_{j}). Since ρ is a K-run and j ≤ π_{M,N,K}, all counter values at the configurations χ_{0}, χ_{1}, …, χ_{j} must be bounded by π_{M,N,K} + K. If F (χ_{i}) < F (χ_{j}), ρ would satisfy the lemma with r = i and s = j, so it must be the case F (χ_{i}) = F (χ_{j}).

Since χ_{i} = χ_{j}, we can construct a shorter computation ρ′ = χ_{0} ⟹^{t_{1}t_{2}...t_{i}} χ_{i} ⟶^{t_{j+1}} χ_{j+1} ⟶^{t_{j+2}} ⋯ ⟶^{t_{n}} χ_{n}. It is easy to see that the same counter whose value exceeded π_{M,N,K} + K in ρ must also exceed π_{M,N,K} + K in ρ′—the only configurations visited by ρ which are not visited by ρ′ are those in the interval χ_{i+1}, χ_{i+2}, … χ_{j}. However, we have already seen that all counter values in χ_{0}, χ_{1}, …, χ_{j} are bounded by π_{M,N,K} + K.

It is clear that if ρ′ satisfies the lemma, then so does ρ. On the other hand, if ρ′ does not satisfy the lemma, then ρ is not a minimum length counterexample to the lemma. In either case we obtain a contradiction. □

We now return to the proof of the Decomposition Lemma.

Proof: (of Lemma 4.5) The proof is by induction on N, the number of counters.

Basis: If N = 0, set n = 0 and u_{1} = ρ.

Induction step: Let Γ_{gt} denote the set of counters whose values exceed Π_{M,N,K} in the K-run ρ.

If Γ_{gt} = ∅, we set n = 0 and u_{1} = ρ.

Otherwise, by Proposition 4.6, we can find positions r and s in ρ such that χ_{0} ⟹^{u′} χ_{r} ⟹^{v′} χ_{s} ⟹ χ_{m}, with Q(χ_{r}) = Q(χ_{s}), F (χ_{r}) < F (χ_{s}) and all counter values at χ_{0}, χ_{1}, …, χ_{s} bounded by π_{M,N,K} + K.

Let Σ be the input alphabet of A and Γ its set of counters. Fix a counter C′ in which increases strictly between χ_{r} and χ_{s}—that is, C′(χ_{s}) > C′(χ_{r}). By our choice of χ_{r} and χ_{s}, such a counter must exist. Construct an automaton A′ with input alphabet Σ ∪ {C^{′+}, C^{′−}} and counters Γ \ {C′}. The states and transitions of A′ are the same as those of A. In other words, A′ behaves like A except that it treats moves involving the counter C′ as input letters.

Consider the computation χ_{s} ⟹^{t_{s+1}t_{s+2}...t_{m}} χ_{m} of A. It is easy to see that there is a corresponding computation ρ′ : χ′_{s} ⟹^{t_{s+1}t_{s+2}...t_{m}} χ′_{m} of A′ such that for each k ∈ [s..m], Q(χ_{k}) = Q(χ′_{k}) and for each counter C ≠ C′, C(χ_{k}) = C(χ′_{k}).

From Proposition 4.6, we know that ρ′ is in fact a (π_{M,N,K}+K)-run of A′. Further, for every counter C in Γ_{gt} \ {C′}, there exists a j ∈ [s..m], such that C(χ′_{j}) = C(χ_{j}) > Π_{M,N,K} > Π_{M,N−1,π_{M,N,K}+K}. (In the K-run ρ, no counter could have exceeded Π_{M,N,K} before χ_{s} because Proposition 4.6 guarantees that all counter values at χ_{0}, χ_{1}, …, χ_{s} are bounded by π_{M,N,K} + K.) By the induction hypothesis, we can find a pumpable decompostion

χ′_{s} ⟹^{u′_{1}} χ′_{i′_{1}} ⟹^{v′_{1}} χ′_{j′_{1}} ⟹^{u′_{2}} χ′_{i′_{2}} ⟹^{v′_{2}} χ′_{j′_{2}} ⟹^{u′_{3}} ⋯ ⟹^{u′_{p}} χ′_{i′_{p}} ⟹^{v′_{p}} χ′_{j′_{p}} ⟹^{u′_{p+1}} χ_{m}

of ρ′ such that if C is a counter with C(χ′_{j}) > Π_{M,N−1,π_{M,N,K}+K} for some j ∈ [s..m], then there exists k ∈ [1..p] such that Δ_{C}(v′_{k}) is positive.

Consider the corresponding computation

χ_{s} ⟹^{u′_{1}} χ_{i′_{1}} ⟹^{v′_{1}} χ_{j′_{1}} ⟹^{u′_{2}} χ_{i′_{2}} ⟹^{v′_{2}} χ_{j′_{2}} ⋯ ⟹^{u′_{p}} χ_{i′_{p}} ⟹^{v′_{p}} χ_{j′_{p}} ⟹^{u′_{p+1}} χ_{m}

of A. In this computation, for each k ∈ [1..p], Q(χ_{i′_{k}}) = Q(χ′_{i′_{k}}) = Q(χ′_{j′_{k}}) = Q(χ_{j′_{k}}). Further, for each C ∈ Γ_{gt} \ {C′}, C(χ_{i′_{k}}) = C(χ′_{i′_{k}}) and C(χ_{j′_{k}}) = C(χ′_{j′_{k}}).

We prefix the computation χ_{s} ⟹^{u′_{1}v′_{1}...u′_{p+1}} χ_{m} with the K-run χ_{0} ⟹^{u′} χ_{r} ⟹^{v′} χ_{s} which we used to identify χ_{s} and χ_{r}. We then assert that the composite K-run

χ_{0} ⟹^{u′} χ_{r} ⟹^{v′} χ_{s} ⟹^{u′_{1}} χ_{i′′_{1}} ⟹^{v′_{1}} χ_{j′′_{1}} ⟹^{u′_{2}} χ_{i′′_{2}} ⟹^{v′_{2}} χ_{j′′_{2}} ⋯ ⟹^{u′_{p}} χ_{i′′_{p}} ⟹^{v′_{p}} χ_{j′′_{p}} ⟹^{u′_{p+1}} χ_{m}.

provides the decomposition

χ_{0} ⟹^{u_{1}} χ_{i_{1}} ⟹^{v_{1}} χ_{j_{1}} ⟹^{u_{2}} χ_{i_{2}} ⟹^{v_{2}} χ_{j_{2}} ⋯ ⟹^{u_{n}} χ_{i_{n}} ⟹^{v_{n}} χ_{j_{n}} ⟹^{u_{n+1}} χ_{m}

of ρ claimed in the statement of the lemma. In other words, u_{1} = u′, v_{1} = v′, χ_{i_{1}} = χ_{r} and χ_{j_{1}} = χ_{s}, while for k ∈ [2..n], u_{k} = u′_{k−1}, v_{k} = v′_{k−1}, χ_{i_{k}} = χ_{i′_{k−1}} and χ_{j_{k}} = χ_{j′_{k−1}}.

Let us verify that this decomposition satisfies all the conditions required by the lemma. First we verify that this decomposition is pumpable.

• Since p ≤ N−1, it is clear than n = p+1 ≤ N.

• By construction Q(χ_{i_{1}}) = Q(χ_{r}) = Q(χ_{s}) = Q(χ_{j_{1}}). For k ∈ [2..n], Q(χ_{i_{k}}) = Q(χ_{i′_{k−1}}) = Q(χ_{j′_{k−1}}) = Q(χ_{j_{k}}).

• We know that Δv_{1} = Δv′ is non-zero and strictly positive by the choice of v′. For k ∈ [2..n], we know that Δ_{C}(v_{k}) = Δ_{C}(v′_{k−1}) for C ≠ C′. Since we have already established that Δv′_{k−1} is non-zero and has at least one positive entry for k ∈ [2..n], it follows that the corresponding change vectors Δv_{k} are also non-zero and have at least one positive entry.

• Let C be a counter and k ∈ [1..n] such that Δ_{C}(v_{k}) is negative. Since Δv_{1} = Δv′ is positive by the choice of v, it must be that k ∈ [2..n]. If C ≠ C′, then Δ_{C}(v′_{k−1}) = Δ_{C}(v_{k}) is negative. In this case, we already know that there exists ℓ ∈ [2..k−1], such that Δ_{C}(v′_{ℓ−1}) = Δ_{C}(v_{ℓ}) is positive.

On the other hand, if C = C′, it could be that Δ_{C′}(v′_{z}) is negative for all z ∈ [1..p], since C′ is treated as an input letter rather than as a counter in the automaton A′. However, we know that Δ_{C′}(v_{1}) = Δ_{C′}(v′) is positive by the choice of v′ and C′, so C′ also satisfies the condition of the lemma.

Finally, let C be a counter such that C(χ_{j}) > Π_{M,N,K} for some j ∈ [1..m]. If C ≠ C′, then C(χ_{j}) > Π_{M,N−1,π_{M,N,K}+K} for some j ∈ [s..m], so we already know that Δ_{C}(v′_{k−1}) = Δ_{C}(v_{k}) is positive for some k ∈ [2..n]. On the other hand, if C = C′, we know that Δ_{C}(v_{1}) = Δ_{C}(v′) is positive by the choice of v′ and C′.

□

The Counter Pumping Lemma we stated earlier allows us to pump blocks of transitions in a computation. However, it is possible for a pumpable block to consist solely of invisible transitions which increment and decrement counters. Using the Decomposition Lemma, we can prove a more traditional kind of pumping lemma, stated in terms of input strings.

Lemma 4.7 (Visible Pumping) Let L be a counter recognisable language. There exists n ∈ ℕ such that for all input strings w, if w ∈ L and |w| ≥ n then w can be written as w_{1}w_{2}w_{3} such that |w_{1}w_{2}| ≤ n, |w_{2}| ≥ 1 and w_{1}w_{2}^{i}w_{3} ∈ L for all i ≥ 1.

Proof: Let A = (Q, Σ, Γ, T, q_{in}, F) be a counter automaton which accepts L. From A, we construct a new automaton A′ by adding a new counter C_{vis} which is incremented each time an input letter is read.

Formally, A′ = (Q′, Σ, Γ′, T′, q_{in}, F) where:

• Q′ = Q ∪ {q_{t} | t = (q, d, q′) ∈ T and d ∈ Σ}.

• Γ′ = Γ ∪ {C_{vis}}.

• T′ = {(q, d, q′) ∈ T | d ∉ Σ} ∪ {(q, C_{vis}^{+}, q_{t}), (q_{t}, d, q′) | t = (q, d, q′) ∈ T, d ∈ Σ}.

It is clear that L(A′) = L(A) = L. Let M = |Q′| and N = |Γ′|. Set n = Π_{M,N,0}.

Let χ_{0} ⟹^{x} χ_{f} ⟹^{y} χ_{g} be an accepting run of A′ on w, where |w| ≥ Π_{M,N,0} and |α(x)↾_{Σ} | = Π_{M,N,0}. Let χ_{0} ⟹^{u_{1}v_{1}...u_{n}v_{n}u_{m+1}} χ_{f} be the pumpable decomposition of χ_{0} ⟹^{x} χ_{f} given by the Decomposition Lemma.

Since C_{vis} attains the value Π_{M,N,0} along χ_{0} ⟹^{x} χ_{f}, there is a pumpable block v_{i}, i ∈ [1..m], such that Δ_{C_{vis}}(v_{i}) > 0. Choose the first such block. Then Δ_{C_{vis}}(v_{j}) = 0 for all j < i.

Each pumpable block defines a cycle in A′. However, the structure of A′ ensures that a cycle has a move labelled C_{vis}^{+} iff it also has a move labelled by an input letter. Thus, v_{i} contains at least one move with a label from Σ, while α(v_{j})↾_{Σ} is empty for each j < i.

Let w_{1} = α(u_{1}v_{1}u_{2} … u_{i}), w_{2} = α(v_{i}) and w_{3} = α(u_{i+1}v_{i+1} … v_{n}u_{n+1}y).

By Corollary 4.4 (ii), for each I ∈ ℕ, there is a run χ_{0} ⟹^{u_{1}v_{1}^{ℓ_{1}}...u_{i}v_{i}^{I}u_{i+1}v_{i+1}...u_{m}v_{m}u_{m+1}} χ′_{f}

with Q(χ′_{f}) = Q(χ_{f}) and F (χ′_{f}) ≥ F (χ_{f}).

This means that ρ : χ_{0} ⟹^{u_{1}v_{1}^{ℓ_{1}}...u_{i}v_{i}^{I}u_{i+1}v_{i+1}...u_{m}v_{m}u_{m+1}} χ′_{f} ⟹^{y} χ′_{g} is an accepting run on

α(u_{1}v_{1}^{ℓ_{1}} … u_{i}v_{i}^{I}u_{i+1} … u_{m}v_{m}u_{m+1}z) ↾_{Σ} . Since α(v_{j}) = ε for all j < i, it follows that α(u_{1}v_{1}^{ℓ_{1}} … u_{i−1}v_{i−1}^{ℓ_{i−1}}u_{i}) = α(u_{1}v_{1} … u_{i−1}v_{i−1}u_{i}) = w_{1}. Thus, ρ is an accepting run over w_{1}w_{2}^{I}w_{3}, as claimed by the lemma.

□

Example 4.8 The language L = {a^{p} | p is prime} is not counter recognisable.

Proof: Suppose L is counter recognisable. Let p be a prime larger that n, the pumping constant for L specified by Lemma 4.7. Then, we can write p as x + y + z such that a^{x+my+z} ∈ L for all m ≥ 1. Choose m = p + 1. Then a^{x+(p+1)y+z} ∈ L, though x + (p + 1)y + z = x + y + z + py = (1 + y)p is not a prime! □

One difference between the preceding lemma and the traditional pumping lemma for regular languages is that in the context of counter recognisable languages, for a pumpable string uvw, we must have at least one iteration of the pumpable segment v to ensure that the resulting string uv^{i}w is in the language, whereas for regular languages, uv^{0}w = uw is also guaranteed to be in the language.

Lemma 4.9 (Counter Hierarchy) For k ∈ ℕ, let L_{k} be the set of languages recognisable by counter automata with k counters. Then, for all k, L_{k} ⊊ L_{k+1}.

Proof: Define L_{k+1} = {a_{0}^{n_{0}}a_{1}^{n_{1}} ⋯ a_{k}^{n_{k}}a_{k+1}^{n_{k+1}} | n_{0} ≥ n_{1} ≥ ⋯ ≥ n_{k+1}}. It is not difficult to construct a counter automaton with k+1 counters which accepts L_{k+1}. However, there is no k-counter machine which accepts this language.

Suppose A is a k-counter machine which accepts L_{k+1}. As in the proof of Lemma 4.7, we extend A with a new counter C_{k+1} which is incremented precisely when a_{k+1} is read from the input. Let the new machine A′ have M states.

Consider an accepting run ρ of A′ on a string w = a_{0}^{n_{0}}a_{1}^{n_{1}} … a_{k+1}^{n_{k+1}} with n_{k+1} ≥ Π_{M,k+1,0}. By Lemma 4.5, the run ρ has a pumpable decomposition χ_{0} ⟹^{u_{1}v_{1}...u_{m}v_{m}u_{m+1}} χ_{f} such that m ≤ k+1 and Δ_{C_{k+1}}(v_{i}) > 0 for some i ∈ [1..m].

By Lemma 4.3, for each I ≥ 1, there exist ℓ_{1}, ℓ_{2}, …, ℓ_{m} ∈ ℕ such that each ℓ_{j} ≥ I

and χ_{0} ⟹^{u_{1}v_{1}^{ℓ_{1}}...u_{m}v_{m}^{ℓm}u_{m+1}} χ′_{f} is an accepting run. From the structure of words in L_{k+1}, it follows that for each pumpable block v_{i}, α(v_{i}) contains at most one of the visible letters {a_{0}, a_{1}, …, a_{k+1}}. Since m ≤ k+1 at least one letter from {a_{0}, a_{1}, …, a_{k+1}} does not appear in ⋃_{i∈[1..m]} α(v_{i}). Also, since Δ_{C_{k+1}}(v_{i}) > 0 for some i ∈ [1..m], from the structure of A′ it follows that a_{k+1} does appear in ⋃_{i∈[1..m]} α(v_{i}).

Let a_{r} be a letter which does not appear in ⋃_{i∈[1..m]} α(v_{i}) and let v_{j} be the block such that a_{k+1} appears in α(v_{j}). By Corollary 4.4 (ii), for all I ≥ 1, there exist ℓ_{1}, ℓ_{2}, …, ℓ_{j−1}

with each ℓ_{j} ≥ I such that χ_{0} ⟹^{u_{1}v_{1}^{ℓ_{1}}...v_{j−1}^{ℓ_{j−1}}u_{j}v_{j}^{I}u_{j+1}v_{j+1}...u_{m}v_{m}^{ℓm}u_{m+1}} χ′_{g} is an accepting run of

A′. Choose I = n_{r} + 1.

Thus w′ = α(u_{1}v_{1}^{ℓ_{1}} … v_{j−1}^{ℓ_{j−1}}u_{j}v_{j}^{n_{r}+1}u_{j+1}v_{j+1} … u_{m}v_{m}^{ℓ_{m}}u_{m+1})) ↾_{Σ} ∈ L(A′). But, w′ has only n_{r} a_{r}’s and at least n_{r}+1 a_{k+1}’s, which violates the definition of L_{k+1}.

Thus, there is no k-counter machine which accepts L_{k+1}.

□

The proof above requires alphabets of size k+2 to separate L_{k} from L_{k+1}. However, it is not difficult to tighten the proof to establish a strict hierarchy for alphabets of size 3.

5 Characterising Regularity of Counter Recognisable Languages

Automata with bounded counters

Let A = (Q, Σ, Γ, T, q_{in}, F) be a counter automaton. For K ∈ ℕ, define A[K] = (Q[K], T [K], Q[K]_{in}, F [K]) to be the finite-state automaton over the alphabet Σ ∪ Γ^{±} given by:

• Q[K] = Q × {f | f : Γ ⟶ [0..K]}.

• Q[K]_{in} = (q_{in}, \overline{0}).

• F [K] = Q_{f} × {f | f : Γ ⟶ [0..K]}.

• If (q, d, q′) ∈ T, then ((q, f), d, (q′, f′)) ∈ T [K] where:

– If d ∈ Σ, f′ = f.

– If d = C^{+}, f′(C′) = f(C′) for all C′ ≠ C and f′(C) = \{ \begin{matrix}f(C)+1 & if f(C) < K \\ K & otherwise \end{matrix}

– If d = C^{−}, f′(C′) = f(C′) for all C′ ≠ C, f(C) ≥ 1 and f′(C) = \{ \begin{matrix}f(C)−1 & if f(C) < K \\ K & otherwise \end{matrix}

Notice that each transition t = ((q, f), d, (q′, f′)) ∈ T [K] corresponds to a unique transition (q, d, q′) ∈ T, which we denote t^{−1}. For a sequence of transitions t_{1}t_{2} … t_{n}, we write (t_{1}t_{2} … t_{n})^{−1} for t_{1}^{−1}t_{2}^{−1} … t_{n}^{−1}. Note that for any sequence t_{1}t_{2} … t_{n} of transi-

tions in T [K], α(t_{1}t_{2} … t_{n}) = α((t_{1}t_{2} … t_{n})^{−1}). Moreover, if (q_{0}, f′_{0}) ⟹^{t_{1}t_{2}...t_{n}} (q_{n}, f′_{n}) and

(q_{0}, f_{0}) ⟹^{(t_{1}t_{2}...t_{n})^{−1}} χ_{n}, then Q(χ_{n}) = q_{n}.

Thus, the finite-state automaton A[K] behaves like a counter automaton except that it deems any counter whose value attains a value K to be “full” . Once a counter is declared to be full, it can be decremented as many times as desired. The following observations are immediate.

Proposition 5.1

(i) If (q_{0}, f′_{0}) ⟶^{t′_{1}} (q_{1}, f′_{1}) ⟶^{t′_{2}} ⋯ ⟶^{t′_{n}} (q_{n}, f′_{n}) is a computation of A then, (q_{0}, f_{0}) ⟶^{t_{1}}

(q_{1}, f_{1}) ⟶^{t_{2}} ⋯ ⟶^{t_{n}} (q_{n}, f_{n}) is a computation of A[K] where

• t′_{1}t′_{2} … t′_{n} = (t_{1}t_{2} … t_{n})^{−1}.

• ∀C ∈ Γ. ∀i ∈ [1..n]. f_{i}(C) = \{ \begin{matrix}f′_{i}(C) & if f′_{j}(C) < K for all j ≤ i \\ K & otherwise \end{matrix}

(ii) Let (q_{0}, f_{0}) ⟶^{t_{1}} (q_{1}, f_{1}) ⟶^{t_{2}} ⋯ ⟶^{t_{n}} (q_{n}, f_{n}) be a computation of A[K]. Then there is a maximal prefix t_{1}t_{2} … t_{ℓ} of t_{1}t_{2} … t_{n} such that there is a computation

(q_{0}, f′_{0}) ⟶^{t_{1}^{−1}} (q_{1}, f′_{1}) ⟶^{t_{2}^{−1}} … ⟶^{t_{ℓ}^{−1}} (q_{ℓ}, f′_{ℓ}) of A with f_{0} = f′_{0}. Moreover, if ℓ < n,

then for some counter C, α(t′_{ℓ+1}) = C^{−}, f′_{ℓ}(C) = 0 and there is a j < ℓ such that f′_{j}(C) = K.

(iii) Let L(A[K]) be the language over Σ ∪ Γ^{±} accepted by A[K]. Let L_{Σ}(A[K]) = {w↾_{Σ} | w ∈ L(A[K])}. Then, L(A) ⊆ L_{Σ}(A[K]).

Synchronised products of counter automata

Product automaton Let A_{1} = (Q_{1}, Σ_{1}, Γ_{1}, T_{1}, q_{in}^{1}, F_{1}) and A_{2} = (Q_{2}, Σ_{2}, Γ_{2}, T_{2}, q_{in}^{2}, F_{2}) be two counter automata. The product automaton A_{1} ×A_{2} is the structure (Q_{1} ×Q_{2}, Σ_{1} ∪ Σ_{2}, Γ_{1} ∪ Γ_{2}, T_{1} × T_{2}, (q_{in}^{1}, q_{in}^{2}), F_{1} × F_{2}), where ((q_{1}, q_{2}), d, (q′_{1}, q′_{2})) ∈ T_{1} × T_{2} iff one of the following holds:

• d ∈ (Σ_{1} ∪ Γ_{1}) ∩ (Σ_{2} ∪ Γ_{2}) and (q_{i}, d, q′_{i}) ∈ T_{i} for i ∈ {1, 2}.

• d ∈ (Σ_{1} ∪ Γ_{1}) \ (Σ_{2} ∪ Γ_{2}), (q_{1}, d, q′_{1}) ∈ T_{1} and q_{2} = q′_{2}.

• d ∈ (Σ_{2} ∪ Γ_{2}) \ (Σ_{1} ∪ Γ_{1}), (q_{2}, d, q′_{2}) ∈ T_{2} and q_{1} = q′_{1}.

For t = ((q_{1}, q_{2}), d, (q′_{1}, q′_{2})) ∈ T and i ∈ {1, 2}, let π_{i}(t) denote (q_{i}, d, q′_{i}) if d ∈ (Σ_{i} ∪Γ_{i}) and the empty string ε otherwise. As usual, π_{i}(t_{1}t_{2} … t_{n}) is just π_{i}(t_{1})π_{i}(t_{2}) … π_{i}(t_{n}). Thus, for a sequence of transitions ρ = t_{1}t_{2} … t_{n} over T_{1} × T_{2}, π_{1}(ρ) and π_{2}(ρ) denote the projections of ρ onto the transitions of A_{1} and A_{2} respectively. Clearly, α(t_{1}t_{2} … t_{n})↾_{(Σ_{i}∪Γ_{i})} = α(π_{i}(t_{1}t_{2} … t_{n})) for i ∈ {1, 2}.

We shall often write a configuration ((q_{1}, q_{2}), f) of A_{1} × A_{2} as a pair of configurations ((q_{1}, f_{1}), (q_{2}, f_{2})) of A_{1} and A_{2}, where f_{1} and f_{2} are restrictions of f to Γ_{1} and Γ_{2} respectively.

The following observations are easy consequences of the definition of product automata.

Proposition 5.2

(i) ((q_{in}^{1}, \overline{0}), (q_{in}^{2}, \overline{0})) ⟹^{t_{1}t_{2}...t_{n}} ((q_{1}, f_{1}), (q_{2}, f_{2})) is a computation of A_{1} × A_{2} if and only if

(q_{in}^{1}, \overline{0}) ⟹^{π_{1}(t_{1}t_{2}...t_{n})} (q_{1}, f_{1}) and (q_{in}^{2}, \overline{0}) ⟹^{π_{2}(t_{1}t_{2}...t_{n})} (q_{2}, f_{2}) are computations of A_{1} and

A_{2} respectively.

(ii) If Σ_{1} = Σ_{2} and Γ_{1} ∩ Γ_{2} = ∅, then L(A_{1} × A_{2}) = L(A_{1}) ∩ L(A_{2}).

Regularity and closure under complementation

Let L ⊆ Σ^{∗} be a language such that both L and its complement \overline{L} are accepted by counter automata. Let L = L(A) and \overline{L} = L(\overline{A}), where we can assume that A and \overline{A} use disjoint sets of counters. Then the language accepted by A × \overline{A} must be empty.

Let M be the number of states of A×\overline{A} and N be the number of counters that it uses. Let K be a number greater than Π_{M,N,0}, the strong pumping constant for (M, N, 0). Recall that A[K] = (Q[K], T [K], Q[K]_{in}, F [K]) is a finite-state automaton without counters working on the input alphabet Σ ∪ Γ^{±}.

Lemma 5.3 L(A[K] × \overline{A}) = ∅.

Proof: Let A[K] = (Q[K], T [K], Q[K]_{in}, F [K]) and \overline{A} = (\overline{Q}, Σ, \overline{Γ}, \overline{T} , \overline{q}_{in}\overline{F}). Each com-

putation ρ of A[K] × \overline{A} is of the form ((q_{0}, \overline{0}), (\overline{q}_{0}, \overline{0})) ⟶^{u_{1}} ((q_{1}, f_{1}), (\overline{q}_{1}, \overline{f}_{1})) ⟶^{u_{2}} ⋯ ⟶^{u_{n}}

((q_{n}, f_{n}), (\overline{q}_{n}, \overline{f}_{n})), where, for i ∈ [0..n], u_{i} ∈ T [K] × \overline{T}.

By Propositions 5.1 and 5.2, corresponding to the sequence u_{1}u_{2} … u_{n} there exists a maximal sequence of transitions v_{1}v_{2} … v_{m} of A × \overline{A} where:

• Each v_{i} belongs to T × \overline{T}.

• For each i ∈ [1..m], π_{2}(v_{i}) = π_{2}(u_{i}).

• For each i ∈ [1..m], π_{1}(v_{i}) = \{ \begin{matrix}(π_{1}(u_{i}))^{−1} & if π_{1}(u_{i}) ≠ ε \\ ε & otherwise \end{matrix}

• ρ′ : ((q_{0}, \overline{0}), (\overline{q}_{0}, \overline{0})) ⟶^{v_{1}} ((q_{1}, f′_{1}), (\overline{q}_{1}, \overline{f}_{1})) ⟶^{v_{2}} ⋯ ⟶^{v_{m}} ((q_{m}, f′_{m}), (\overline{q}_{m}, \overline{f}_{m})) is a com-

putation of A × \overline{A}.

• If m < n, then for some Ĉ ∈ Γ, α(u_{m+1}) = Ĉ^{−}, f′_{m}(Ĉ) = 0 and f′_{j}(Ĉ) = K for some j ∈ [0..m].

Let us define the residue length of ρ to be n−m.

Suppose that L(A[K]×\overline{A}) is non-empty. Since L(A×\overline{A}) is empty, it is easy to see that any accepting run of A[K] × \overline{A} has a non-zero residue length. Without loss of generality, assume that the run ρ considered earlier is an accepting run of A[K] × \overline{A} whose residue length is minimal. Then, in the corresponding run ρ′ of A × \overline{A}, the counter Ĉ ∈ Γ attains the value K along ρ′ and then goes to 0 at the end of the run so that the move labelled Ĉ^{−} is not enabled at ((q_{m}, f′_{m}), (\overline{q}_{m}, \overline{f}_{m})).

Since K exceeds the strong pumping constant for A × \overline{A}, by Lemma 4.3 we can find

an alternative run ρ̂′ : ((q_{0}, \overline{0}), (\overline{q}_{0}, \overline{0})) ⟹^{v′_{1}v′_{2}...v′_{ℓ}} ((q′_{ℓ}, f′_{ℓ}), (\overline{q}′_{ℓ}, \overline{f}′_{ℓ})) with (q′_{ℓ}, \overline{q}′_{ℓ}) = (q_{m}, \overline{q}_{m}),

f′_{ℓ}(Ĉ) ≥ K, and all other counter values at (f′_{ℓ}, \overline{f}′_{ℓ}) at least as large as at (f_{m}, \overline{f}′_{m}). In particular, every counter which exceeded the cutoff value K along ρ′ is pumpable and thus exceeds K along ρ̂′ as well.

By Propositions 5.1 and 5.2, we can construct a corresponding sequence of transitions u′_{1}u′_{2} … u′_{ℓ} over T [K]×\overline{T} such that π_{1}(v′_{1}v′_{2} … v′_{ℓ}) = (π_{1}(u′_{1}u′_{2} … u′_{ℓ}))^{−1} and π_{2}(v′_{1}v′_{2} … v′_{ℓ}) =

π_{2}(u′_{1}u′_{2} … u′_{ℓ}), where ρ̂ : ((q_{0}, \overline{0}), (\overline{q}_{0}, \overline{0})) ⟹^{u′_{1}u′_{2}...u′_{ℓ}} ((q′′_{ℓ}, f′′_{ℓ}), (\overline{q}′_{ℓ}, \overline{f}′_{ℓ})) is a run of A[K] × \overline{A}

with (q′′_{ℓ}, \overline{q}′_{ℓ}) = (q_{m}, \overline{q}_{m}) and f′′_{ℓ}(C) ≥ f_{m}(C) for each C ∈ Γ.

We already know that \overline{f}′_{ℓ}(C) ≥ \overline{f}_{m}(C) for each C ∈ \overline{Γ}. Further, since every counter which exceeded the cutoff value K along ρ′ also exceeds K along ρ̂′, we know that any counter which has become full along ρ would also have become full along ρ̂. Thus, we can extend ρ̂ to an accepting run σ by appending the sequence of transitions u_{m+1}u_{m+2} … u_{n} which occur at the end of the accepting run ρ.

Recall that α(u_{m+1}) = Ĉ^{−} and f′_{ℓ}(Ĉ) ≥ 1 by our choice of ρ̂′. From this, it follows that the residue length of the newly constructed accepting run σ is at least one less than the residue length of ρ, which is a contradiction, since ρ was assumed to be an accepting run of minimal residue length. □

Theorem 5.4 Let L be a language over Σ. L and \overline{L} are counter recognisable iff L is regular.

Proof: Let L = L(A) and \overline{L} = L(\overline{A}). Define A[K] as above. We claim that L_{Σ}(A[K]) = L(A).

By Proposition 5.1, we know that L(A) ⊆ L_{Σ}(A[K]).

On the other hand, from the previous lemma it follows that L_{Σ}(A[K]) ∩ L(\overline{A}) = ∅. This implies that L_{Σ}(A[K]) ⊆ \overline{L(\overline{A})}, which means that L_{Σ}(A[K]) ⊆ L(A).

So L(A) = L_{Σ}(A[K]). Since A[K] is a finite- state automaton, it follows that L(A) is regular. Therefore, if a language and its complement are counter recognisable then the language is regular.

The converse is obvious: if L is a regular language, we can find finite-state automata recognising both L and \overline{L}. Since finite-state automata are trivial examples of counter automata, both L and \overline{L} are counter recognisable. □

Observe that our construction is effective—given automata A and \overline{A} for L and \overline{L} respectively, we can construct a finite-state automaton A[K] for L.

Regularity and closure under reversal

Suppose L is recognised by the deterministic counter automaton A and L-reverse is accepted by the counter automaton B. We will show that there is a constant τ, depending on the number of states M and the number of counters N of A, such that A[τ] recognises L.

Overview

The proof has two parts.

Part 1. We assume that L(A[τ]) ≠ L and conclude from this that there exist strings β, γ ∈ Σ^{∗} such that

∀i ≥ 1. ∃α ∈ Σ^{∗}. ∃n. [αβ^{i}γ ∈ L & ∀j ≥ n. αβ^{j}γ ∉ L].

Part 2. We consider the reverse of the language L. Part 1 shows that there exist strings β̂, γ̂ ∈ Σ^{∗} such that

∀i ≥ 1. ∃α ∈ Σ^{∗}. ∃n. [γ̂β̂^{i}α̂ ∈ L-reverse & ∀j ≥ n. γ̂β̂^{j}α̂ ∉ L-reverse].  (1)

On the other hand, we will show that for all counter automata B and all β, γ ∈ Σ^{∗}, there exists an n such that if γβ^{i}α ∈ L(B) for some i ≥ n, then γβ^{j}α ∈ L(B) for infinitely many j. Thus, it follows from (1) that L-reverse is not counter recognisable. This contradiction shows that our assumption L ≠ L(A[τ]) (of Part 1) is false. We thus have L = L(A[τ]), and in particular, that L is regular.

Notation.

• While analysing the computation of counter automata, we will permit counters to assume negative values. We refer to such computations as free runs, and use χ_{0} ⇝^{t} χ_{m} to denote the free run corresponding to the sequence of transitions t, starting from configuration χ_{0} and ending at configuration χ_{m}, passing through configurations χ_{i}.

• Let A be a counter automaton with M states and N counters. We say that the counter C is saturated in the free run χ_{0} ⇝^{u} χ_{m}, if for some i ∈ [0..m], C(χ_{i}) ≥ Π_{M,N,0}, and for all j < i, C(χ_{j}) ≥ 0.

Constants. In the rest of this section we write Π for Π_{M,N,0}. Let

κ = M · Π^{N} + 1;
τ = N · κ.

Part 1

Lemma 5.5 Suppose t is a sequence of transitions such that (q_{in}, \overline{0}) ⟹^{t} is an accepting run of A[τ] but not of A. Then, we have t = uvw with the free run

χ_{0} ⇝^{u} χ_{i} ⇝^{v} χ_{j} ⇝^{w} χ_{n},

where 0 < i < j < n, such that

(i) For some counter Ĉ, ΔĈ(v) < 0.

(ii) Q(χ_{i}) = Q(χ_{j}).

(iii) If for some counter C, Δ_{C}(v) ≠ 0 or C assumes a negative value on the free run of A corresponding to t, then C is saturated in the free run A ⇝^{u}.

Proof: Let t = t_{1}t_{2} … t_{n}. Consider the free run corresponding to t,

ρ : (q_{in}, \overline{0}) = χ_{0} ⇝^{t_{1}} χ_{1} ⇝^{t_{2}} ⋯ ⇝^{t_{n}} χ_{n}.

Since this is not an accepting run of A, there is a j < n and a counter C such that C(χ_{j}) < 0. Since (q_{in}, \overline{0}) ⟹^{t} is an accepting run of A[τ], there must be an i < j, where C(χ_{i}) = τ. Choose ℓ to be the maximum i such that there is a counter Ĉ satisfying the following two conditions.

• Ĉ(χ_{i}) = τ.

• For some j > i, Ĉ(χ_{j}) < 0.

Let m be the minimum j > ℓ such that Ĉ(χ_{j}) = 0. Note that m < n, because there is a j > ℓ where Ĉ(χ_{j}) < 0.

Let x = t_{1}t_{2} … t_{ℓ}, y = t_{ℓ+1}t_{ℓ+2} … t_{m} and z = t_{m+1}t_{m+2} … t_{n}. Since Ĉ(χ_{ℓ}) = τ and Ĉ(χ_{m}) = 0, in the computation

χ_{ℓ} ⇝^{t_{ℓ+1}} χ_{ℓ+1} ⇝^{t_{ℓ+2}} ⋯ ⇝^{t_{m}} χ_{m},

Ĉ takes all values in the range [0..τ]. For j ∈ [0, N], let k_{j} be the minimum k ∈ [ℓ..m] such that Ĉ(χ_{k}) = τ − jκ. The computation on xy can then be written as

ρ′ : χ_{0} ⇝^{y_{0}=x} χ_{ℓ} = χ_{k_{0}} ⇝^{y_{1}} χ_{k_{1}} ⇝^{y_{2}} ⋯ ⇝^{y_{N}} χ_{k_{N}} = χ_{m}.

Let Γ′ be the set of counters that assume a value Π or bigger somewhere in ρ′. For C ∈ Γ′, let j_{C} be the minimum j such that C assumes a value Π or bigger in the segment of the above computation corresponding to y_{j}. In particular, jĈ = 0 because Ĉ(χ_{ℓ}) = τ ≥ Π and χ_{0} ⇝^{y_{0}} χ_{ℓ}. There are only |Γ′| ≤ N counters, whereas there are N +1 segments. Thus, there is a j ∈ [0..N] such that j ≠ j_{C} for all C ∈ Γ′. Let ĵ be the minimum such j; since jĈ = 0, we have ĵ ≠ 0. Consider the computation corresponding to yĵ,

ρ′′ : χ′_{0} ⇝^{t′_{1}} χ′_{1} ⇝^{t′_{2}} ⋯ ⇝^{t′_{h}} χ′_{h},

where t′_{i} = t_{k_{ĵ−1}+i}, χ′_{i} = χ_{k_{ĵ−1}+i} and h = kĵ−k_{ĵ−1}. In this computation the value of Ĉ falls from τ − (ĵ− 1)κ to τ − ĵκ, that is, by κ. For i ∈ [0..κ], let p_{i} be the minimum p ∈ [0..h] such that Ĉ(χ′_{p}) = Ĉ(χ′_{0}) − i = τ − (ĵ− 1)κ − i. Then, ρ′′ can be written as

ρ′′ = χ′′_{0} ⇝^{y′_{1}} χ′′_{1} ⇝^{y′_{2}} χ′′_{2} ⇝^{y′_{3}} ⋯ ⇝^{y′_{κ}} χ′′_{κ},

where χ′′_{i} = χ′_{p_{i}} for i ∈ [0..κ]. Let Γ′′ be the set of counters whose values in ρ′′ after χ′′_{0} are less than Π. Since κ = MΠ^{N} + 1, there exist r, s ∈ [1..κ], r < s, such that

(C1) C(χ′′_{r}) = C(χ′′_{s}), for all C ∈ Γ′′.

(C2) Q(χ′′_{r}) = Q(χ′′_{s}).

The definition of χ′′_{i} implies

(C3) Ĉ(χ′′_{r}) = Ĉ(χ_{k_{j−1}}) − r > Ĉ(χ_{k_{j−1}}) − s = Ĉ(χ′′_{s}).

Now let

u = xy_{1}y_{2} … yĵ ; −1 y′_{1}y′_{2} … y′_{r};
v = y′_{r+1}y′_{r+2} … y′_{s};
and w = y′_{s+1}y′_{s+2} … y′_{κ} yĵ ; +1yĵ ; +2 … y_{N} z.

We claim that this choice of u, v and w satisfies the requirements of the lemma. Clearly, t = uvw. Part (i) of the lemma follows immediately from condition (C3) above; part (ii) follows from condition (C2). We now consider part (iii).

If C becomes negative in the free run ρ, then it must assume the value τ somewhere before that, because (q_{in}, \overline{0}) ⟹^{t} is an accepting run in A[τ]. By the maximality of ℓ, this happens at or before χ_{ℓ}. Thus, C is saturated in the free run χ_{0} ⇝^{u}. Next, we consider counters C such that Δ_{C}(v) ≠ 0. We may assume that C does not become negative in ρ, for we have just taken care of all such counters. By condition (C1) above, C ∉ Γ′′. That is, C takes a value Π or bigger after χ′′_{0} in the computation ρ′′. Thus, j_{C} ≤ ĵ. Since ĵ ≠ j_{C} for all C, we have j_{C} < ĵ. Hence, C is saturated in the free run χ_{0} ⇝^{u}. □

We need the following pumping lemma for free runs.

Lemma 5.6 Suppose χ_{0} ⇝^{t} χ_{m} is a free run of A, where every counter that assumes a negative value is saturated. Let Γ′ be the set of counters saturated in this run. Then, for

all K, A has a run χ′_{0} ⟹^{t′} χ′_{m′} such that χ_{0} = χ′_{0}, Q(χ′_{m′}) = Q(χ_{m}), F (χ′_{m′}) ≥ F (χ_{m})

and C(χ′_{m′}) ≥ K for all C ∈ Γ′.

Proof: Similar to the proof of the Counter Pumping Lemma. Omitted. □

Proof of Part 1. If L ≠ L(A[τ]), then there exists a string a ∈ L(A[τ]) \ L. Let (q_{in}, \overline{0}) ⟹^{t} be the shortest accepting run of A[τ] such that α(t)↾_{Σ} = a. Clearly, χ_{0} ⇝^{t} is a free run of A, but since a ∉ L, this is not an accepting run of A. Using Lemma 5.5, we obtain a decomposition t = uvw such that the free run

χ_{0} ⇝^{u} χ_{ℓ} ⇝^{v} χ_{m} ⇝^{w} χ_{n},

(0 < ℓ < m < n) satisfies (i), (ii) and (iii). Let β = α(v)↾_{Σ} and γ = α(w)↾_{Σ} . We first show that for all i ≥ 1 there is an α such that αβ^{i}γ ∈ L.

Fix i ≥ 1. Part (ii) implies that there is a free run of the form

χ′_{0} ⇝^{u} χ′_{ℓ′} ⇝^{v^{i}} χ′_{m′} ⇝^{w} χ′_{n′},

where χ_{0} = χ′_{0} and Q(χ′_{n′}) = Q(χ_{n}). Part (iii) implies that all counters that assume a negative value in this run are saturated in the initial segment χ′_{0} ⇝^{u} χ′_{ℓ′}. We apply Lemma 5.6 to this initial segment with

K = max_{C,l′≤j≤n′} |C(χ′_{j})|.

We obtain u′ such that in the run χ_{0} ⟹^{u′} χ′′, Q(χ′′) = Q(χ′_{ℓ′}), C(χ′′) ≥ C(χ′_{ℓ}) for all C

and C(χ′′) ≥ K for all counters saturated in χ′_{0} ⇝^{u} χ′_{ℓ′}. Then, A ⟹^{u′v^{i}w} is an accepting run of A. In particular, α(u′v^{i}w) = αβ^{i}γ ∈ L, where α = α(u′)↾_{Σ} .

It remains to show that αβ^{j}γ ∉ L, for all large enough j. We first observe that α(v)↾_{Σ} is not empty. For otherwise, since A is deterministic, the set of states of A that appear in the run χ_{m} ⇝^{w} χ_{n} is a subset of the set of states that appear in the run χ_{ℓ} ⇝^{v} χ_{m}. This implies that Q(χ_{n}) = Q(χ_{j}), for some j ∈ [ℓ..m], and, furthermore, that α(w)↾_{Σ} is empty. But then χ_{0} ⇝^{t} is not the shortest accepting run of A[τ] with α(t)↾_{Σ} = a. This contradiction shows that α(v)↾_{Σ} is not empty.

Clearly, for all j ≥ 1 we have the free run χ_{0} ⇝^{uv^{j}w}. Since ΔĈ(v) < 0, for all large enough j this is not an accepting run of A. Suppose αβ^{j}γ ∈ L for some such j. Then, since A is deterministic, we have uv^{j}w = t_{1}t_{2}, where χ_{0} ⟹^{t_{1}} is an accepting run of A and α(t_{2})↾_{Σ} is empty, which implies that |t_{2}| < |vw|. Let |t_{2}| = k; we have 1 ≤ k < |vw|. Now χ_{0} ⟹^{t_{1}} is an accepting run of A. By comparing this run with the run χ_{0} ⟹^{t} χ_{n}, we observe that Q(χ_{n−k}) is a final state of A. But then α(t_{1}t_{2} … t_{n−k})↾_{Σ} = a and χ_{0} ⇒ t_{1}t_{2} … t_{n−k} is an accepting run of A[τ], contradicting the minimality of t. Hence, αβ^{j}γ ∉ L for all large enough j. □

Part 2.

Lemma 5.7 There exists a function A(M, N, K, L) such that if ρ : χ_{0} ⟹^{t} is a K-run of a counter automata A with M states and N counters such that

• |α(t)↾_{Σ} | ≤ L and

• |t| ≥ A(M, N, K, L),

then t = uvw such that

• χ_{0} ⟹^{u} χ′ ⟹^{v} χ′′ ⟹^{w};

• Q(χ′) = Q(χ′′) and F (χ′) ≤ F (χ′′);

• α(v′) is non-empty but has no symbols from Σ.

Proof: Let

A(M, N, K, L) = \{ \begin{matrix}π_{M,N,K} & if L = 0 \\ π_{M,N,K} + A(M, N, K + π_{M,N,K}, L − 1) & if L ≥ 1 \end{matrix} .

We will prove by induction on L that A(M, N, K, L) defined above satisfies the requirements of the lemma. Basis: If L = 0, the claim follows from the definition of the weak pumping constant. Induction step: Let ρ : χ_{0} ⟹^{t′} χ_{1} ⟶^{a} χ_{2} ⟹^{t′′}, where t′ is the maximal prefix of t with no symbols from Σ, and a ∈ Σ. If |t′| ≥ π_{M,N,K}, then the claim follows from the definition of the weak pumping constant.

Otherwise, χ_{2} ⟹^{t′′} is a (K + π_{M,N,K})-run. Also, |α(t′′)↾_{Σ} | = |α(t)↾_{Σ} | − 1 and

|t′′| ≥ t − π_{M,N,K} ≥ A(M, N, K + π_{M,N,K}, L − 1).

The claim then follows from the induction hypothesis. □

Note. In the above lemma, we can assume that |uv| ≤ A(M, N, K, L), for we can always restrict ourselves to the prefix of t of length exactly A(M, N, K, L).

Lemma 5.8 Suppose A is a counter automaton with M states and N counters. Let (l_{i})_{i=0}^{∞} be a sequence of non-negative integers. Then there exists a constant B = B(M, N, K, (l_{i})) such that if

ρ : χ_{0} ⟹^{v_{0}} χ_{1} ⟹^{v_{1}} ⋯ ⟹^{v_{B−1}} χ_{B},

where |v_{i}| ≤ l_{i}, then there exist i, j ∈ [1, B], i < j, such that Q(χ_{i}) = Q(χ_{j}) and F (χ_{i}) ≤ F (χ_{j}).

Proof: We will modify the proof of Lemma 2.7. Consider the following infinite tree T whose nodes are labelled by elements of ℕ^{N}. The root of T is labelled by F (χ_{0}). If a node at level i (the root is at level 0) is labelled by f, then v has one child for each N-tuple obtained by performing at most l_{i} increment and decrement operations on the components of f.

Clearly, T is finitely branching and infinite. By Lemma 2.6 there exists μ_{k} such that along any path in T of length μ_{k} starting at the root, the corresponding sequence of labels has a non-decreasing subsequence of length k. Now μ_{k} depends only on the tree T, which is unique if the label of the root and the sequence (l_{i}) are fixed. The label of the root has at most (K + 1)^{N} possibilities; hence there exists a function μ(k, M, N, K, (l_{i})), such that in every such tree in every path of length μ(k, M, N, K, (l_{i})) starting from the root, the corresponding labels have a non-decreasing sequence of length at least k.

We set B(M, N, K, (l_{i})) = μ(M +2, M, N, K, (l_{i})) and complete the proof of the lemma by arguing as in Lemma 2.7. (We have M + 2 and not M + 1 because in the lemma we want i ≠ 0.) □

Lemma 5.9 (Part 2) Let A be a counter automaton with M states and N counters. There exists a constant E = E(M, N, K, ℓ) such that if χ_{0} ⟹^{t} is an accepting K-run of A, where α(t)↾_{Σ} = γβ^{m}α (|β|, |γ| ≤ ℓ), and m ≥ E, then for infinitely many j there is an accepting run χ_{0} ⟹^{t_{j}} with α(t_{j})↾_{Σ} = γβ^{j}α.

Proof: Define the sequence (ℓ_{i}(M, N, K)) by

l_{0} = A(M, N, K);
l_{i} = A(M, N, K + ℓ_{1} + ℓ_{2} + ⋯ + ℓ_{i−1}).

Let D(M, N, K) = B(M, N, K, (ℓ_{i}(M, N, K))) and

\overline{ℓ}(M, N, K) = ∑_{i=1}^{D(M,N,K)−1} l_{i}(M, N, K).

Then, E(M, N, K) is defined by

E(M, N, K, ℓ) = \{ \begin{matrix}B(M, N, K, (ℓ)) & if N=0. \\ D(M, N, K) + E(M, N − 1, K + \overline{ℓ}(M, N, K), ℓ) & if N > 1 \end{matrix} .

(Here (ℓ) denotes the infinite sequence all of whose terms are ℓ.)

We will use induction on the number of counters to show that E as defined above meets the requirements of the lemma. Basis: If N = 0, there are no counter moves. The claim then follows from Lemma 5.8. Induction step: Assume t is minimal such that χ_{0} ⟹^{t} is an accepting K-run of A with α(t)↾_{Σ} = γβ^{m}α (m ≥ E). We may write this computation as

χ_{0} ⟹^{v_{0}} χ_{1} ⟹^{v_{1}} χ_{2} ⟹^{v_{2}} ⋯ ⟹^{v_{m}} χ_{m+1} ⟹^{w} χ_{f},

where α(v_{0}) ↾_{Σ} = γ, α(v_{i}) ↾_{Σ} = β for i ∈ [1..m] and α(w) ↾_{Σ} = α. If |v_{i}| ≤ ℓ_{i} for i ∈ [0..D(M, N, K) − 1], then the claim follows from Lemma 5.8.

Otherwise, there exists an i ∈ [0..D(M, N, K) − 1] such that |v_{i}| ≥ ℓ_{i}. Let i be the smallest with this property. By Lemma 5.7, for this i, we may write the computation on v_{i} as

χ_{i} ⟹^{v} χ′ ⟹^{v′} χ′′ ⟹^{v′′} χ_{i+1},

where Q(χ′) = Q(χ′′), F (χ′) ≤ F (χ′′), where α(v′) is nonempty but has no input symbols. Since t is minimal, we have F (χ′) < F (χ′′). Fix a counter C such that Δ_{C}(v′) > 0. Next, consider the computation after v′, that is

χ′′ ⟹^{v′′} χ_{i+1} ⟹^{v_{i+1}} χ_{i+2} ⟹^{v_{i+2}} ⋯ ⟹^{v_{m}} χ_{m+1} ⟹^{w} χ_{f}.

Here we treat C^{+} and C^{−} as elements of the input alphabet. As noted above, we may assume |vv′| ≤ ℓ_{i}. Thus, |v_{0} … v_{i−1}vv′| ≤ \overline{ℓ}(M, N, K). Also, α(v′′v_{i+1} … v_{m}w)↾_{Σ} = γ′β^{j}α, where

j ≥ E(M, N, K, ℓ) − D(M, N, K) ≥ E(M, N − 1, K + \overline{ℓ}(M, N, K), ℓ).

We apply the induction hypothesis to this computation. For infinitely many j we obtain

t′_{j} such that X′′ ⟹^{t′_{j}} is an accepting computation of A and α(t_{j})↾_{Σ} = γ′β^{j}α. Since Δ_{C}(v′) > 0, it is easily verified that for sufficiently large k and

t = v_{0}v_{1} … v_{i−1}vv^{′k}v′′t′_{j},

χ_{0} ⟹^{t} is an accepting computation of A. Since α(v′) has no input symbols, this implies that for infinitely many j, there is a t_{j} such that χ_{0} ⟹^{t_{j}} is an accepting computation of A and α(t_{j})↾_{Σ} = γβ^{j}α. □

6 Discussion

In this concluding discussion, we point out similarities and differences between our work and earlier results from the theory of vector addition systems and Petri nets. We also identify some directions for further work in developing our model of finite-state distributed systems with asynchronous communication.

Vector addition systems

An n-coordinate vector addition system (VAS) consists of a finite set of initial vectors and a finite set of transition vectors. Each initial vector is an n-tuple of natural numbers and each transition vector is an n-tuple of integers. An n-tuple of natural numbers is reachable if it can be generated from an initial vector by performing a sequence of additions with vectors from the set of transitions while ensuring that each intermediate vector generated is non-negative.

In [KM69], Karp and Miller study various decision problems for vector addition systems. They show how to associate with each VAS a finite object called its covering tree. This can be used to solve a number of other questions, including whether the set of reachable vectors of the VAS is finite. These results have immediate applicability in the theory of Petri nets because a Petri net can be represented as a VAS. Our Counter Pumping Lemma (Lemma 4.3) is similar in spirit to Karp and Miller’s covering tree result.

Petri net languages

It is well known that there is a strong connection between automata with blind counters and Petri nets [G78, J86a]. It is not difficult to show that we can go back and forth between labelled Petri nets and counter automata in such a way that given a net N and its corresponding counter automaton A, there is bijection a between the firing sequences of N and the computations of A. Thus, questions about Petri net languages can rephrased as questions about languages accepted by counter automata.

There are several ways to associate a language with a Petri net [H75, J86a]. The first is to just examine all firing sequences of the net. The second is to fix a set of final markings and look at the labels along firing sequences leading to these designated markings. The third possibility is to fix final markings but only require a firing sequence to lead to a marking which dominates a final marking rather than be exactly equal to a final marking. Following the terminology of [J86a], we designate the class of languages generated by these three definitions L, L_{0} and L_{1} respectively. When transitions are allowed to have invisible labels, the corresponding classes of languages are designated L^{λ}, L_{0}^{λ} and L_{1}^{λ} respectively.

In the setting of counter automata, the first definition corresponds to examining the set of computations of the automaton. The second definition yields a definition of accepting runs in terms of both final states and final counter values. The third definition corresponds more directly to the one we use in this paper—the final states are fixed but the final counter values are irrelevant.

In the theory of Petri net languages, a number of positive results have been established for the class L—for instance, regularity is decidable [GY80, VV80]. On the other hand, it is quite easy to exhibit languages from the class L_{1} (and hence, counter recognisable languages) where the language itself is regular but the underlying language of transitions is not. Hence the results of [GY80, VV80] do not carry over to counter recognisable languages—in fact, the problem of deciding whether a counter recognisable language is regular is open.

At the other end of the spectrum, a number of negative results have been established for the class L_{0} (and hence also L_{0}^{λ}). For instance, it is undecidable whether such a language is universal—that is, whether it consists of all strings [VV80]. However, this result crucially uses the fact that final markings must be reached exactly. The problem of deciding whether a counter recognisable language is universal is open.

Few, if any, results have been proved for the classes L_{1} and L_{1}^{λ}, which correspond most closely to counter recognisable languages. Our characterisation of the subclass closed under complementation is probably the only non-trivial result known for this class. Notice that this characterisation fails for the class L_{0}—it is possible to construct nets for both the language L_{ge} of Example 2.1 and its complement, though L_{ge} is not regular.

Counter recognisable languages and message-passing

How can we interpret our results on counter recognisable languages in terms of distributed systems for asynchronous communication? We say that an asynchronous protocol is robust if it responds “sensibly” to any sequence of interactions with the environment—in other words, for any such sequence, it either accepts the sequence as valid or terminates with an error. When we model asynchronous protocols by counter automata, the strings accepted by the automaton correspond to sequences of interactions with the environment. For a robust protocol, both the set of interactions accepted by the protocol and the set of interactions rejected by the protocol are counter recognisable. Our characterisation of the complementation-closed subset of counter recognisable languages then tells us that all robust protocols use only bounded buffers. Any messages exchanged by processes following a robust protocol can be viewed as just hand-shakes which coordinate the interaction between the different processes and the environment.

One shortcoming of our model is that we implicitly sequentialise all the interactions of a distributed system into a sequence of global interactions. It would be more satisfying to build a theory where we separate the interaction of each process and allow our automata to read n-tuples of strings, where n is the number of processes. It is not obvious how to extend the notion of a robust protocol to this setting. One possibility is to use the fact we can keep track of the latest information each process has about every other process in a message-passing system using the algorithm proposed in [MNS95]. In the theory of synchronous communication, an analogous result is the key to generating a distributed finite-state system recognising an n-tuple of strings from a global description of such a system [MS94, Z87]. We have some preliminary results in this direction.

References

[AJ93] P.A. Abdulla and B. Jonsson: Verifying programs with unreliable channels, in Proc. 8th IEEE Symp. Logic in Computer Science, Montreal, Canada (1993).

[AJ94] P.A. Abdulla and B. Jonsson: Undecidability of verifying programs with unreliable channels, in S. Abiteboul, E. Shamir (eds.), Proc. ICALP ’94, Springer LNCS 820 (1994) 316–327.

[GY80] A. Ginzburg and M. Yoeli: Vector Addition Systems and Regular Languages, J. Comput. System. Sci. 20 (1980) 277–284

[G78] S.A. Greibach: Remarks on Blind and Partially Blind One-Way Multicounter Machines, Theoret. Comput. Sci 7 (1978) 311–324.

[H75] M. Hack: Petri Net Languages, C.S.G. Memo 124, Project MAC, MIT (1975).

[J86a] M. Jantzen: Language Theory of Petri Nets, in W. Brauer, W. Reisig, G. Rozenberg (eds.), Petri Nets: Central Models and Their Properties, Advances in Petri Nets, 1986, Vol 1, Springer LNCS 254 (1986) 397–412.

[J86b] M. Jantzen: Complexity of Place/Transition Nets, in W. Brauer, W. Reisig, G. Rozenberg (eds.), Petri Nets: Central Models and Their Properties, Advances in Petri Nets, 1986, Vol 1, Springer LNCS 254 (1986) 413–434.

[KM69] R.M. Karp and R.E. Miller: Parallel Program Schemata, J. Comput. System Sci., 3 (4) (1969) 167–195.

[LT87] N.A. Lynch and M. Tuttle: Hierarchical Correctness Proofs for Distributed Algorithms, Technical Report MIT/LCS/TR-387, Laboratory for Computer Science, MIT (1987).

[L76] R.J. Lipton: The Reachability Problem Requires Exponential Space, Research Report No 62, Dept of Computer Science, Yale University (1976).

[M78] A. Mazurkiewicz: Concurrent Program Schemes and their Interpretations, Report DAIMI-PB-78, Computer Science Department, Aarhus University, Denmark (1978).

[MNS95] M. Mukund, K. Narayan Kumar and M. Sohoni: Keeping Track of the Latest Gossip in Message-Passing Systems, Proc. Structures in Concurrency Theory (STRICT), Berlin 1995, Workshops in Computing Series, Springer-Verlag (1995) 249–263.

[MS94] M. Mukund and M. Sohoni: Gossiping, Asynchronous Automata and Zielonka’s Theorem, Report TCS-94-2, School of Mathematics, SPIC Science Foundation, Madras, India (1994).

[PS88] P. Panangaden and E.W. Stark: Computations, Residuals, and the Power of Indeterminacy, in T. Lepisto and A. Salomaa (eds.), Proc. ICALP ’88, Springer LNCS 317 (1988) 439–454.

[VV80] R. Valk and G. Vidal-Naquet: Petri Nets and Regular Languages, J. Comput. System. Sci. 20 (1980) 299–325.

[Z87] W. Zielonka: Notes on Finite Asynchronous Automata, R.A.I.R.O.—Inf. Théor. et Appl., 21 (1987) 99–135.

SPIC Mathematical Institute

Internal Reports (Theoretical Computer Science)

TCS-90-1 M. Mukund: Expressiveness and Completeness of a Logic for Well

Branching Prime Event Structures.

TCS-90-2 M. Mukund and P.S. Thiagarajan: An Axiomatization of Well Branching

Prime Event Structures.

TCS-90-3 K. Lodaya, M. Mukund, R. Ramanujam, P.S. Thiagarajan: Models and

Logics for True Concurrency.

TCS-91-1 P.S. Thiagarajan (ed.): Proceedings of National Seminar on Theoretical

Computer Science, Madras, India, July 4–6, 1991.

TCS-91-2 M. Mukund: A Transition System Characterization of Petri Nets.

TCS-91-3 P.W. Hoogers, H.C.M. Kleijn, P.S. Thiagarajan: A Trace Semantics for

Petri Nets.

TCS-91-4 M. Nielsen, G. Rozenberg, P.S. Thiagarajan: Elementary Transition Sys-

tems.

TCS-91-5 M. Nielsen, G. Rozenberg, P.S. Thiagarajan: Transition Systems, Event

Structures and Unfoldings.

TCS-92-1 M. Nielsen, G. Rozenberg, P.S. Thiagarajan: Elementary Transition Sys-

tems and Refinement.

TCS-92-2 M. Mukund and M. Nielsen: CCS, Locations and Asynchronous Transi-

tion Systems.

TCS-92-3 M. Mukund: Transition System Models for Concurrency.
TCS-93-2 M. Agrawal: On the Isomorphism Problem for Weak Reducibilities.

TCS-93-3 M. Mukund and M. Sohoni: Keeping Track of the Latest Gossip: Bounded

Time-Stamps Suffice.

TCS-93-4 P.S. Thiagarajan: A Trace Based Extension of PTL.

TCS-93-5 N. Klarlund, M. Mukund, M. Sohoni: Determinizing Asynchronous Au-

tomata.

TCS-93-6 P.S. Thiagarajan: TrPTL: A Trace Based Extension of Linear Time

Temporal Logic.

TCS-93-7 M. Agrawal and V. Arvind: On Quasi-Linear Truth-Table Reductions to

P-Selective Sets.

TCS-93-8 K. Lodaya, R. Parikh, R. Ramanujam, P.S. Thiagarajan: A Logical Study of Distributed Transition Systems.

TCS-94-1 P.W. Hoogers, H.C.M. Kleijn, P.S. Thiagarajan: A Event Structure Se-

mantics for General Petri Nets.

TCS-94-2 M. Mukund and M. Sohoni: Gossiping, Asynchronous Automata and

Zielonka’s Theorem.

TCS-94-3 R. Krishnan and S. Venkatesh: Optimizing the Gossip Automaton.

TCS-94-4 M. Agrawal, R. Krishnan and S. Venkatesh: The Isomorphism Problem

for 2-DFA Reductions.

TCS-94-5 M. Agrawal and V. Arvind: Geometric Sets of Low Information Content.
TCS-95-1 M. Agrawal: Self-reducibility Versus Prunability.

TCS-95-2 M. Agrawal, P. Ramadevi and V Vinay: A New Link Invariant and its

Complexity.

TCS-95-3 M. Mukund, K. Narayan Kumar and M. Sohoni: Keeping Track of the

Latest Gossip in Message-Passing Systems.

TCS-95-4 P.S. Thiagarajan: PTL over Product State Spaces.

TCS-95-5 M. Agrawal: DSPACE(n) =^{?} NSPACE(n): A Degree Theoretic Charac-

terization.

TCS-95-6 N. Klarlund, M. Mukund, M. Sohoni: Determinizing Asynchronous Au-

tomata on Infinite Inputs.

TCS-95-7 S. Krishnamurthy, M. Mukund: Implementing Causal Ordering with

Bounded Time-stamps.

TCS-96-1 M. Mukund, P.S. Thiagarajan: Linear Time Temporal Logics over

Mazurkiewicz Traces.

TCS-96-2 M. Mukund: Finite-state Automata on Infinite Inputs.

TCS-97-1 Jesper G. Henriksen and P.S. Thiagarajan: Dynamic Linear Time Tem-

poral Logic.

TCS-97-2 P.S. Thiagarajan and I. Walukiewicz: An Expressively Complete Linear

Time Temporal Logic for Mazurkiewicz Traces.

TCS-97-3 Jesper G. Henriksen and P.S. Thiagarajan: A Product Version of Dy-

namic Linear Time Temporal Logic.

TCS-97-4 M. Mukund, K. Narayan Kumar, J. Radhakrishnan and M. Sohoni: Message-Passing Automata and Asynchronous Communication.

Copies of reports can be ordered from the following address:

SPIC Mathematical Institute 92, G.N. Chetty Road T. Nagar Madras 600 017

 Email: office@smi.ernet.in