One-counter circuits? Vladimir A. Bashkin Yaroslavl State University Yaroslavl, 150000, Russia email: bas@uniyar.ac.ru Abstract. One-counter nets are nondeterministic one-counter automata without zero-testing (Petri Nets with at most one unbounded place). A one-counter circuit of length ∆ is a strongly connected one-counter net, such that ∆ is a greatest common divisor of effects of all its cycles. A circuit has simple periodic behaviour: for any control state the set of corresponding reachable counter values is an arithmetic progression with difference ∆ (with an exception of a bounded subset). Properties of circuits and general one-counter nets are studied. It is shown that the infinite behaviour of a one-counter net can be represented by a composition of a finite set of circuits. 1 Introduction One-counter nets are Petri nets with one unbounded place, or, equivalently, pushdown automata with a single-symbol stack alphabet. The restriction on the number of counters makes them less expressive than ordinary Petri nets [12], but more analyzable and hence more suitable for specific modeling and verification tasks. Reachability, similarity and bisimilarity for one-counter automata and one-counter nets have been considered, among others, in [1, 8, 9]. The maximal number of unbounded counters generates a lot of substantial hierarchies in Petri net theory and allows to find some interesting borders of com- plexity and decidability. For example, one-counter nets is the largest class with decidable bisimularity [7], two-counter nets is the largest class with semilinear reachability [6] and flatness [10]. In a more expressive formalism of determinis- tic automata one-counter systems is the largest class with decidable language equivalence [14]. In the field of finite automata M.Chrobak proved that any nfa over a unary alphabet can be represented in a certain normal form [4]. Note that the constructive parts of all mentioned results were obtained by finding some specific periodicity of the infinite state space. In [2] we studied the periodicity of a single counter, using a particular number-theoretic method, based on Frobenius numbers (Sylvester solution of Frobenius coin problem [13]). It was shown that a semilinear set of naturals can be represented by a disjoint union of a finite set and a finite family of semilin- ear sets with the same single period. Using this number-theoretic property we ? This research is partially supported by Russian Fund for Basic Research (11-01- 00737, 11-07-00549, 12-01-00281) and Higher School of Economics. proved that a set of reachable counter values of a one-counter net, greater than some value x, may be completely described by arithmetic progressions. In this article we study the cyclic structure of one-counter nets and give an effective estimation of x. In particular it is shown, that a key structural property, defining the “depth” of a non-trivial behaviour of a counter is a greatest common divisor of effects of all cycles of strongly connected component of a net. The paper is organized as follows. In section 2 we recall basic definitions and notations on linear sets, Frobenius numbers and one-counter nets. In section 3 strongly connected one-counter nets (one-counter circuits) are studied. In section 4 we consider general one-counter nets. Section 5 contains some conclusions. 2 Preliminaries 2.1 Linear sets of naturals Let Z, Z− , Z+ denote integers, negative integers and positive integers respec- tively. Let also Nat denote a set of nonnegative integers. A set m ⊆ Nat is called linear if it can be represented as m = Lin{v, {w1 , . . . , wl }} =def {v + n1 w1 + . . . + nl wl | n1 , . . . , nl ∈ Nat}, where v, w1 , . . . , wl ∈ Nat are fixed. A set m ⊆ Nat is called a finitely erased linear set if m = m0 \ m00 , where m0 is a linear set and m00 is a finite set. If m0 = Lin{v, {w1 , . . . , wl }} and w ∈ Nat is a largest element of m00 , then we denote m by DLin{v, w + 1, {w1 , . . . , wl }}. Note that DLin{v, w, E} is not a description of a set: it does not tell us what values are erased. We know only the borderline w between a “corrupt” head and an infinite linear tail. A set Lin{v, {w}} is an arithmetic progression (a series) with a difference w. 2.2 Facts from number theory In this paper we use the following number-theoretic fact (a solution of the Frobe- nius coin problem by Sylvester) [13]: Fact 1. If gcd(a, b) = 1, then the greatest number c such that the equation ax + by = c has no solution in natural numbers is (a − 1)(b − 1) − 1. A simple consequence: Lemma 1. [2] If m = Lin{v, {w1 , w2 }} then, denoting p = gcd(w1 , w2 ), we have m = DLin{v, v + p( wp1 − 1)( wp2 − 1), {p}}. The generalization of Frobenius problem to an arbitrary number of variables still does not have the exact solution. As far as we know, the best known ap- proximation is [3, 11, 5]: Fact 2. Let a1 , . . . , ak be natural numbers ≤ n. Let X be the set of all x’s for which the Diophantine equation a1 x1 +· · ·+ak xk = x is solvable in natural num- bers. Then the set of numbers in X greater than n2 is an arithmetic progression with difference gcd(a1 , . . . , ak ). 2.3 One-counter nets An (unlabelled) one-counter net is a pair N = (Q, T ), where Q is a finite set of control states, T ⊂ Q × Q × Z is a finite set of transitions.        Fig. 1. A one-counter net. A state of the net is described by a pair q|c, where q ∈ Q is a control state, c ∈ Nat – a counter value. A transition t = (q, q 0 , z) is enabled in state q|c if c+z ≥ 0. Enabled transition t may fire, changing the state to q 0 |c + z (denoted by q|c → q 0 |c + z). The value z is also called an effect of t (denoted Eff(t)). A support is defined as:  0, z ≥ 0; Supp(t) =def |z|, z < 0. A marked one-counter net is a pair (N, s0 ), where N = (Q, T ) is a one-counter net and s0 ∈ (Q×Nat) – its initial state. For a marked one-counter net (N, s0 ) its reachability set R(N, s0 ) is defined as follows: ∗ R(N, s0 ) =def {s ∈ (Q×Nat) | s0 → s}. A marked net (N, s0 ) is unbounded iff the set R(N, s0 ) is infinite. For a particular control state q ∈ Q its counter reachability set R(N, s0 )[q] is defined as follows: ∗ R(N, s0 )[q] =def {c ∈ Nat | s0 → q|c}. A control state q ∈ Q is reachable iff R(N, s0 )[q] 6= ∅. A one-counter net is a digraph with arcs labeled by integers. Recall some basic notion from graph theory. A walk is an alternating sequence of vertices and arcs, beginning and ending with a vertex, where each vertex is incident to both the arc that precedes it and the arc that follows it in the sequence, and where the vertices that precede and follow an arc are the head and the tail of that arc. We consider only non-empty walks, containing at least one arc. A walk is closed if its first and last vertices are the same. A path is a walk where no arcs are repeated (vertices may be repeated). A simple path is a path where no vertices are repeated. A cycle is a closed path. A simple cycle is a closed path where no vertices are repeated. An effect and a support of the walk are defined inductively. Let t be a tran- sition, σ – a walk, such that the tail t is a head of the first transition of σ. Denoting by tσ a walk, constructed by linking t and σ, we have: Eff(tσ) =def Eff(t) + Eff(σ); Supp(tσ) =def Supp(t) + (Supp(σ) Eff(t)). Here denote a truncated subtraction. A positive (resp., negative) walk is a walk with a positive (resp., negative) effect. Obviously, effect of a cycle does not depend on a choice of starting node. A node q is called a generator, iff there exists a positive path from q to q (constituting a positive cycle) with a zero support. Lemma 2. Any positive cycle contains at least one generator. Proof. Straightforward, by induction on the length of a cycle. 3 Strongly connected one-counter nets Definition 1. A one-counter net is called strongly connected (SCN) iff it has a strongly connected control graph. Definition 2. Let N = (Q, T ) be an SCN. We will call N : – a positive circuit iff it has at least one positive cycle; – a negative circuit iff it has no positive cycles and at least one negative cycle; – a neutral circuit otherwise (iff all cycles have zero effect). Definition 3. Let q be a control state. Denote basic support values for q: – RSupp(q) — the smallest value of counter, such that in (N, q|RSupp(q)) every control state is reachable; – USupp(q) — the smallest value of counter, such that (N, q|USupp(q)) is un- bounded. Proposition 1. 1) If N is a positive circuit, then USupp(q) is the smallest support of paths from q to generators; otherwise USupp(q) is undefined. 2) If N is a positive circuit, then RSupp(q) = USupp(q). Proof. 1) The case of negative or neutral circuit is obvious. In the case of a positive circuit it is easy to see that unboundedness of the net implies unboundedness of all control states (since the net is strongly connected). On the other hand, unboundedness of a generator implies unboundedness of a net (again, since the net is strongly connected). Generator is bounded iff it is not reachable, so the reachability of at least one generator is equivalent to the unboundedness of the net. 2) Obviously, RSupp(q) ≤ USupp(q). Assume the converse: RSupp(q) < USupp(q). Due to the definition of the positive circuit, there exists at least one positive cycle θ. It contains at least one generator q 0 . The path σ from q to q 0 requires at most RSupp(q) support, so by previous property we can take RSupp(q) as USupp(q) — a contradiction. Note that: – both supports can be effectively computed (e.g. by variants of Tarjan algo- rithm). – in particular 1) means that an SCN is structurally bounded iff it is not a positive circuit. Definition 4. We will call a greatest common divisor of effects of all cycles a period of the circuit and denote it by ∆(N ). Note that a period is defined only for positive and negative circuits. Some trivial properties of ∆-circuits (circuits, having period ∆): Proposition 2. In a ∆-circuit: 1. effect of any closed walk is divisible by ∆; 2. for any pair (q, q 0 ) of control states there exists a non-negative integer Off(q, q 0 ) (we will call it an offset) with Off(q, q 0 ) < ∆, such that for any simple path σ from q to q 0 we have Eff(σ) = Off(q, q 0 ) + k∆ for some k ∈ Z; 3. for any walk σ from q to q 0 we have Eff(σ) = Off(q, q 0 ) + k∆ for some k ∈ Z. Proof. 1) Obviously, since any closed walk is a combination of simple cycles (a simple cycle with a finite number of cycles, attached to the vertices of this cycle). 2) Let σ1 and σ2 be two different simple paths from q to q 0 . Let also Eff(σ1 ) = δ1 + k1 ∆ and Eff(σ2 ) = δ2 + k2 ∆, where δ1 , δ2 ∈ Nat, δ1 < ∆, δ2 < ∆ and k1 , k2 ∈ Z. It is sufficient to prove that δ1 = δ2 (and hence is equal to Off(q1 , q2 )). The net is strongly connected, so there exists a simple path σ 0 from q 0 to q. Let Eff(σ 0 ) = e + m∆ with e ∈ Nat, e < ∆ and m ∈ Z. The walks σ1 σ 0 and σ2 σ 0 are closed, hence Eff(σ1 σ 0 ) = n1 ∆ and Eff(σ2 σ 0 ) = n2 ∆ for some n1 , n2 ∈ Z. Therefore, we have δ1 + k1 ∆ + e + m∆ = n1 ∆; δ2 + k2 ∆ + e + m∆ = n2 ∆. It can be rewrited: δ1 + e = (n1 − k1 − m)∆; δ2 + e = (n2 − k2 − m)∆. Natural numbers δ1 , δ2 and e are smaller than ∆. Hence, δ1 = δ2 . 3) Since any walk from q to q 0 is a simple path from q to q 0 with a finite number of cycles, attached to the vertices of this path. This proposition in particular shows that positive and negative circuits has a convenient graphical representation (Fig. 2). A net can be drawn as a ring with ∆ sectors. The n-th sector corresponds to the offset n, starting clockwise from the top sector (0-th). If we place a control state q into sector 0, then all other control states will be placed into sectors accordingly to their offsets (for example, if Off(q, q 0 ) = n, then q 0 is in the n-th sector). Positive transitions will be oriented clockwise, negative — counter-clockwise. Effect of a transition will be naturally represented by its length (number of traversed sectors).    Fig. 2. A circuit. 3.1 Positive circuits Let C+ and C− denote a finite sets of all positive and, respectively, negative cycles of a positive circuit. Consider a set of closed walks C∗ , constructed from elements of C− by adding a minimal required number of compatible (linkable) positive cycles to obtain a closed positive walk: C∗ =def {σ k θ | θ ∈ C− , σ ∈ C+ , k ∈ Nat s.t. Eff(σ k θ) > 0 ∧ Eff(σ k−1 θ) ≤ 0}. Since a net is strongly connected, such compatible positive cycle σ always exists. Also note that the largest effect of all closed walks from C∗ is not greater than the largest effect of all positive cycles (otherwise Eff(σ k−1 θ) would be positive). Denote C =def C+ ∪ C∗ . It contains all positive cycles and some positive closed walks. Note that since every positive cycle contains a generator, every element of C by construction also contains a generator. Denote the set of effects of C by E. Lemma 3. gcd{E} = ∆. Proof. Denote g = gcd{E}. Assume the converse: g <> ∆. Consider the case g < ∆. It is impossible, since from Prop. 2(1) effect of any closed walk is divisible by ∆. Consider the case g > ∆. The set C contains all positive cycles, hence there exists a negative cycle θ, which effect is not divisible by g. On the other hand, C contains a positive closed walk φ = σ k θ, where σ is a positive cycle, k ∈ Nat. Eff(φ) = Eff(σ k θ) = kEff(σ) + Eff(θ). Since σ is a positive cycle, it belongs to C and it’s effect is divisible by g, and hence Eff(φ) = kmg + Eff(θ) for some m ∈ Nat. The closed walk φ also belongs to C, so Eff(φ) = ng for some n ∈ Nat. We obtained kmg + Eff(θ) = ng, so Eff(θ) is divisible by g — a contradiction. Let q be a control state, U (q) – a set of all closed paths from q to q (cycles), containing generators, F (q) – the set of effects of these paths. Denote W (q) =def lcm{F (q)} – the minimal value of effect, that can be achieved by visiting any of the generators from the state q. In other words, W (q) is the minimal number that we can produce by iterating any of the cycles from U (q). Obviously, W (q) is divisible by ∆. Theorem 1. Let N = (Q, T ) be a positive ∆-circuit, e ∈ Nat – a largest effect of all cycles in N, q ∈ Q – a control state. Then R(N, q|u)[q] = DLin{USupp(q), USupp(q) + W (q) + e2 , {∆}}. Proof. In other words, the theorem states that, denoting u = USupp(q) and w = W (q), the set R(N, q|u)[q] is a disjoint union of two sets: a finite set R0 with elements not exceeding u + w + e2 , and an arithmetic progression R∞ with base u + w + e2 and difference ∆ : G R(N, q|u)[q] = R0 R∞ , where R0 ⊆ x ∈ Lin u, {∆} | x < u + w + e2 , R∞ = Lin u + w + e2 , {∆} .    1) Consider reachable values of the counter, smaller than u + w + e2 . It is sufficient to prove that distance from u to any such reachable value is divisible by ∆. This follows from Prop. 2(3) and an obvious fact that Off(q, q) = 0. So, the structure of R0 is proven. 2) Consider reachable values of the counter, greater or equal than u + w + e2 . Recall that u = USupp(q). Hence, from Prop. 1(2), u = RSupp(q) and hence all generators are reachable. Construct C and E as it was done in Lemma 3. Also recall that max{E} = e by construction of C. The set of effects of all possible closed walks from q contains (is underap- proximated by) a linear set X = Lin{w, E}. Note that we use the value w to guarantee that linear combinations of effects from E will be added to the same base – all corresponding generators are “visited” from q by walks (iterated cycles) with the same effect w. From Fact 2 it follows that the set of numbers in X greater than w + e2 is an arithmetic progression with period gcd{E}. From Lemma 3 we have gcd{E} = ∆. Additionally, from Prop. 2(3) and an obvious fact that Off(q, q) = 0 we have that no closed walks with effects greater than e2 and not in X are possible from q. Indeed, ∆ is the minimal distance between reachable counter values for q (and for any other control state). Therefore, the structure of R∞ is proven. Remark 1. We believe that our estimation of the “lower border of regularity” (u + w + e2 ) can be refined to a smaller value. For example, it may be promising to decrease w using “resources” from u. Of course, it would produce even more heavyweight formulae. 3.2 Negative circuits Theorem 2. Let N = (Q, T ) be a negative ∆-circuit, e ∈ Z− – a smallest effect of all cycles in N, f ∈ Z− – a smallest effect of all transitions in N, q ∈ Q – a control state. Denote R(N, q) =def {c ∈ Nat | 0 ∈ R(N, q|c)[q]}. Then R(N, q) = DLin{0, |f | + |e|2 , {∆}}. Proof. Note that the resource |f | is enough to support any cycle of the net. The set R(N, q) completely describes all possible counter subtractions that can be executed by a negative circuit. 3.3 Combining circuits Definition 5. Let X ⊆ Nat, Y ⊆ Nat. By X + Y and X Y we denote sets, obtained by, resp., adding and subtructing elements of Y to/from elements of X (shifts Y are applied to numbers X): X + Y =def {x + y ∈ Nat | x ∈ X, y ∈ Y }. X Y =def {x y ∈ Nat | x ∈ X, y ∈ Y }. Proposition 3. If X = DLin{a, b, {c}} and Y = {d} with a, b, c, d ∈ Nat, then: X + Y = DLin{a + d, b + d, {c}}; X Y = DLin{a d, b d, {c}}. Proof. Straightforward. Proposition 4. If X = DLin{a, b, {c}} and Y = DLin{d, e, {f }} with a, b, c, d, e, f ∈ Nat then, denoting g = gcd(c, f ), we have  X + Y = DLin a + d, b + e + g(c/g − 1)(f /g − 1), {g} . Proof. It is easy to see that “erased” part of X + Y indeed has such a structure (since if summands are divisible by g, then the sum is also divisible by g). Consider an infinite part. Note, that all elements of X + Y, greater than b + e, can be produced only by adding linear combinations of c and f. From Lemma 1 it follows that the set of all linear combinations, greater than g(c/g −1)(f /g −1), is an arithmetic progression with difference g. Proposition 5. If X = DLin{a, b, {c}} and Y = DLin{d, e, {f }} with a, b, c, d, e, f ∈ Nat then, denoting g = gcd(c, f ), we have  X Y = DLin a d, b e + g(c/g − 1)(f /g − 1), {g} . Proof. Straightforward. Propositions 4 and 5 show that if we give a finitely erased series to a circuit as an input, the output will also be a finitely erased series. Moreover, the growth of the borderline value, separating incomplete “head” and simple infinite “tail”, is quite slow. Also note that if in a positive circuit a negative closed walks are possible, their effects can only shift this borderline to a smaller values. 4 General one-counter nets Any one-counter net N contains a finite number of strongly connected com- ponents. It is known from graph theory, that if all nodes within each strong component are combined into a new “supernode”, then the condensed graph N̂ governing these supernodes is acyclic (Fig. 3).       Fig. 3. A condensed graph of strongly connected components. By copying supernodes this acyclic net N̂ can be transformed into a tree Ñ (Fig. 4). Now recall that every supernode of Ñ is actually an SCN (a circuit). Consider such a circuit. By construction of Ñ this circuit may be linked with other supern- odes (SCN’s) by at most one input state i and a finite number of output states       &'()+*-,    !"# $ % Fig. 4. A condensed tree of strongly connected components. {o1 , . . . , ok }. By copying all simple paths from i to o-s a net with a through- passage can be transformed into an equivalent net with a single “linkage” state i (Fig. 5). So, any one-counter net can be transformed into a tree with linked circuits (Fig. 6). Every control state of this net corresponds to a finite set or a finitely erased series of reachable counter values. The period and borderline values of such a series are structural properties of the corresponding circuit and do not depend on an initial state of the net. Roughly speaking, a reachability problem for one-counter nets is also a kind of a structural problem. An infinite part of a reachability set is predictable too easily. 5 Conclusion One-counter nets are a well-studied formalism with a lot of established proper- ties. The results of the article are quite simple. However (for our best knowledge), the presented number-theoretic approach to the one-counter state space is novel. A strongly connected one-counter net is called here a circuit. In our opinion, this term is sufficiently justified by circular graphical form of an SCN. We also think that this kind of symbolic representation may be useful in applications. References 1. P.A.Abdulla and K.Cerans. Simulation is decidable for one-counter nets (extended abstract). Proc. of CONCUR’98, LNCS 1466, 69–153, 1998. 2. V.A.Bashkin. On the single-periodic representation of reachability in one-counter nets. Proc. of CS&P’2009. 60–71. Warsaw, 2009.      Fig. 5. A circuit with a single interface state.       Fig. 6. A tree of hanging circuits. 3. A.Brauer. On a problem of partitions. Amer. J. Math.. 64, 299–312, 1942. 4. M.Chrobak. Finite automata and unary languages. Theor. Comput. Sci., 47, 149– 158, 1986. 5. P.Erdös and R.L.Graham. On a linear diophantine problem of Frobenius. Acta Arithm., 21, 399–408, 1972. 6. J.E.Hopcroft and J.-J.Pansiot. On the reachability problem for 5–dimensional vector addition systems. Theor. Comp. Sci., 8(2), 135–159, 1979. 7. P.Jančar. Decidability questions for bisimilarity of Petri nets and some related problems. Proc. of STACS’94. LNCS 775, 581–592, 1994. 8. P.Jančar, A.Kučera, F.Moller, Z.Sawa. DP Lower bounds for equivalence-checking and model-checking of one-counter automata. Inf. Comput., 188(1), 1–19, 2004. 9. A.Kučera. Efficient verification algorithms for one-counter processes. Proc. of ICALP’2000, LNCS 1853, 317–328, 2000. 10. J.Leroux and G.Sutre. On flatness for 2-dimensional vector addition systems with states. Proc. of CONCUR’2004, LNCS 3170, 402–416, 2004. 11. U.I.Liubicz. Bounds for the optimal determinization of nondeterministic autonomic automata. Sibirskii Matemat. Journal, 2, 337–355, 1964. (in Russian) 12. B.C.Reutenauer. The Mathematics of Petri Nets. Prentice Hall, 1990. 13. J.J.Sylvester. Question 7382. Mathematical Questions with their Solutions, Edu- cational Times Vol.41, 21, 1884. 14. L.Valiant and M.Paterson. Deterministic One-Counter Automata. J. of Computer and System Sciences, 10, 340–350, 1975.