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.
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 complexity 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 deterministic 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 semilinear sets with the same single period. Using this number-theoretic property we ? This research is partially supported by Russian Fund for Basic Research (11-0100737, 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 2.1
tively. Let also Nat denote a set of nonnegative integers.
m = Lin{v, {w1, . . . , wl}} =def {v + n1w1 + . . . + nlwl | 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}}.
values are erased. We know only the borderline w between a “corrupt” head and an infinite linear tail.
2.2
In this paper we use the following number-theoretic fact (a solution of the Frobenius 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 approximation 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 a1x1 + · · · + akxk = x is solvable in natural numbers. Then the set of numbers in X greater than n2 is an arithmetic progression with difference gcd(a1, . . . , ak). 2.3
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.
c ∈ Nat – a counter value.
A transition t = (q, q0, z) is enabled in state q|c if c+z ≥ 0. Enabled transition may fire, changing the state to q0|c + z (denoted by q|c →t q0|c + z). The value z is also called an effect of t (denoted Eff(t)). A support is defined as: Supp(t) =def 0, |z|, z ≥ 0; 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}.
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 transition, σ – 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
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 unbounded.
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.
USupp(q). Due to the definition of the positive circuit, there exists at least one positive cycle θ. It contains at least one generator q0. The path σ from q to q0 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 algorithm). – 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 Δ):
1. effect of any closed walk is divisible by Δ; 2. for any pair (q, q0) of control states there exists a non-negative integer Off(q, q0) (we will call it an offset) with Off(q, q0) < Δ, such that for any simple path σ from q to q0 we have Eff(σ) = Off(q, q0) + kΔ for some k ∈ Z; 3. for any walk σ from q to q0 we have Eff(σ) = Off(q, q0) + 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 q0. 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 q0 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.
δ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 q0 is a simple path from q to q0 with a finite number of cycles, attached to the vertices of this path.
Therefore, we have It can be rewrited: δ1 + k1Δ + e + mΔ = n1Δ;
δ2 + k2Δ + e + mΔ = n2Δ.
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, q0) = n, then q0 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).
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 the largest effect of all positive cycles (otherwise Eff(σk−1θ∗) wisonuoldt gbreeaptoesrittivhea)n.
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(
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 Δ :
R(N, q|u)[q] = R0 G 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(
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 underapproximated 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
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, {Δ}}.
be executed by a negative circuit. 3.3
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
Any one-counter net N contains a finite number of strongly connected components. 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. 4).
such a circuit. By construction of N˜ this circuit may be linked with other supernodes (SCN’s) by at most one input state i and a finite number of output states {o1, . . . , ok}. By copying all simple paths from i to o-s a net with a throughpassage 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
One-counter nets are a well-studied formalism with a lot of established properties. 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. 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¨os 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(
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, Educational 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.