arXiv:1701.02808v1 [cs.FL] 10 Jan 2017

University of Warsaw

Abstract. The regular separability problem asks, for two given languages, if there exists a regular language including one of them but disjoint from the other. Our main result is decidability, and PSpacecompleteness, of the regular separability problem for languages of one counter automata without zero tests (also known as one counter nets). This contrasts with undecidability of the regularity problem for one counter nets, and with undecidability of the regular separability problem for one counter automata, which is our second result.

1

Introduction

We mainly focus on separability problems for languages of ﬁnite words. We say that a language K is separated from another language L by a language S, if K ⊆ S and L ∩ S = ∅. For two families of languages F and G, the F separability problem for G asks, for two given languages K, L ∈ G over the same alphabet, whether K is separated from L by some language from F . In this paper we mainly consider the class F of regular languages (thus using the term regular separability). As regular languages are closed under complement, K is separated from L by a regular language if, and only if L is separated from K by a regular language. In such case we shortly say that K and L are regular separable. As the class G we consider languages of one counter automata (NFA extended with a non-negative counter that can be incremented, decremented and tested for zero), or its subclass – the languages of one counter nets (one counter automata without zero tests). Motivation and context. Separability is a classical problem in formal languages. It was investigated most extensively for G the class of regular languages, and for F a suitable subclass thereof. Since regular languages are eﬀectively closed under complement, the F separability problem is in that case a generalization of the F characterization problem, which asks whether a given language belongs to F : indeed, L ∈ F if and only if L is separated from its complement by some language from F . Separability problems for regular languages were investigated since a long time using a generic connection established by Almeida [1] between proﬁnite semigroup theory and separability. Recently it attracted a lot of attention also outside algebraic community, which resulted in establishing the decidability of F separability for the family F of separators being, among others, – the piecewise testable languages [9, 19] 1

– the locally and locally threshold testable languages [18], – the languages deﬁnable in ﬁrst order logic [21], – the languages of certain higher levels of the ﬁrst order hierarchy [20]. The ﬁrst result has been recently generalized to ﬁnite ranked trees [13]. Separability of non-regular languages attracted little attention till now. The reason for this may be twofold. First, for regular languages one can use standard algebraic tools, like syntactic monoids, and indeed most of the results have been obtained using algebraic techniques. Second, the few known negative results on separability of non-regular languages are strongly discouraging. To start oﬀ, some strong intractability results have been known already since 70’s, when Szymanski and Williams proved that regular separability of context-free languages is undecidable [24]. Later Hunt [14] strengthened this result: he showed that F separability of context-free languages is undecidable for every class F containing all definite languages, i.e., ﬁnite Boolean combinations of languages of the form wΣ ∗ for w ∈ Σ ∗ . This is a very weak condition, hence the result of Hunt suggested that nothing nontrivial can be done outside regular languages with respect to separability problems. Furthermore, Kopczy´ nski has recently shown that regular separability is undecidable even for languages of visibly pushdown automata [16], thus strengthening the result by Szymanski and Williams once more. On the positive side, piecewise testable separability has been shown decidable for context-free languages, languages of vector addition systems with states (VASS languages), and some other classes of languages [10]. This inspired us to start a quest for decidable cases beyond regular languages. Once beyond regular languages, the regular separability problem seems to be the most intriguing. VASS languages is a well-known class of languages, for which the decidability status of the regular separability problem is unknown. A few positive results related to this problem have been however obtained recently. First, decidability of unary (and modular) separability of reachability sets1 of VASS was shown in [8]; the problem is actually equivalent to regular separability of commutative closures of VASS languages. Second, decidability of regular separability of languages of Parikh automata was shown recently in [7]. Parikh automata recognize exactly the same languages as integer-VASS (a variant of VASS where one allows negative counter values [15, 5]), and therefore are a subclass of VASS languages. The open decidability status of regular separability of VASS languages is our main motivation in this paper. A more general goal is understanding for which classes of languages regular separability problem is decidable. Our contribution. We consider the regular separability problem for languages of one counter automata (with zero test) and its subclass, namely one counter nets (without zero test); the latter model is exactly VASS in dimension 1. The two models we call shortly OCA and OCN, respectively. Our main result is decidability of the regular separability problem for languages of one counter nets. 1

Note that these are sets of vectors, not words.

2

Moreover, we determine the exact complexity of the problem, namely PSpacecompleteness. For complexity estimations we assume a standard encoding of OCA (or OCN) and their conﬁgurations; in particular we assume binary encoding of integers appearing in the input. Theorem 1. Regular separability of languages of OCN is PSpace-complete. Our approach to prove decidability is by regular over-approximation: for every OCN language L there is a decreasing sequence of (computable) regular languages over-approximating L, such that two OCN languages are regular separable if, and only if some pair of their approximants is disjoint. Furthermore, the latter condition can be reduced to a kind of reachability property of the cross-product of two OCN, and eﬀectively checked in PSpace by exploiting effective semi-linearity of the reachability set of the cross-product. Our PSpace lower bound builds on PSpace-hardness of bounded non-emptiness of OCA [12]. It is interesting to compare the regular separability problem with the regularity problem, which asks whether a given language is regular. For every class G eﬀectively closed under complement, regular separability is a generalization of ¯ are regular separable. It turns regularity, as L is regular if, and only if L and L however that regularity of OCN languages can not be reduced to regular separability: while we prove regular separability decidable, the regularity problem is undecidable for languages of OCN [25, 26]. As our second main contribution, we show that adding zero tests leads to undecidability, for any separator language class containing all deﬁnite languages. In particular, regular languages are an example of such class. Theorem 2. For every language class F containing all definite languages, the F separability problem for languages of OCA is undecidable. Our argument is inspired by the undecidability proof by Hunt [14]: we show, roughly speaking, that every decidable problem reduces in polynomial time to the separability problem for OCA. Organization. In Section 2 we deﬁne the models of OCA and OCN, then Sections 3–5 are devoted to the proof of Theorem 1, and ﬁnally Section 6 contains the proof of Theorem 2. The proof of Theorem 1 is factorized as follows: in Section 3 we introduce the regular over-approximation of OCN languages, in Section 4 we provide a PSpace procedure for testing the disjointness property of approximants, as discussed above, and in Section 5 we give a PSpace lower bound. The next Section 6 contains a proof of undecidability of regular separability for OCA. The last section 7 contains some concluding remarks, including the discussion of undecidability of the regularity problem for OCN.

2

One counter automata and nets

In order to ﬁx notation we start by recalling ﬁnite automata, in a speciﬁcally chosen variant convenient for us later, when working with one counter automata. 3

A nondeterministic finite automaton (NFA) A = (Q, q0 , qf , T ) over a ﬁnite alphabet Σ consists of a ﬁnite set of control states Q, distinguished initial and ﬁnal states q0 , qf ∈ Q (for convenience we assume here, w.l.o.g., a single ﬁnal state), and a set of transitions T ⊆ Q × Σε × Q, where Σε = Σ ∪ {ε}. For a word v ∈ (Σε )∗ , let v|Σ be the word obtained by removing all occurrences of ε. A run of A over a word w ∈ Σ ∗ is a sequence of transitions of the form (p0 , a1 , p1 ), (p1 , a2 , p2 ), . . . , (pn−1 , an , pn ) such that (a1 . . . an )|Σ = w. The run is accepting if p0 = q0 and pn = qf . The language of A, denoted L(A), is the set of all words w over which A has an accepting run. Languages of NFA are called regular. One counter automata and nets. In brief, a one counter automaton (OCA) is an NFA with a non-negative counter, where we allow for arbitrary changes of the counter value in one step. Formally, an OCA is a tuple A = (Q, α0 , αf , T, T=0 ), where Q are control states as above. A configuration (q, n) ∈ Q × N of A consists of a control state and a non-negative counter value. There are two distinguished conﬁgurations, the initial one α0 = (q0 , n0 ) and the ﬁnal one αf = (qf , nf ). The ﬁnite set T ⊆ Q × Σε × Q × Z, contains transitions of A. A transition (q, a, q ′ , z) can be ﬁred in a conﬁguration α = (q, n) if n + z ≥ 0, leading to a new conﬁguration a α′ = (q ′ , n + z). We write α −→ α′ if this is the case. Finally, the set T=0 ⊆ Q×Σε ×Q contains zero tests. A zero test (q, a, q ′ ) can be ﬁred in a conﬁguration α = (q, n) only if n = 0, leading to a new conﬁguration α′ = (q ′ , n). Again, we a write α −→ α′ if this is the case. A run of an OCA over a word w ∈ Σ ∗ is a sequence of transitions and zero tests of the form an a2 a1 αn . . . −→ α1 −→ α0 −→ w

such that (a1 . . . an )|Σ = w; we brieﬂy write α0 −→ αn if this is the case, and α0 −→ αn if a word w is irrelevant. The run is accepting if α0 is the initial conﬁguration of A, and αn is the ﬁnal one. The language of A, denoted L(A), is the set of all words w over which A has an accepting run. A one counter net (OCN) is an OCA without zero tests, i.e., one with T=0 = ∅. We drop the component T=0 and denote OCN as (Q, α0 , αf , T ). In other words, an OCN is exactly a VASS in dimension 1. Example 3. Consider two OCN languages over the alphabet {a, b}: K = {an bn | n ∈ N}

L = {an bn+1 | n ∈ N}.

Here is an example regular language separating K from L: R = {an bm | n ≡ m mod 2}. Indeed, R includes K and is disjoint with L. 4

Other modes of acceptance. We brieﬂy discuss other possible modes of acceptance of OCA. First, consider a variant of OCA with a ﬁnite set of initial conﬁgurations, and a ﬁnite set of ﬁnal ones. This variant can be easily simulated by OCA as deﬁned above. Indeed, add two fresh states q0 , qf , and ﬁx the initial and ﬁnal conﬁgurations α0 = (q0 , 0) and αf = (qf , 0). Moreover, add transitions enabling to go from α0 to every of former initial conﬁgurations, and symmetrically add transitions enabling to go from every of former ﬁnal conﬁgurations to αf . The above simulation reveals that w.l.o.g. we can assume that the counter values n0 and nf in the initial and ﬁnal conﬁgurations are 0. This will be implicitly assumed in the rest of the paper. Yet another possibility is accepting solely by control state: instead of a ﬁnal conﬁguration αf = (qf , nf ), such an OCA would have solely a ﬁnal control state qf , and every run ending in a conﬁguration (qf , n), for arbitrary n, would be considered accepting. Again, this variant is easily simulated by our model: it is enough to add a transition (qf , ε, qf , −1) decrementing the counter in the ﬁnal state, and to ﬁx the ﬁnal conﬁguration as (qf , 0). Finally, note that all the simulations discussed above work for OCN as well. In particular, in the sequel we may assume, w.l.o.g., that the counter values in initial and ﬁnal conﬁgurations of OCN are 0.

3

Regular over-approximation of OCN

For an OCN A and n > 0, we are going to deﬁne an NFA An which we call n-approximation of A. As long as the counter value is below n, the automaton An stores this value exactly (we say then that An is in low mode); if the counter value exceeds n, the automaton An only stores the remainder of the counter value modulo n (we say then that An is in high mode). Thus An can pass from low mode to high one; but An can also nondeterministically decide to pass the other way around, from high to low mode. Let Q be the state space of A, and let (q0 , 0) and (qf , 0) be its initial and ﬁnal conﬁgurations. As the state space of An we take the set Qn = Q × {0, . . . , n − 1} × {low, high}. The initial and ﬁnal state of An are (q0 , 0, low) and (qf , 0, low), respectively. Every transition (q, a, q ′ , z) of A induces a number of transitions of An , as deﬁned below (for any c satisfying 0 ≤ c < n): (q, c, low), a, (q, c+z, low) if 0 ≤ c+z < n (q, c, low), a, (q, (c+z) mod n, high) if n ≤ c+z (q, c, high), a, (q, (c+z) mod n, low) if c+z < 0 (q, c, high), a, (q, (c+z) mod n, high) . Note that passing from high mode to low one is only possible if the counter value (modulo n) drops, after an update, strictly below 0; in particular, this requires z < 0. 5

Example 4. Recall the languages K and L from Example 3, and consider an OCN A recognizing K that has two states q0 , qf , and three transitions: (q0 , a, q0 , +1) (q0 , ε, qf , 0) (qf , b, qf , −1). The 2-approximating automaton A2 has 8 states {q0 , qf }×{0, 1}×{low, high}. In state (q0 , 1, low) on letter a, the automaton is forced to change the mode to high; symmetrically, in state (qf , 0, high) on letter b, the automaton can change its mode back to low: (q0 , 1, low), a, (q0 , 0, high) (qf , 0, high), b, (qf , 1, low) . Otherwise, the mode is preserved by transitions; for instance, in high mode the automaton changes the state irrespectively of the input letter: for every q ∈ {q0 , qf }, x ∈ {a, b} and c ∈ {0, 1}, there is a transition (q, c, high), x, (q, 1 − c, high) . The language recognized by A2 is {an bm | (n = m < 2) ∨ (n, m ≥ 2 ∧ n ≡ m mod 2)}. According to the deﬁnition above, the automaton An can oscillate between low and high mode arbitrarily many times. Actually, as we argue below, it is enough to allow for at most one oscillation. Proposition 5. For every run of An between two states in high mode, there is a run over the same word between the same states which never exits the high mode. Proof. Indeed, observe that if T contains any of the following transitions (q, m, low), a, (q ′ , m′ , low) (q, m, low), a, (q ′ , m′ , high) (q, m, high), a, (q ′ , m′ , low) then T necessarily contains also the transition (q, m, high), a, (q ′ , m′ mod n, high) . Thus every run oscillating through high and low modes that starts and ends in high mode, can be simulated by a one that never exits high mode. ⊓ ⊔ A run of an OCN A we call n-low, if the counter value is strictly below n in all conﬁgurations of the run. Proposition 6 below characterizes the language of An in terms of runs of An , and will be useful for proving the Approximation Lemma below. Then Corollary 7, its direct consequence, summarizes some properties of approximation useful in the sequel. 6

Proposition 6. Let A = (Q, (q0 , 0), (qf , 0), T ) be an OCN, and let n > 0. Then w ∈ L(An ) iff (a) either A has an n-low run over w, (b) or w factorizes into w = wpref wmid wsuff , such that A has the following runs w

pref (q, n + d) (q0 , 0) −→

w

mid (q ′ , c′ n + d′ ) (q, cn + d) −→

′

(1)

wsuff

′

(q , n + d ) −→ (qf , 0), for some states q, q ′ ∈ Q and natural numbers c, c′ ≥ 1 and d, d′ ≥ 0. Proof. We start with the ’if’ direction. If there is an n-low run over w in A then clearly w ∈ L(An ). Otherwise, suppose that w = wpref wmid wsuff and the words wpref , wmid and wsuff admit the runs as stated in (1) above. Then clearly An admit the following runs: w

pref (q, d mod n, high) (q0 , 0, low) −→

w

mid (q ′ , d′ mod n, high) (q, d mod n, high) −→

w

suff (qf , 0, low) (q ′ , d′ mod n, high) −→

w

and thus (q0 , 0) −→ (qf , 0) in An as required. For the ’only if’ direction, suppose w ∈ L(An ). If An has a run over w that never exits low mode, then clearly A has an n-low run over w. Otherwise, consider any run of An over w. Distinguish the ﬁrst and the last conﬁguration in high mode along this run, say (q, d, high) and (q ′ , d′ , high). The two conﬁgurations determine a factorization of the word w into three parts w = wpref wmid wsuff such that An admit the following runs: w

pref (q, d, high) (q0 , 0, low) −→

w

mid (q ′ , d′ , high) (q, d, high) −→

w

suff (qf , 0, low). (q ′ , d′ , high) −→

The ﬁrst and the last run imply the ﬁrst and the last run in (1). For the middle one, we may assume (w.l.o.g., by Proposition 5) that An never exits high mode, which implies immediately existence of the middle run in (1). ⊓ ⊔ Corollary 7. Let A be an OCN and let m, n > 0. Then (a) L(A) ⊆ L(An ), (b) L(An ) ⊆ L(Am ) if m | n. Proof. The ﬁrst inclusions follow easily by the characterization of Proposition 6. The second one is easily shown by deﬁnition of n-approximation. ⊓ ⊔ Now we state and prove Approximation Lemma, which is the crucial property of approximation. In the sequel we will strongly rely on direct consequences of this lemma, formulated as Corollaries 9 and 10 below. 7

Lemma 8 (Approximation Lemma). For an OCN A, the following conditions are equivalent: (a) L(A) is empty, (b) L(An ) is empty, for some n > 0. Proof. Clearly (b) implies (a), by Corollary 7(a). In order to prove that (a) implies (b), ﬁx A = (Q, (q0 , 0), (qf , 0), T ) and suppose that the languages L(An ) are non-empty for all n > 0; our aim is to show that L(A) is non-empty either. In the sequel we do not need the non-emptiness assumption for all n; it will be enough to use the assumption for some ﬁxed n computed as follows. Let |Q| be the number of states of A and dA be the maximal absolute value of integer constants appearing in transitions T of A. Then let K = |Q| · dA , and let n = K! Let w be a ﬁxed word that belongs to L(An ). Our aim is to produce a word w′ that belongs to L(A), by a pumping in the word w; the pumping will allow to make a run of An into a correct run of A. As w ∈ L(An ), by Proposition 6 we learn that w satisﬁes one of conditions (a), (b). If w satisﬁes (a) then w′ = w ∈ L(A) as required. We thus concentrate, from now on, on the case when w satisﬁes condition (b) in Proposition 6. Let’s focus on the ﬁrst (ﬁxed from now on) run of A in (1), namely w

pref (q, n + d), (q0 , 0) −→

for some preﬁx wpref of w and d ≥ 0. This run starts with the counter value 0, and ends with the counter value at least n. We are going to analyze closely the preﬁx of the run that ends immediately before the counter value exceeds K for the ﬁrst time; denote this preﬁx by ρ. A conﬁguration (q, m) in ρ we call latest if the counter value stays strictly above m in all the following conﬁgurations in ρ. In other words, a latest conﬁguration is the last one in ρ where the counter value is at most m. A crucial but easy observation is that the diﬀerence of counter values of two consecutive latest conﬁgurations is at most dA . Therefore, as K has been chosen large enough, ρ must contain more than |Q| latest conﬁgurations. By a pigeon hole principle, there must be a state of A, say q, that appears in at least two latest conﬁgurations. In consequence, for some inﬁx v of wpref , the OCN A has a run over v of the form v

(q, m) −→ (q, m′ ),

for some m < m′ ≤ m + K.

As a consequence, the word v can be repeated an arbitrary number of times, preserving correctness of the run but increasing the ﬁnal counter value. Recall that the ﬁnal counter value of ρ is n + d, while we would like to achieve cn + d (for c in Proposition 6). Modify the word wpref by adding (c − 1) · n/(m′ − m) ′ repetitions of the word v, thus obtaining a new word wpref such that A has a run w′

pref (q0 , 0) −→ (q, cn + d).

8

(2)

In exactly the same way we modify the suﬃx wsuff of w, thus obtaining a ′ word wsuff over which the OCN A has a run w′

suff (q ′ , c′ n + d′ ) −→ (qf , 0).

(3)

′ ′ By concatenation we obtain a word w′ = wpref wmid wsuff which is accepted by A, by composition of the run (2), the middle run in (1), and the run (3). Thus L(A) is non-empty, as required. ⊓ ⊔

Corollary 9. For an OCN A and a regular language R, the following conditions are equivalent: (a) L(A) and R are disjoint, (b) L(An ) and R are disjoint, for some n > 0. Proof. Fix an OCN A = (Q, (q0 , 0), (qf , 0), T ) and an NFA B = (P, p0 , pf , U ) recognizing the language R. For convenience we assume here that A has an εtransition of the form (q, ε, q, 0) in every state q ∈ Q, and B has a self-loop ε-transitions (p, ε, p) in every state p ∈ P . We will use the synchronized product A × B of OCN A and NFA B, which is the OCN deﬁned by A × B = Q × P, ((q0 , p0 ), 0), ((qf , pf ), 0), V , where a transition (q, p), a, (q ′ , p′ ), z ∈ V if (q, a, q ′ , z) ∈ T and (p, a, p′ ) ∈ U ). Observe that the synchronized product construction commutes with napproximation: up to isomorphism of ﬁnite automata, (A × B)n = An × B.

(4)

Condition (a) in Corollary 9 is equivalent to emptiness of the product A × B which, by Approximation Lemma applied to A × B, is equivalent to emptiness of the left automaton in (4), for some n. Therefore condition (a) is also equivalent to emptiness of the right automaton in (4), for some n. Finally, the latter condition is equivalent to condition (b). ⊓ ⊔ Corollary 10. For two OCN A and B, the following conditions are equivalent: (a) L(A) and L(B) are regular separable, (b) L(An ) and L(B) are disjoint, for some n > 0, (c) L(An ) and L(Bn ) are disjoint, for some n > 0. Proof. In order to prove that (a) implies (b), suppose that a regular language R separates L(B) from L(A), i.e., R includes L(B) and is disjoint from L(A). By Corollary 9 we learn that for some n > 0, R and An are disjoint. Thus necessarily L(B) and L(An ) are disjoint too. To show that (b) implies (c) use Corollary 9 for OCN B and regular language L(An ). We get that there exists m > 0 such that L(Bm ) and L(An ) are disjoint. Then using Corollary 7(b) we have that L(Anm ) and L(Bnm ) are disjoint as well. Finally, (c) easily implies (a), as any of the regular languages L(An ), L(Bn ) can serve as a separator (Corollary 7(a) is used here). ⊓ ⊔ 9

Our decision procedure for OCN, to be presented in the next section, will perform an eﬀective testing of condition (b) in Corollary 10. Remark 11. Interestingly, exactly the same notion of approximation can be deﬁned for OCA as well. Even if Propositions 5 and 6 are no more valid for OCA, all other facts proved in this section still hold for this more general model, in particular Approximation Lemma and Corollaries 9 and 10. Confronting this with undecidability of regular separability for OCA (which we prove in Section 6) leads to a conclusion that the characterizations of Corollary 10 are not eﬀectively testable in case of OCA, while they are in case of OCN.

4

PSPACE algorithm

In this section we prove the PSpace upper bound of Theorem 1. All the PSpace complexity statements below are understood with respect to the size of the two input OCN, under binary encoding of integers. The proof splits into two parts. In the ﬁrst part (up to Remark 14) we reduce the (non-)separability problem to a kind of reachability property in the crossproduct of A and B. In the second (more technical) part we concentrate on testing this reachability property in PSpace. Vector addition systems with states. We start by recalling the notion of integer vector addition systems with states (integer-VASS). For d > 0, a ddimensional integer-VASS V = (Q, T ), or d-integer-VASS, consists of a ﬁnite set Q of control states, and a ﬁnite set of transitions T ⊆ Q × Zd × Q. A conﬁguration of V is a pair (q, v) ∈ Q × Zd consisting of a state and an integer vector. Note that we thus allow, in general, negative values in conﬁguration (this makes a diﬀerence between integer-VASS and VASS); however later we will typically impose non-negativeness constraints on a selected subset of coordinates. A dinteger-VASS V determines a step relation between conﬁgurations: there is a step from (q, v) to (q ′ , v ′ ) if T contains a transition (q, z, q ′ ) such that v ′ = v + z. We write (q, v) −→ (q ′ , v ′ ) if there is a sequence of steps leading from (q, v) to (q ′ , v ′ ), and say that (q ′ , v ′ ) is reachable from (q, v) in V. Cross-product operation. We will use a cross-product operation over one counter nets. For two OCN A = (Q, α0 , αf , T ) an B = (P, β0 , βf , U ), their crossproduct A ⊗ B is a 2-integer-VASS whose states are pairs of states Q × P of A and B, respectively, and whose transitions contain all triples (q, p), (z, v), (q ′ , p′ ) such that there exists a ∈ Σε with (q, a, q ′ , z) ∈ T and (p, a, p′ , v) ∈ U . (For convenience we assume here that every OCN has an ε-transition of the form (q, ε, q, 0) in every control state q.) Note that A ⊗ B is unlabeled — the alphabet letters are only used to synchronize A and B — and allows, contrarily to A and B, for negative values on both coordinates. Moreover note that there is no distinguished initial or ﬁnal conﬁguration in an integer-VASS. 10

We will later need to impose a selective non-negativeness constraint on values of conﬁgurations. For a d-integer-VASS V and a sequence C1 , . . . , Cd , where Ci = N or Ci = Z for each i, by V (C1 , . . . , Cd ) we mean the transition system of V truncated to the subset Q × C1 × . . . × Cd ⊆ Q × Zd of conﬁgurations. For instance, (A ⊗ B)(N, N) diﬀers from A ⊗ B by imposing the non-negativeness constraint on both coordinates, and is thus a 2-VASS. On the other hand, in (A ⊗ B)(Z, N) the counter of A can get arbitrary integer values while the counter of B is restricted to be non-negative. Disjointness assumption. Fix for the rest of this section two input OCN A = (Q, (q0 , 0), (qf , 0), T ) and B = (P, (p0 , 0), (pf , 0), U ), and let V = A ⊗ B be their cross-product. If the intersection of L(A) and L(B) is non-empty, the answer to the separability question is obviously negative. We may thus consider only input OCN A and B with L(A) and L(B) are disjoint. This is eligible as the disjointness can be eﬀectively checked in PSpace. Indeed, the intersection of L(A) and L(B) is nonempty if, and only if (q0 , p0 ), 0, 0 −→ (qf , pf ), 0, 0 in the 2-VASS V(N, N), which can be checked in PSpace by the result of [4]. Assumption 12 In the sequel, w.l.o.g., we assume that L(A) and L(B) are disjoint. Our strategy is to reduce regular separability of A and B to (a kind of) reachability property in their cross-product V, and then to encode this property using (multiple) systems of linear Diophantine equations. The number of systems will not be polynomial, however they will be all enumerable in polynomial space. Using the enumeration, our decision procedure will boil down to checking a suitable property of solution sets of these system. Reduction to reachability in V. Recall Corollary 10(b) which characterizes regular non-separability by non-emptiness of the intersection of L(An ) and L(B), for all n > 0, which, roughly speaking, is equivalent to a reachability property in the cross-product of NFA An and the OCN B, for all n > 0. We are going now to internalize the quantiﬁcation over all n, by transferring the reachability property to the cross-product V of the two OCN A and B. For convenience we introduce the following terminology. For n > 0 we say that V admits n-reachability (or n-reachability holds in V) if there are q, q ′ ∈ Q, p, p′ ∈ P , m, m′ ≥ n, l, l′ ≥ 0 and m′′ ∈ Z such that m′′ = m′ mod n and (a) (q0 , p0 ), 0, 0 −→ (q, p), m, l in V(N, N), (b) (q, p), m, l −→ (q ′ , p′ ), m′′ , l′ in V(Z, N), ′ ′ ′ ′ (c) (q , p ), m , l −→ (qf , pf ), 0, 0 in V(N, N). The n-reachability in V diﬀers in three respect from ordinary reachability (q0 , p0 ), 0, 0 −→ (qf , pf ), 0, 0 in V(N, N). First, we require two intermediate values of the counter in A, namely m, m′ , to be at least n. Second, in the middle part we allow the 11

counter of A to be negative. Finally, we allow for a mismatch between m′ and m′′ . Thus n-reachability does not imply non-emptiness (q0 , 0) −→ (qf , 0) of A. On the other hand, n-reachability does imply non-emptiness (p0 , 0) −→ (pf , 0) of B. Proposition 13. A and B are not regular separable if, and only if V admits n-reachability for all n > 0. Proof. Using the characterization of Corollary 10(b), it suﬃces to show that for every n > 0, L(An ) ∩ L(B) 6= ∅ if, and only if V admits n-reachability. Fix n > 0 in the sequel. For the ,,only if” direction, let w ∈ L(An ) ∩ L(B). As w ∈ L(An ), we may apply Proposition 6. Note that the condition (a) of Proposition 6 surely does not hold, as we know that w ∈ / L(A); therefore condition (b) must hold for some states q, q ′ ∈ Q and natural numbers c, c′ ≥ 1 and d, d′ ≥ 0. Put m := n + d, m′ := n + d′ and m′′ := m′ + (c′ − c + 1)n (recall that m′′ may be negative). As w ∈ L(B), the corresponding states p, p′ and counter values l, l′ can be taken from the corresponding two positions in an accepting run of B over w. The chosen states q, q ′ , p, p′ and integer values m, m′ , l, l′ , k prove n-reachability in V, as required. For the ”if” direction suppose that V admits n-reachability, and let wpref , wmid and wsuff be some words witnessing the conditions (a)–(c) of n-reachability. In particular, this implies w

mid (q ′ , m′′ + (c − 1)n) in A (q, m + (c − 1)n) −→

(5)

for c ≥ 1 large enough. This also implies that the word w = wpref wmid wsuff belongs to L(B). We will prove that w also belongs to L(An ), by demonstrating that the factorization w = wpref wmid wsuff satisﬁes the condition (2) in Proposition 6. Indeed, for d := m − n, d′ := m′ − n, we obtain then runs over mpref and msuff as required in (2) in Proposition 6. In order to get a run over wmid , we take c ≥ 1 large enough so that (5) holds; for c′ := c + (m′′ − m′ )/n, (5) rewrites to wmid (q ′ , c′ n + d′ ) in A, (q, cn + d) −→ ⊓ ⊔

as required.

Building on Proposition 13, we are going to design a decision procedure to check whether V admits n-reachability for all n > 0. To this end we slightly reformulate n-reachability, using the following relations expressing the conditions (a)–(c) of n-reachability: ′

2 midpp qq′ ⊆ N × Z × N,

prefpq , suffpq ⊆ N2 ,

for q, q ′ ∈ Q and p, p′ ∈ P , deﬁned as follows: prefpq (m, l) ⇐⇒ (a) holds ′

′′ ′ midpp qq′ (m, l, m , l ) ⇐⇒ (b) holds ′

suffpq′ (m′ , l′ ) ⇐⇒ (c) holds. 12

(6)

Let R ⊆ N2 × Z contain all triples (m, m′ , x) satisfying the following formula: there exist q, q ′ ∈ Q, p, p′ ∈ P, l, l′ ∈ N, m′′ ∈ Z s. t. ′

′′ ′ prefpq (m, l) ∧ midpp qq′ (m, l, m , l ) ∧ ′ suffpq′ (m′ , l′ )

′′

(7)

′

∧ x=m −m .

Then n-reachability is equivalent to saying that some (n1 , n2 , n3 ) ∈ R satisﬁes n1 , n2 ≥ n

and

n|n3 .

(8)

Any triple (n1 , n2 , n3 ) satisfying the condition (8) we call n-witness in the sequel. In this terminology, our algorithm is to decide whether R contains n-witnesses for all n > 0. Semi-linear sets. For a set P ⊆ Zl of vectors, let P ∗ ⊆ Zl contain all vectors that can be obtained as a ﬁnite sum, possibly the empty one, and possibly with repetitions, of vectors from P . In other words, P ∗ is the set of non-negative linear combinations of vectors from P . Linear sets are sets of the form L = {b} + P ∗ , where b ∈ Zl , P is a ﬁnite subsets of Zl , and addition + is understood elementwise. Thus L contains sums of the vector b and a vector from P ∗ . The vector b is called base, and vectors in P periods; we write shortly b + P ∗ . Finite unions of linear sets are called semi-linear. Remark 14. For decidability, we are going to observe that all the sets appearing in (7) are eﬀectively semi-linear. Indeed, prefpq is essentially the reachability set of a 2-VASS, and thus eﬀectively semi-linear [4], and likewise for suffpq ; ′

and eﬀective semi-linearity of midpp qq′ can be derived from Parikh theorem (see, e.g., Lemma 3.4 in [11]). In consequence, the set R is eﬀectively semi-linear too. Thus non-separability reduces to checking if a given semi-linear set contains nwitnesses for all n > 0. However, in order to get tight PSpace upper bound, we need to provide suitable estimations on representation size of semi-linear sets. To this aim we introduce PSpace-enumerable sets. PSpace-enumerable sets. Recall that complexity estimations are with respect to the sizes of the input OCN A and B. For a ﬁnite set of vectors P , we say that an algorithm enumerates P if it computes consecutive elements of a sequence p1 , . . . , pm , possibly with repetitions, such that P = {p1 , . . . , pm }; in other words, every element of P appears at least once in the sequence, but no other element does. An algorithm enumerates a linear set L = b + P ∗ if it ﬁrst computes b and then enumerates P . If there is a polynomial space algorithm which enumerates L, the set L is called PSpace-enumerable. A semi-linear set S we call PSpaceenumerable if for some sequence of linear sets L1 , . . . , Lk such that S = L1 ∪ . . . ∪ Lk , there is a polynomial space algorithm that ﬁrst enumerates L1 , then enumerates L2 , and so on, and ﬁnally enumerates Lk . In particular, this means that for some 13

polynomial bound N , every base and every period can be stored using at most N bits. Propositions 15 and 16 below state that all the sets appearing in (7) are PSpace-enumerable. The next Proposition 17, being their direct consequence, say the same about the set R; it will be the cornerstone of our decision procedure. Proofs of the propositions are postponed towards the end of this section. Proposition 15. For every q ∈ Q and p ∈ P , the sets prefpq and suffpq are PSpace-enumerable. ′

Proposition 16. For every q, q ′ ∈ Q and p, p′ ∈ P , the set midpp qq′ is PSpaceenumerable. Proposition 17. The set R is PSpace-enumerable. Proof. Recall the deﬁnition (7) of the set R as a projection of a conjunction of constraints: there exist q, q ′ ∈ Q, p, p′ ∈ P, l, l′ ∈ N, m′′ ∈ Z s. t. ′

′′ ′ prefpq (m, l) ∧ midpp qq′ (m, l, m , l ) ∧ ′

suffpq′ (m′ , l′ ) ∧ x = m′′ − m′ . We are going to prove that R is PSpace-enumerable. The algorithm enumerates quadruples of states q, q ′ , p, p′ . For each ﬁxed quadruple, it enumerates (by ′ p Propositions 15 and 16) component linear sets of prefpq , midpp qq′ and suffq . Thus it is enough to consider three ﬁxed PSpace-enumerable linear sets Lpref = bpref + Ppref ∗ ⊆ prefpq ⊆ N2 ′

2 Lmid = bmid + Pmid ∗ ⊆ midpp qq′ ⊆ N × Z × N

Lsuff = bsuff + Psuff ∗ ⊆ suffpq ⊆ N2 . We now treat each of these linear sets as a system of linear Diophantine equations. For instance, if Ppref = {p1 , . . . , pk }, all pairs (x, y) ∈ Lpref are described by two equations (xpref , ypref ) = bpref + p1 x1 + . . . + pk xk ,

(9)

for fresh variables x1 , . . . , xk . Note that the number of variables is exponential, but the number of equations is constant, namely equal two. The same can be done with two other linear sets, yielding 6 more equations involving 6 vari′ ables xmid , ymid , x′mid , ymid , xsuff , ysuff , plus exponentially many other fresh variables. Points in Lsuff are represented as (xsuff , ysuff ), while points in Lmid as ′ ). (Since we only consider non-negative solutions of systems (xmid , ymid , x′mid , ymid of equations, in case of Lmid two separate cases should be considered, depending on whether the ﬁnal value x′mid is non-negative or not. For simplicity we only 14

consider here the case when it is non-negative.) In addition, we add the following equations (and one variable x): xpref = xmid ypref = ymid ′ ymid = ysuff x = x′mid − xsuff . In total, we have a system U of 12 equations (8 mentioned before and 4 presented above) involving exponentially many variables, including these 9 variables ′ xpref , ypref , xmid , ymid , x′mid , ymid , xsuff , ysuff , x.

(10)

The value of 3 of them is relevant for us, namely xpref , xsuff and x. We claim that the projection of the solution set sol(U) onto these 3 relevant coordinates is PSpace-enumerable. To prove this, we use a reﬁnement of Lemma 24, which also follows from Prop. 2 in [6]: Lemma 18. sol(U) = B + P ∗ , with every base b ∈ B and period p ∈ P bounded by N , for a computable bound N ∈ N polynomial in the number of variables in U and maximal absolute values of coefficients in U, but exponential in the number of equations in U. By Lemma 18 we know that the solution set of U is of the form B + P ∗ , for all bases b ∈ B and all periods p ∈ P bounded exponentially. Hence each number appearing in a base or a period is representable in polynomial space; the same applies to the projection onto the 3 relevant coordinates. Finally, observe that the projections of the sets B and P onto the 3 relevant coordinates can be enumerated in polynomial space. Indeed, in order to check whether a vector in N3 is (the projection of) a B or P , we proceed similarly as in the proof of Proposition 15: the algorithm ﬁrst guesses values of other 6 variables among (10), and then guesses the values of other (exponentially many) variables on-line, in the course of enumerating the coeﬃcients pi (cf. (9)); the latter is possible as the sets Lpref , Lmid and Lsuff are PSpace-enumerable. ⊓ ⊔ The set R is therefore a ﬁnite union of linear sets, R = L1 ∪ . . . ∪ Lk ,

(11)

each of them being PSpace-enumerable. The next lemma allows us to consider each of the linear sets separately: Lemma 19. If a finite union X1 ∪ . . . ∪ Xk ⊆ N2 × Z contains n-witnesses for all n > 0, then some of X1 , . . . , Xk also does. Proof. We use a monotonicity property: if n′ |n then every n-witness is automatically also n′ -witness. Consider a sequence of (n!)-witnesses (n! stands for n factorial), for n > 0, contained in X. One of the sets X1 , . . . , Xk necessarily contains inﬁnitely many of them. By monotonicity, this set contains (n!)-witnesses for all n > 0, and hence n-witnesses for all n > 0. ⊓ ⊔ 15

Relying on Lemma 19 and Proposition 17, our procedure guesses one of the linear sets (11). It thus remains to describe a PSpace algorithm for the following core problem: for a given PSpace-enumerable linear set L = b + P ∗ ⊆ N2 × Z, determine whether it contains n-witnesses for all n > 0. Decision procedure for the core problem. In case of a linear set L, the condition we are to check boils down to two separate sub-conditions: Lemma 20. L = b + P ∗ contains n-witnesses for all n > 0 if, and only if (a) for every n, there is (n1 , n2 , n3 ) ∈ L with n1 , n2 ≥ n; (b) for every n, there is (n1 , n2 , n3 ) ∈ L with n|n3 . Proof. Put b = (b1 , b2 , b3 ). Indeed, if (b1 , b2 , b3 ) + (k1 , k2 , k3 ) ∈ L for b1 + k1 , b2 + k2 ≥ n, and (b1 , b2 , b3 ) + (m1 , m2 , m3 ) ∈ L for n|(b3 + m3 ), then (b1 , b2 , b3 ) + n(k1 , k2 , k3 ) + (m1 , m2 , m3 ) ∈ L is an n-witness. Hence conditions (a) and (b) imply that L contains n-witnesses for all n > 0. The opposite direction is obvious. ⊓ ⊔ Condition (a) in Lemma 20 is easy for algorithmic veriﬁcation: enumerate vectors in P while checking whether some vector is positive on ﬁrst coordinate, and some (possibly diﬀerent) vector is positive on second coordinate. As the last bit of our decision procedure, it remains to check condition (2) in Lemma 20. Writing b3 , resp. P3 , for the projection of b, resp. P , on the third coordinate, we need to check whether the set b3 + P3 ∗ ⊆ Z contains (possibly negative) multiplicities of all n > 0. We build on the following fact: Proposition 21. The set b3 + P3 ∗ contains multiplicities of all n > 0 if, and only if b3 is a linear combination of P3 , i.e., b 3 = a1 p 1 + . . . + ak p k , for a1 , . . . , ak ∈ Z and p1 , . . . , pk ∈ P3 . Proof. For the ’only if’ direction, suppose that b3 + P3 ∗ contains multiplicities of all positive numbers. Note that in particular P3 is forcedly nonempty. Fix arbitrary n such that n ∈ P3 . Suppose n > 0 (if n < 0 take −n instead of n). By the assumption, b3 + p ≡ 0 mod n for some p ∈ P3 ∗ , i.e., b3 ≡ −p mod n. Then for some a ∈ Z, b3 = −p + an, hence b3 is a linear combination of P3 , as required. For the ’if’ direction, suppose b3 is a linear combination of P3 , say b 3 = a1 p 1 + . . . + ak p k , 16

for a1 , . . . , ak ∈ Z and p1 , . . . , pk ∈ P3 . Let n > 0. It is possible to decrease the numbers a1 , . . . , ak by multiplicities of n so that they become non-positive. Thus we have −b3 ≡ −a1 p1 − . . . − ak pk mod n, for a1 , . . . , ak ∈ N, i.e., b3 ≡ −p mod n for some p ∈ P3 ∗ . In consequence b3 +p ≡ 0 mod n, as required. ⊓ ⊔ Thus we only need to check whether b3 is a linear combination of P3 . By Chinese remainder theorem, this is equivalent to b3 being a multiplicity of the greatest common divisor of all numbers in P3 . Thus our decision procedure enumerates the set P , computes the greatest common divisor g of projections p3 on the third coordinate of all vectors p ∈ P , and ﬁnally checks whether g|b3 . The upper bound of Theorem 1 is thus proved. 4.1

Proof of Proposition 15

We concentrate on showing that the sets prefpq are PSpace-enumerable. (The sets suffpq can be dealt with in exactly the same way as prefpq , but with V replaced by the reverse of V.) In the sequel ﬁx states q, p of A and B, respectively. The set prefpq is nothing but the reachability set of a 2-VASS V(N, N) in control state (q, p), from the initial conﬁguration ((q0 , p0 ), 0, 0). We build on a result of [4] which describes the reachability set in terms of sets reachable via a ﬁnite set of linear path schemes, a notion that we are going to recall now. Let T be transitions of V. A linear path scheme is a regular expression over T of the form: E = α0 β1∗ α1 . . . βk∗ αk ,

(12)

where αi , βi ∈ T ∗ . The sequences β1 , . . . , βk are called loops of E. By length of E we mean the sum of lengths of all αi and βi . Let ReachE (the reachability set via E) contain all pairs (n, m) ∈ N2 such that ((q0 , p0 ), 0, 0) −→ ((q, p), n, m) in V(N, N) via a sequence of transitions that belongs to E. Here is Thm. 1 in [4], translated to our terminology: Lemma 22 ([4]). There are computable bounds N1 , N2 , where N1 is exponential and N2 is polynomial in the size of V, such that prefpq is a union of sets ReachE , for linear path schemes E of length at most N1 , with at most N2 loops. In order to test whether a conﬁguration is reachable in V(N, N) by a given linear path scheme E, it is not needed to know the whole scheme. For our purposes it is enough to describe E as in (12) using 4k + 1 pairs of integers. Let ai ∈ Z2 , for i = 0, . . . , k, be the total eﬀect of executing the sequence αi , and likewise bi for the sequence βi , for i = 1, . . . , k. Moreover, let ci ∈ N2 , for i = 1, . . . , k be the (point-wise) minimal values of counters that allow to execute the sequence αi (in V(N, N)), and likewise di for the sequence βi , for i = 1, . . . , k. The 4k + 1 pairs of numbers, namely ai (for i = 0 . . . k) and bi , ci , di (for i = 1 . . . k), we jointly call a profile of the linear path scheme E. 17

Lemma 23. Given pairs ai ∈ Z2 (for i = 0 . . . k) and bi ∈ Z2 and ci , di ∈ N2 (for i = 1 . . . k), it can be checked in PSpace if they form a profile of some linear path scheme. Proof. Guess intermediate control states (q1 , p1 ), . . . , (qk , pk ). Put c0 = (0, 0) and (qk+1 , pk+1 ) = (q, p). Check that the following reachability properties hold in V(N, N), for i = 0, . . . , k and i = 1, . . . , k, respecively: (qi , pi ), ci −→ qi+1 , pi+1 ), ci + ai (qi , pi ), di −→ qi , pi ), di + bi and that the above properties fail to hold if any ci (resp. di ) is replaced by a point-wise smaller pair of numbers. All the required checks are instances of the reachability problem for 2-VASS, hence doable in PSpace [4]. ⊓ ⊔ Denote by Reachp the set of conﬁgurations reachable in V(N, N) via some linear path scheme with proﬁle p. Using Lemma 23 we can enumerate all proﬁles of linear path schemes (12) of length at most N1 with k ≤ N2 loops. Note that each such proﬁle can be represented (in binary) in polynomial space. Thus by the virtue of Lemma 22 it is enough to show, for a ﬁxed proﬁle p, that the set Reachp is PSpace-enumerable. Fix a proﬁle p from now on. As a convenient tool we will use linear Diophantine equations. There are systems of equations of the form a1 x1 + . . . + al xl = a,

(13)

where x1 , . . . , xl are variables, and a, a1 , . . . , al are integer coeﬃcients. For a system U of such equations, we denote by sol(U) ⊆ Nl the solution set of U, i.e., the set all of non-negative integer vectors (n1 , . . . , nl ) such that the valuation x1 7→ n1 , . . . , xl 7→ nl satisﬁes all the equations in U. We say that a vector is bounded by m if it is smaller than m on every coordinate. By size(U) we denote the size of U, with integers encoded in binary. By Prop. 2 in [6] we get: Lemma 24. sol(U) = B + P ∗ , with every base b ∈ B and period p ∈ P bounded by 2N , for a computable bound N ∈ N polynomial in size(U). Observe that, forcedly, P ⊆ sol(U0 ) where U0 denotes a modiﬁcation of the system of linear equations U with all right-hand side constants a (cf. (13)) replaced by 0. We will use Lemma 24 once we state the last lemma we need: Lemma 25. The set Reachp is a projection of the union sol(U 1 ) ∪ . . . ∪ sol(U l ), for systems of linear Diophantine equations U 1 . . . U l that can be enumerated in polynomial space. 18

The two lemmas immediately imply that Reachp is PSpace-enumerable. Indeed, by Lemma 24 applied to every of the systems U i , we have sol(U i ) = Bi +Pi ∗ for bases Bi containing all vectors b ∈ sol(U i ) bounded by 2N , and periods Pi containing all vectors p ∈ sol(U i 0 ) bounded by 2N , where N is polynomial. Relying on Lemma 25, the algorithm enumerates all systems U i , then enumerates all b ∈ Bi satisfying the above constraints, and for each b it enumerates all periods p ∈ Pi satisfying the above constraints. The proof of Proposition 15 will be thus completed, once we prove the last lemma. Proof (of Lemma 25). Introduce variables xi , for i = 1 . . . k, to represent the number of times the loop βi has beed executed. The necessary and suﬃcient condition for executing the linear path scheme (12) can be described by a positive Boolean combination of linear inequalities (that can be further transformed into linear equations using auxiliary variables), which implies Lemma 25. Indeed, for every i = 1 . . . k, we distinguish two sub-cases, xi = 0 or xi > 0. In the former case (the loop βi is not executed) we put the two inequalities described succinctly as (note that all aj , bj , cj , dj are pairs in Z2 , resp. N2 ) a0 + b1 x1 + a1 + . . . + bi−1 xi−1 + ai−1 ≥ ci to say that αi can be executed. In the latter case (the loop βi is executed) we put the following four inequalities a0 + b1 x1 + a1 + . . . + bi−1 xi−1 + ai−1 ≥ di a0 + b1 x1 + a1 + . . . + bi−1 xi−1 + ai−1 + bi (xi − 1) ≥ di to say that the ﬁrst and the last iteration of the loop βi can be executed (which implies that each intermediate iteration of βi can be executed as well), plus the two inequalities a0 + b1 x1 + a1 + . . . + bi−1 xi−1 + ai−1 + bi xi ≥ ci to assure that αi can be executed next. Finally, the two variables (y1 , y2 ) representing the ﬁnal conﬁguration, are related to other variables by the two equations: a0 + b1 x1 + a1 + . . . + bk xk + ak = (y1 , y2 ). The set Reachp is the projection, onto (y1 , y2 ), of the union of solution sets of all the above-described systems of equations. ⊓ ⊔ 4.2

Proof of Proposition 16

In the sequel we ﬁx states q, q ′ of A and p, p′ of B, respectively. Our aim is to ′ prove that midpp qq′ is PSpace-enumerable. Recall Parikh image Pi(w) of a word w ∈ Σ ∗ , for a ﬁxed ordering a1 < . . . < ak of Σ, deﬁned as the vector (n1 , . . . , nk ) where ni is the number of occurrences 19

of ai in w, for i = 1, . . . , k. Parikh image lifts to languages: Pi(L) = {Pi(w) | w ∈ L}. An OCN we call 1-OCN if its every transition (q, a, q, z) satisﬁes z ∈ {−1, 0, 1}. We deﬁne a 1-OCN C of exponential size, over a 5-letter alphabet {a0 , b0 , a+ , a− , bf }, ′ such that midpp qq′ is the image of the linear function of Pi(L(C)). C starts with the zero counter value, and its execution splits into three phases. In the ﬁrst phase C reads arbitrarily many times a0 without modifying the counter, and arbitrary many times b0 , increasing the counter by 1 at every b0 . Thus the counter value of C at the beginning of the second phase is equal to the number of b0 s. In the last third phase, C reads arbitrarily many times bf , decreasing the counter by 1 at every bf . The accepting conﬁguration of C requires the counter to be 0. Thus the counter value of C at the end of the second phase is equal to the number of bf s. In the middle second phase C simulates execution of V(Z, N). The counter value of C corresponds, during this phase, to the counter value of B. On the other hand, the counter value of A will only be reﬂected by the the number of a+ and a− read by C. States of C correspond to pairs of states of A and B, respectively; there will be also exponentially many auxiliary states. The phase starts in state (q, p), and ends in state (q ′ , p′ ). A transition (q1 , p1 ), (z1 , z2 ), (q2 , p2 ) of V is simulated in C as follows: First, if z1 ≥ 0 then C reads z1 letters a+ ; otherwise, C reads −z1 letters a− . Second, if z2 ≥ 0 then C performs z2 consecutive increments of the counter; otherwise C performs −z2 decrements. In both tasks, fresh auxiliary states are used. We assume w.l.o.g. that every transition of V satisﬁes (z1 , z2 ) 6= (0, 0); hence C has no ε-transitions. This completes the description of the 1-OCN C. ′ 5 Let S = Pi(L(C)) ⊆ N5 . Then midpp qq′ = f (S), for a linear function f : Z → 4 Z deﬁned by (intensionally, we re-use alphabet letters in the role of variable names): (a0 , b0 , a+ , a− , bf ) 7→ (a0 , b0 , a0 + a+ − a− , bf ). Therefore if S is PSpace-enumerable then f (S) is also so; it thus remains to prove that S is PSpace-enumerable. Our proof builds on results of [2, 17]. In order to state it we need to introduce the concept of pump of an accepting run ρ of C (called direction in [2]). We treat accepting runs ρ as sequences of transitions. A pump of ρ of ﬁrst kind is a sequence α of transitions such that ρ factorizes into ρ = ρ1 ρ2 , and ρ1 αρ2 is again an accepting run. Note that in this case the eﬀect of α on the counter is necessarily 0. A pump of second kind is a pair α, β of sequences of transitions, where the eﬀect of α is non-negative, such that ρ factorizes into ρ = ρ1 ρ2 ρ3 , and ρ1 αρ2 βρ3 is again an accepting run. Note that in this case the eﬀect of β is necessarily opposite to the eﬀect of α. Parikh image of a sequence of transitions Pi(ρ) is understood as a shorthand for Parikh image of the input word of ρ. Furthermore, we use a shorthand notation for Parikh image of a pump π: let Pi(π) mean either Pi(α) or Pi(αβ), in case of the ﬁrst or second kind, respectively. Similarly, the length of π is either 20

the length of α, or the length of αβ. Lemma 26 follows by [2], Lem. 15, and [3], Lem. 58 (see also [17], Thm. 6): Lemma 26. There is a computable bound N , polynomial in the size of C, such that S is a union of linear sets of the form Pi(ρ) + {Pi(π1 ), . . . , Pi(πl )}∗

(l ≤ 5),

where ρ is an accepting run of C of length at most N , and π1 . . . πl are pumps of ρ of length at most N . Lemma 27 is used for verifying candidate linear sets delivered by Lemma 26. Lemma 27. For b ∈ N5 and P = {p1 , . . . , pl } ⊆ N5 , l ≤ 5, it is decidable in PSpace if there is an accepting run ρ of C of length at most N and pumps π1 , . . . , πl of ρ of length at most N , such that b = Pi(ρ) and pi = Pi(πi ) for i = 1, . . . , l. Proof. Algorithm will simulate in parallel, in polynomial space at most 6 diﬀerent runs of C. Concretely, it guesses, for each of pi , whether it corresponds to a pump of ﬁrst or second kind. We assume below that all pumps are of second kind, i.e., pairs αi , βi – pumps of ﬁrst kind are treated in a simpler but similar way. Note that N is exponential in the size of A, B, thus counting up to N is possible in polynomial space. Start by simulating nondeterministically a run ρ of C of length at most N (call this simulation main thread ; in addition, there will be also at most 5 pump threads). The algorithm thus maintains the current conﬁguration c of C, and chooses nondeterministically consecutive transitions to execute. In addition, the algorithm updates Parikh image of the run executed so far (in polynomial space). In the course of simulation the algorithm guesses nondeterministically l points where a pump i intervenes into the simulated run, i = 1, . . . , l. At each so guessed point suspend all the threads, and add and run a new pump thread, responsible for simulating from the current conﬁguration c of C some sequence of transitions αi of length at most N . The simulation of αi ﬁnishes nondeterministically, say in conﬁguration ci , if the counter value of ci is greater or equal the counter value of c (the eﬀect of αi is non-negative) and the state of ci is the same as the state of c. Then Parikh image ai = Pi(αi ) is stored (in polynomial space), and the simulation of all threads (the suspended ones and the new one) are continued, with the proviso that all threads use the same nondeterministically chosen sequence of transitions. Thus the algorithm maintains up to 6 conﬁgurations c, c1 , . . . , cl of C, and stores up to 5 vectors a1 . . . al . Later in the course of simulation the algorithm also guesses nondeterministically l points where a pump i intervenes into the simulated run for the second time, i = 1 . . . l. Similarly as above, at each so guessed point suspend all other threads except for the one corresponding to pump i, and simulate in that thread some sequence βi of length at most N . This simulation terminates only if its current conﬁguration becomes equal to the current conﬁguration of the main 21

thread, i.e., ci = c, and moreover Parikh image of βi , say bi , satisﬁes ai + bi = pi ; and once this happens, the pump thread is cancelled. Note that one pump thread might be cancelled before some another pump thread starts, this however does not introduce any problem, as the total number of all pump threads is at most 5. The whole simulation ﬁnishes when all pump threads are cancelled, the current conﬁguration c is the ﬁnal conﬁguration of C, and Parikh image of the run executed in the main thread equals b. ⊓ ⊔ The two lemmas imply that S is PSpace-enumerable. Indeed, it is enough to enumerate all candidates b, P bounded by N , as speciﬁed in Lemma 26, and validate them, using Lemma 27. This completes the proof of Proposition 16.

5

PSPACE-hardness

Recall that a language is definite if it is a ﬁnite Boolean combination of languages of the form wΣ ∗ , for w ∈ Σ ∗ . In this section we prove the following result which, in particular, implies the lower bound of Theorem 1: Theorem 28. For every class F containing all definite languages, the F separability problem for languages of OCN is PSpace-hard. A convenient PSpace-hard problem, to be reduced to F separability of OCN, can be extracted from [12]. Given an OCA A and b ∈ N, the bounded nonemptiness problem asks whether A accepts some word by a b-bounded run; a run is b-bounded if counter values along the run are at most b. Theorem 29 ([12]). The bounded non-emptiness problem is PSpace-complete, for A and b represented in binary. A detailed analysis of the proof reveals that the problem remains PSpacehard even if the input OCA A = (Q, α0 , αf , T, T=0 ) is assumed to be acyclic, in the sense that there is no conﬁguration α reachable by a b-bounded run α0 −→ α with a non-empty b-bounded run α −→ α. Observe that an acyclic OCA has no b-bounded run longer than b|Q|, a property which will be crucial for the correctness of our reduction. Proposition 30. The bounded non-emptiness problem is PSpace-complete, for acyclic A and b represented in binary. We are now ready to prove Theorem 28, by reduction from bounded nonemptiness of acyclic OCA. Given an acyclic OCA A = (Q, (q0 , 0), (qf , 0), T, T=0 ) and b ∈ N, we construct in polynomial time two OCN B and B ′ , with the following properties: (a) if A has a b-bounded accepting run then L(B) ∩ L(B ′ ) 6= ∅ (and thus L(B) and L(B ′ ) are not F separable); (b) if A has no b-bounded accepting run then L(B) and L(B ′ ) are F separable. 22

The two OCN B and B ′ will jointly simulate a b-bounded run of A, obeying an invariant that the counter value v of B is the same as the counter value of A, while the counter value of B ′ is b − v. The actual input alphabet of A is irrelevant; as the input alphabet of B and B ′ we take Σ = T ∪ T=0 . The OCN B behaves essentially as A, except that it always allows for a zero test. Formally, B = (Q, (q0 , 0), (qf , 0), U ), where the transitions U are deﬁned as follows. For every transition t = (q, a, q ′ , z) ∈ T , there is a corresponding transition (q, t, q ′ , z) ∈ U. Moreover, for every zero test t = (q, a, q ′ ) ∈ T=0 , there is a transition (q, t, q ′ , 0) ∈ U. On the other hand, the OCN B ′ starts in the conﬁguration (q0 , b), ends in (qf , b), and simulates the transitions of A but with the opposite eﬀect. Formally, B ′ = (Q ∪ X, (q0 , b), (qf , b), U ′ ), for X a set of auxiliary states. For every transition t = (q, a, q ′ , z) ∈ T , there is a corresponding transition (q, t, q ′ , −z) ∈ U with eﬀect −z is the opposite of the eﬀect of t. Moreover, for every zero test t = (q, a, q ′ ) ∈ T=0 , we include into U ′ the following three transitions (q, ε, p, −b) (p, ε, p′ , +b) (p′ , t, q ′ , 0), for some auxiliary states p, p′ . The aim of the ﬁrst two transitions is to allow the last one only if the counter value is exactly b. We need to argue that the implications (a) and (b) hold. The ﬁrst one is immediate: every b-bounded accepting run of A is faithfully simulated by B and B ′ , and thus the languages L(B) and L(B ′ ) have non-empty intersection. For the implication (b), suppose A has no b-bounded accepting run. The ﬁrst step is to notice that the languages L(B) and L(B ′ ) are necessarily disjoint. Indeed, any word w ∈ L(B) ∩ L(B ′ ) would describe a b-bounded accepting run of A: B ensures that the counter remains non-negative, while B ′ ensures that the counter does not increase beyond b and that the zero tests are performed correctly. Let L contain all preﬁxes of words from L(B), and likewise L′ for L(B ′ ). Let n = b|Q|. Recall that due to acyclicity, A has no b-bounded run of length n (in the sense of the number of transitions) or longer. Thus, for the same reason as above, the intersection L ∩ L′ contains no word of length n or longer. In simple words, we are going to show that for a word of length n or longer, it is enough to inspect its preﬁx of length n in order to classify the word between L(B) and L(B ′ ). We deﬁne a language K ∈ F as follows: [ wΣ ∗ , K := L(B) ∩ Σ