=Paper=
{{Paper
|id=None
|storemode=property
|title=One-counter Circuits
|pdfUrl=https://ceur-ws.org/Vol-928/0025.pdf
|volume=Vol-928
|dblpUrl=https://dblp.org/rec/conf/csp/Bashkin12
}}
==One-counter Circuits==
https://ceur-ws.org/Vol-928/0025.pdf
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.