Decidability Analysis of Self-Stabilization for Infinite-State Systems
Hsu-Chun Yen
and Lien-Po Yu
Dept. of Electrical Engineering National Taiwan University Taipei, Taiwan 106, R.O.C. yen@cc.ee.ntu.edu.tw lpyu@seed.net.tw
Abstract. For a variety of infinite-state systems, the problem of deciding whether a given system is self-stabilizing or not is investigated from the decidability viewpoint. We develop a unified strategy
through which checking self-stabilization is shown to be decidable for lossy vector addition systems
with states, one-counter machines, and conflict-free Petri nets. For lossy counter machines and lossy channel systems, in contrast, the self-stabilization problem is shown to be undecidable.
Keywords: Decidability, infinite-state systems, self-stabilization, Petri nets.
1.
Introduction
The notion of self-stabilization was introduced by Dijkstra [7] to describe a system having the behav-ior that regardless of its starting configuration, the system would return to a ‘legitimate’ configuration eventually (by a legitimate configuration, we mean a configuration which is reachable from the initial configuration of the system). The motivation behind self-stabilization is that a self-stabilizing system has the ability to ‘correct’ itself even in the presence of certain unpredictable errors that force the system to reach an ‘illegitimate’ configuration during the course of its operations. In this sense, self-stabilizing systems exhibit tolerant behaviors to a certain degree. With the increased interest in designing fault-tolerant systems, the study of self-stabilization has been gaining increasing popularity in the computer science community lately. In what follows, we briefly review some of the previous work done in the area of self-stabilization.
Research supported in part by NSC 93-2213-E-002-003, and NSC 94-2213-E-002-087, Taiwan
Following the seminal work of Dijkstra [7], the majority of research along the line of self-stabilization has been focusing on providing solutions (and their proofs) for self-stabilizing systems with a variety of properties and topologies (see [10] for a bibliography of self-stabilization). In a somewhat different di-rection of research, Gouda, Howell and Rosier ([9]) have showed that the property of self-stabilization is ‘unstable’ across a wide variety of system classes, ranging from cellular automata, Turing machines, communicating finite state machines, to Petri nets. They basically demonstrated that the simulation
paradigm, which is a useful tool for designing and analyzing systems, may not be ‘robust’ with
re-spect to the property of self-stabilization. The simulation paradigm, simply speaking, is a methodology routinely used for designing or analyzing one class of systems with the help of another (hopefully, a well-studied one) through the simulation of the former by the latter. In this manner, properties of the former can be deduced from the respective properties of the latter. Unlike traditional properties such as liveness, boundedness and fairness which are almost always preserved under standard simulations, self-stabilization could easily be lost through the process of simulation from one class of systems to another (for more details, see [9]). To our knowledge, [9] also pioneers the introduction of the notion of self-stabilization to the model of Petri nets. In a subsequent paper [5], specific efforts have been devoted to reasoning about self-stabilization aspects of Petri nets from the computational complexity point of view. Among those complexity results derived in [5], detecting whether a Petri net is self-stabilizing is com-plete for polynomial time for bounded ordinary Petri nets, whereas it is PSPACE-comcom-plete for bounded general Petri nets.
As far as we know, very little is known regarding the complexity of the self-stabilization problem (i.e., the problem of deciding whether a system is self-stabilizing or not) for infinite-state systems. At this moment, the best bounds of the problem for general Petri nets are a lower bound of exponential space and an upper bound of
(the second level of the arithmetic hierarchy), whereas it is
-complete for Turing machines [5]. Therefore, it is of interest and importance to take a closer look at the problem for other infinite-state systems, in the hope of recognizing the key characteristics which govern the de-cidability/undecidability nature of the problem. An equally important goal is to, perhaps, come up with a unified framework through which decidability/undecidability of self-stabilization can be obtained. In this paper, we extend the work of [5] by investigating, from the decidability viewpoint, the problem of deciding whether a given system is self-stabilizing for a wide range of infinite-state systems, including
lossy vector addition systems with states, one-counter machines, conflict-free Petri nets, lossy counter machines, and lossy channel systems. As it turns out, the decidability of self-stabilization for lossy vec-tor addition systems with states, one-counter machines, and conflict-free Petri nets can be established in
a unified setting, taking advantage of the existence of a periodic witness for non-self-stabilizing infinite computations. For lossy counter machines and lossy channel systems, however, the self-stabilization problem turns out to be undecidable.
The rest of this paper is organized as follows. In Section 2, we give the definitions of transition systems and stabilization. Section 3 deals with the issue of deciding whether a given system is self-stabilized or not from the decidability viewpoint for a variety of infinite-state systems. A conclusion is given in Section 4.
2.
Preliminaries
A transition system (or system, for short) is a four-tuple , where consists of a (possibly
the transition function, and is the initial configuration. We write if . Also let (resp.,
) be the reflexive and transitive closure (resp., transitive closure) of . In words,
(resp., ) iff
can be reached from through zero (resp., one) or more transitions. A computation
is a (finite or infinite) sequence
. A configuration is said to be a dead
configuration if , i.e., has no immediate successor in .
Intuitively speaking, a system is said to be self-stabilizing (ss, for short) if, regardless of its starting configuration, the system would eventually return to a ‘legitimate’ configuration which is reachable from the initial configuration of the system. That is, a self-stabilizing system has the ability to ‘correct’ itself even in the presence of certain unpredictable errors that force the system to reach an ‘illegitimate’ configuration during the course of its operations. Let be a (finite or infinite) system with as its initial
configuration. Also let (= ! ) denote the set of reachable configurations from .
A computation
from configuration" is said to be non-self-stabilizing (non-ss) iff one of the following
holds: 1. is finite ( # $ %'&( )+*,
% , for some - ) such that % is a dead configuration
and%/. , or 2. is infinite ( # 0 ) such that1325467. .
See Figure 1. A system is said to be self-stabilizing if for each configuration , none of the computations
emanating from is non-ss. The self-stabilization problem is to determine, for a given (finite or infinite)
system, whether the system is self-stabilizing. In this paper, our main concern is to investigate the decidability issue of the self-stabilization problem for a variety of infinite-state systems for which the existence of a non-reachable dead configuration is decidable. The formal definitions of configurations and computations of each individual system will be clarified as our discussion progresses.
infinite non-ss computation
configuration dead the set of reachable configurations computation leading to a ‘legitimate’ configuration (1) (2) initial configuration
. . .
0R(S,c )
0 cLet ( ) denote the set of (nonnegative) integers, and
(
) the set of vectors of (nonnegative)
integers. In this paper, we consider only those systems for which can be encoded in such a way
that
, for some finite set and integer 2 4 ( is referred to as the set of states of
system ). For a vector
and a finite set (= , for some )
, the set = ( ! " $#+
&%' is called the linear set with base over the set of periods . A
semilinear set ()(7 ) (cf. [8]) is a finite union of linear sets. A semilinear set is effectively semilinear
if all the periods of those linear sets can be effectively computed. It is known that semilinear sets are exactly those that can be expressed in Presburger Arithmetic [15], which is a decidable theory. Given a set *+
, is upward (resp., downward) closed if , and ,.-+/ (resp., /0-1, ) implies / , where the ordering - in N
is the component-wise extension of the natural ordering in N. Given an upward-closed set 2 , an element 3 N
is said to be minimal if there is no4 .53 2 such
that 47683 . We write - 19 :2 to denote the set of minimal elements of 2 . We denote by <; the set *= > , where> is an object not in N (>@? N) such that the natural operations and ordering over N
is extended toA; as follows: > B> 8> C DA B> 8> ,>E%F DG%'>58> and6H> for all N. The operations and ordering of
; (i.e.
I*= >
) are thus extended likewise. An element
3 N
;
in a downward-closed set J is said to be maximal if there is no 4 .+3 J such that 4LKM3 . We write-A3 IJ to denote the set of maximal elements ofJ . From Dickson’s lemma, it is
well-known that for each upward-closed set 2 N N
,- 19 :2 is finite. Even so,- 19 :2 might not be
effectively computable in general. It is reasonably easy to see that both upward and downward closed sets are semilinear.
3.
Decidability Analysis
In this section, theOPO problem for various infinite-state models, including lossy vector addition systems
with states, one-counter machines, and conflict-free Petri nets, will be shown to be decidable. Before
going into the details, we begin by giving an overview of the general strategy using which the decidability results are obtained.
Recall from the definition of OPO that a system is not self-stabilizing iff either (i) a finite
compu-tation ends up with a dead configuration being not reachable from the initial configuration, or (ii) an infinite non-OPO computation exists. As we shall see later, (i) is relatively easy to check as long as certain
properties of are decidable. The idea behind our approach of checking (ii) is built upon showing that
to demonstrate the non-OPO nature of a system, it is sufficient to search among only non-OPO computations
of periodic behaviors, and hopefully, the confinement to such computations admits a decidable checking of (ii). By non-OPO periodic computations we mean those non-OPO computations of the formORQSQPT TT, i.e.,
repeatingU fromO infinitely many times witnesses non-OPO . In our subsequent investigation, we
character-ize the following two types of non-OPO periodic behaviors, through which a unified strategy is developed
serving as a foundation for our decidability results of theOPO problem.
V
(Strongly periodic:) Every finite computation Q
with
2 and . ensures non-OPO
of its infinite repetition (i.e., QSQPT TT is non-OPO ).
V
The disparity between strongly and weakly periodic non-OPO computations is that in the former, a
finite computation of the form ‘ Q
with
2 and . ’ is guaranteed to conclude the
system’s non-OPO behavior, whereas in the latter, however, not every finite computation of the above form
is extendible to renderOPO ; nevertheless, there does exist a periodic witness.
Before going into the details, we require the following notations. Let = be a transition
system, where A
, , and . V 2 5 O O ' O O
for some transition ,
V 5 O O ' O O ; 5 O O ' O O ; 35PO O , 35 , V
J J 35PO5 O is a dead configuration .
V
System is said to have the s-decidability property (or simply called s-decidable) if the following
holds:
(1) has an infinite non-OPO computation iff there exists an infinite computation O
O O %
, for some O and
, such that& 2 O CG%
. . (2) If O OF
andO . , then & 2 O %
OF 4 % , and & 2 OF E % . .
(3) It is decidable to determine the validity of the following formula :
9 O 9 O OF O . !
S-decidable systems correspond to systems whose non-ss behaviors can be captured by non-ss
computations of the strongly periodic type. What (1) says is that for s-decidable systems, infinite non-ss behaviors are witnessed by the existence of a periodic computation. Furthermore, (2) sug-gests the legitimacy of repeating a finite sequence infinitely many times to yield an infinite non-ss computation. As a result, any finite sequence satisfying the premise stated in (2) is sufficient to guarantee an infinite periodic non-ss computation. Finally, (3) simply says that finding a finite sequence meeting Condition (2) is decidable.
V
System is said to have the w-decidability property (or simply called w-decidable) if the following
holds:
(1) has an infinite non-OPO computation iff there exists an infinite computation O
O O %
, for some O and
, such that& 2 O CG%
.
.
(2) It is decidable to determine the validity of the following formula#" :
9 9 O & 2 OF E % O 4 % OF E % . &
W-decidable systems correspond to systems whose non-ss behaviors can be captured by non-ss
computations of the weakly periodic type. Like the case in s-decidability, (1) suggests that infinite non-ss behaviors are witnessed by the existence of a periodic computation. Condition (2) further ensures that checking the existence of a periodic non-ss computation stated in (1) is decidable. We are in a position to show the following unified strategy using which decidability of the ss problem will be established in our subsequent discussion for a number of infinite-state systems for which the existence of a non-reachable dead configuration is decidable.
Theorem 3.1. With respect to a computational model , if for every system = in , where 5 <
, the query ‘9 IJ J . ’ is decidable, and is
either s-decidable or w-decidable, then theOPO problem is decidable for .
Proof:
The query ‘9 IJ J . ’ being decidable ensures the existence of
an effective procedure to determine whether a non-reachable dead configuration exists or not. It remains to consider those systems for which non-ss is witnessed by the existence of infinite non-ss computations. First consider the case when is s-decidable. In this case, has infinite non-ss computations
iff Condition (1) of the definition of s-decidability holds, meaning that the non-ss is witnessed by a periodic computation. Furthermore, the formula in Condition (3) of the definition of s-decidability is
decidable. For such a system, our decision procedure involves checking whether the formula holds or
not. Assuming the formula holds, let ,O and
be such that O OF O .
According to Condition (2) of the definition of s-decidability, the above implies the validity of the infinite non-ss computation O
O O %
. Hence, is non-ss. On the other hand,
if has an infinite non-ss computation, then there is a finite computation O
O
satisfying
Condition (1) of the definition of s-decidability; hence, the O
above satisfy . In view of the above,
the formula holds iff has a non-ss computation.
Now consider a w-decidable system . Our decision procedure for theOPO problem involves checking
whether the formula " in Condition (2) of the definition of w-decidability holds or not. Suppose "
holds and let O
be the values that satisfy " . Then clearly O
O! O! %
witnesses an infinite non-ss computation. On the other hand, being non-ss, in conjunction with
Condition (1) of the definition of w-decidability, ensures the validity of formula " . This completes the
proof of the theorem.
We are in a position to show each of the models of lossy vector addition systems with states,
one-counter machines and conflict-free Petri nets to be either s-decidable or w-decidable; hence, the OPO
problem for these systems is decidable according to Theorem 3.1.
3.1. Lossy Vector Addition Systems with States
A -dimensional vector addition systems with states (VASSs) is a 5-tuple , where
is called the start vector,0 '
N. 7 is the transition relation, and is the initial state. Elements 3 of are
called transitions and are usually written as 3 . A configuration of a VASS is a pair , where and
. is the initial configuration. The transition 3 can be applied to
the configuration and yields the configuration E3 , written as E3 , provided
that C3 2 0. A lossy VASS is a VASS whose transition relation is modified as follows (see [3]):
if either (1) and
6 (i.e., losing value without involving any transition),
or (2) 2@ 2
(in words, before and/or after the execution of
, the vector may decrease in value).
Theorem 3.2. TheOPO problem for lossy VASSs is decidable.
Proof:
Consider a lossy VASS . From the fact that is downward closed
for each (see [3]), the query ‘9 IJ J . ’ is decidable,
since being lossy implies J J is either or 0 . (Note that if . , then 0 .) It suffices to consider the case when non-ss is witnessed by infinite non-ss
computations. In what follows, we show to be s-decidable.
Suppose has an infinite non-OPO computation ,
(for some transition
se-quences
). Then by Dickson’s Lemma [6] there must be indices 1 6 such that ' and '- . Let U , &( O H,
, and . Due to the monotonicity
property of (lossy) VASSs, CQ implies OQ O Q O W% Q Q O R%
Q . Also O . . Since is downward closed,
we have& 2 O BG%
. ’ (if O 1 %
, for some1 K , were in ,
then O – a contradiction). Hence, Conditions (1) and (2) of the definition of the
s-decidability hold.
Now we show Condition (3) of the definition of the s-decidability, i.e., the decidability of 9 O 9 O OF
O . . Consider the
set 2 PO O OW . Clearly, 2 is upward-closed. In [17], it
was shown that for each upward-closed set N N
, - 19 is effectively computable iff for every
N ; , the problem ‘ .5 ’ is decidable, where 7 - - N - - . Hence,
to show the effective decidability of - 19 :2 , it is sufficient to show, for each N
; , the question E20. to be decidable. The proof idea is sketched in Figure 2, in which a Petri net is
constructed in such a way that <2 /. iff some marking is reachable from the initial marking , in (for ease of explanation, the construction behind the proof is described in terms of a Petri net;
the equivalent VASS can easily be constructed). In this way, the answer to query E2 . is
equivalent to the reachability problem of PNs (VASSs), which is well-known to be decidable. Given a N ; , w.l.o.g., let 4 *+M D> and 54 . The operations of is divided into four phases, controlled by places
and , respectively. Places
are designed to simulate the contents of 4 , respectively, and
are their ‘backups’,
whose role will be explained later. Initially (i.e., at the initial marking, , a token is in+ and 4W- 1 - , , and 4 -A-H , ,
. As can be seen from Figure 2,
an arbitrary number of tokens can be deposited simultaneously to and
,
4 - 1F- , when a token is
in , allowing us to ‘simulate’ the > components of . The second phase begins when the token in
is moved to
, in which each of the places in
(this is to ‘simulate’ the
part in2 O ). When a token is moved from
to , the simulation
of VASS starts at a state, say in Figure 2, with contents of places
4 - 1 -D , remain intact. At
some point in time, the token in is transferred to to signal the end of the simulation as well as the
beginning of the final phase. Suppose, is the marking with respect to
at the end of the third
phase. In the final phase, the design enables us to test 4 - 1'- , " ,
by asking whether the
zeros in
are reachable in the end (this can be done using transitions such as
in Figure
2, which consumes an equal amount of tokens from and
). As the reachability problem for VASS is
decidable, the query 2 O . is therefore decidable as well. In view of the above, we have
that the set of the minimal elements of 2 is effectively computable. This, together with the effective
computability of the set of the maximal elements of (see [3]), yields Condition (3) of
the definition of the s-decidability. Hence, is s-decidable. Theorem 3.1 implies the decidability of the
OPO problem.
Figure 2. Decidability proof of
?
3.2. One-Counter Machines
A one-counter machine consists of a finite-state control equipped with a counter on which three types
of operations, namely, addition, subtraction and test-for-zero can be performed. For convenience, we use the following to denote the above three basic operations:
(1)
, 2 (resp.,76 ), meaning that can go from state to state
by adding to the
counter (resp., by subtracting from the counter, provided that the value of the counter is greater
than or equal to )
(2)
, meaning that can go from state to state
provided that the value of the counter is zero.
Given a one-counter machine , we denote by
and
the sets of states and transitions of ,
respectively. A configuration of one-counter machine is a pair ( ), where
, and
(indicating the value of the counter). Suppose is the initial state of , the configuration is
called the initial configuration of . Given two configurations - ,
- , and a transition , we write - -
iff one of the following holds:
1. 3 , and - -. E , 2. 3 and - - .
A simple positive loop in is a sequence of transitions
% (%, for
some - 2 4 such that for all4 - 1 . - - , .
, and
%
$#+
(K . In words, a simple positive
loop is a cycle (without test-for-zero transitions) in ’s transition diagram along which no state repeats
itself except the first and the last, and the counter has a positive gain in value along the cycle.
Before proceeding, we require the following result which is a direct consequence of a similar one in [16].
Lemma 3.1. Let be a one-counter machine of size (with the usual measure of size). If -
-
, then there exists a computation -
-
, for some transition sequence O , along
which every configuration in has - %
-A3 -
-
.
Proof:
In Lemma 4.3 of [16], it was shown that for one-counter machines in which the counter can only be incre-mented or decreincre-mented by 1, the reachability of
-
from - is witnessed by a short computation
along which the counter never exceeds %
-A3 -
-
, where is the number of transitions of
the machine. In our one-counter machine model, up to can be added to or subtracted from the counter
in a single transition. Hence, our one-counter machines of size can easily be simulated by those defined
in [16] using at most transitions. The lemma follows immediately.
Lemma 3.2. Given a one-counter machine and two states and
, is effectively semilinear. Proof:
is the union of the following two sets:
V =
and sequence does not use any test-for-zero moves . As
one-counter machines without test-for-zero moves are computationally equivalent to 1-dimensional VASSs,
can be characterized as the reachability set of a 2-dimensional VASS in the
following way. We construct a 2-dimensional VASS with to
sim-ulate the computation of in such a way that
is witnessed by the following
computation of : , where repeating
transition 4 4 times is to initialize the counter value, and in the course of
,
simulates ’s transitions using the second vector position to keep track of ’s counter value
while keeping the first vector position intact. The semilinearity of
follows
imme-diately from [11], which shows the reachability sets of 2-dimensional VASSs to be effectively semilinear.
V =
and sequence uses some test-for-zero moves . Consider
a computation !
such that and
are test-for-zero moves, and sequences , and do not use any test-for-zero moves (here ! and
are the first and last, respectively, configurations along the above
compu-tation at which test-for-zero moves are carried out. Also notice that 3 ! may be equal to and to
). We define a binary relation
on
such that
iff
in . According to Lemma 3.1, using a depth-first search the relation
can effectively be com-puted. Now !
, which is expressible in Presburger Arithmetic.
Lemma 3.3. A one-counter machine (with initial state ) has an infinite non-OPO computation iff one
of the following holds:
(1) there exists a configuration such that
and . ,
(2) there exist a configuration and a simple positive loop starting from state such that
, K , and 2 %
. (notice that test-for-zero transitions
are absent in).
Proof:
The if ( ) part is rather obvious; now we show the only if ( ) part.
Suppose 0
0 is a non-OPO computation of infinite length. Then one of the
following must hold:
(A) there exist indices1 1 6 such that
+
, or
(B) the counter grows unboundedly and there exists an1 such that the counter never becomes zero after
and there exists a simple positive loop which appears infinitely often in
. If (A) is the case, then condition (1) follows immediately. Consider case (B). Let
, for some K . We claim that % % constitutes
an infinite non-OPO computation. If this is not the case, there must exist an integer K such that W !%
. Consider Figure 3, where
is the configuration such that appears
times in . Clearly, % TTT
is executable (for the test-for-zero operation is never used after
), which contradicts the assumption that
be on a non-OPO computation
.
Theorem 3.3. TheOPO problem for one-counter machines is decidable.
Proof:
The proof is carried out through the use of the unified strategy stated in Theorem 3.1. For a one-counter machine , Lemma 3.2 establishes the effective semilinearity of
, . 2
is trivially semilinear, for the finiteness of
.
, an is in J J iff the following holds: (i)
&/2 . ), (ii)
σ1 σ2 σ3 σ1 σ2 σj σj σ3 l l l l l non-ss computation d h d =i
. . .
(q,r) (q,r+j*d). . .
Figure 3. A simple positive loop witnessing non-
. implies .
, and (iii) 2 implies
& EK 2 .
; hence, J J is clearly effectively semilinear. As a result, checking of 9
IJ J . is decidable.
Recall from Lemma 3.2 that for arbitrary and
,
is always semilinear. It is
also well known that semilinear sets are exactly those that can be expressed by formulas in Presburger Arithmetic. If has an infinite non-ss computation, then the formula stated in Condition (2) of the
definition of w-decidability can be expressed in Presburger Arithmetic; hence, checking the validity of the formula is decidable since Presburger Arithmetic is a decidable logic. This, together with Lemma 3.3, establishes the w-decidability property of . According to Theorem 3.1, the OPO problem is decidable.
3.3. Conflict-Free Petri Nets
A Petri Net (PN, for short) is a 3-tuple (P,T, ), where P is a finite set of places, T is a finite set of
transitions, and is a flow function : (P T)= (T P) 0, 1 . A marking (or configuration) is a
mapping, : P N. A marked PN is a 2-tuple ( , ) where (=(P,T, )) is a PN and, is a marking
(, : P N) called the initial marking. A transition t T is enabled at a marking, iff for every p P, (p,t) - , (p). A transition t may fire at a marking, if t is enabled at, . We then write,
, , where ,
(p) =, (p) – (p,t) + (t,p) for all p P. A sequence of transitions
t ...t is a firing sequence from , iff, , 0
, for some sequence of markings,3 ,...,, .
To simplify our notations,
, , , 2 ,
andJ J are abbreviated as ,
, , 2 , and J J , respectively, since configurations (i.e., markings) of Petri nets belong to the set
.
V
Conflict-free Petri nets:
A PN (P, T, ) is said to be conflict-free iff for every place , either
1. " -54 , or
2. , and are on a self-loop (i.e., ),
where = K , (resp., = K , ) represents the set of output (resp.,
more than one transition is also an output of each such transition [13]. In a conflict-free PN, once a transition becomes enabled, the only way to disable the transition is to fire the transition itself (that is, T, . ,, , and , implies, ).
To show theOPO problem for conflict-free PNs to be decidable, we require the following lemmas.
Lemma 3.4. Given a conflict-free PN and a marking, , the set is effectively semilinear.
Proof:
The semilinearity of the reachability set for conflict-free PNs was originally illustrated in [13]. Subse-quently, it has been shown in [12] that, given a conflict-free PN , reachability can be
char-acterized as a system of linear inequalities ( over variables
33 ,
among others, such that
(1) the size of( is bounded by a polynomial in the size of ,
(2) given two markings, and,
,,
,
, for some sequence
, if and only if( has an integer
solution while assigning, to and,
to , and
(3) for each transition , the solution of variable 3
in( exactly equals the number of
times transition fires in
.
As a result, is clearly effectively semilinear.
Lemma 3.5. Given a PN = , the set J J is effectively semilinear (here can be a
general Petri net, not necessarily conflict-free, for which the range of is N).
Proof: Let % . We define = "+ ! ! 4 - 1F- - 4 - - FK , (for each and , has at least one input place in ). is clearly a finite set. We
also let , , K , and . , , , for a
given . Notice that , is finite and contains dead markings only. If ,
is a marking such that
, 3 , 4W- - , and , 2C, . , then,
is a dead marking as well. Hence the set of dead markings equals
7 , , 2., , , , which is
semilinear since and, range over finite sets.
Lemma 3.6. (From [18]) For an arbitrary path,
, in a conflict-free PN = , can be re-arranged into
, for some sequences and integers , 4W- - , such that (1). ( 4W- 1 - ) ( T) ( '-54 ), and (2). ( 4W- 1 - 4 ) ( . ), where
denotes the number of occurrences of in
, and
is the set of transitions fired in
The above lemma allows us to rearrange an arbitrary firing sequence in a conflict-free PN into a ‘canoni-cal form’ satisfying conditions (1) and (2), in which (1) ensures that for each
, no transition will appear
more than once (hence,
- , for all1), and (2) says that
forms a ‘shrinking’
sequence of sets in the sense that if a transition, say , occurs in
, for some 1, then is guaranteed
to appear in
4A- 7-/1. Symmetrically, if does not appear in
, then it will never be found in
1 -
-
.
Lemma 3.7. If an infinite non-OPO computation exists in a conflict-free PN = (with initial
marking, ), then there exist markings, ,
and a ‘short’ sequenceU (i.e.,
Q '-54 ) such that , Q , ,,
2C, , and, QSQSQPT TT is an infinite non-OPO computation.
Proof:
Consider an arbitrary infinite non-OPO computation from, . Suppose we consider the suffix computation
along which all the transitions appear infinitely many times. By applying Dickson’s Lemma [6] to
, can be written as # such that , , , with ,
2 , , and all the transitions in
occur infinitely often in . Let
be the canonical rearrangement of
guaranteed by Lemma 3.6. Clearly
must be that if, , , then, 2C, ; otherwise, , '6C,
due to Condition (2) of Lemma 3.6 (to see this, the conflict-freedom property and (2) of Lemma 3.6, together with the fact that - 4 , imply that no transitions will deposit tokens
to a place in any of the segments
if ,
6., ). Finally, since all the transitions in
occur infinitely often in the infinite non-OPO computation, we claim that,
TTT constitutes an infinite
non-OPO computation. Suppose, in contrast, that for some , ,
( , and , , . Let . Let be a prefix of such that -
(i.e., all the transitions of
occur in ). Assume that,
, , for some , . , . Due to the conflict-freedom property of ,
, ,, , and ( -
) imply the existence of a such that
is a permutation of , and, ,
, (see [13]), contradicting the assumption that, . , . By lettingU
, our
result follows.
We are now in a position to show theOPO problem to be decidable.
Theorem 3.4. TheOPO problem for conflict-free PNs is decidable.
Proof:
Again, the proof is done through the use of Theorem 3.1. The semilinearity of (and hence ) and J J follows from Lemmas 3.4 and 3.5, respectively. being finite clearly
implies the semilinearity of 2 . As a result, checking if there exists some marking such that IJ J . is decidable, and the predicate stated in Condition (2) of the definition of
w-decidability can be expressed in Presburger Arithmetic. This, together with Lemma 3.7 (which certifies
Condition (1) of the definition of w-decidability), establishes w-decidability of . The OPO problem is
3.4. Lossy Counter Machines and Lossy Channel Systems
Like one-counter machines, an -counter machine consists of a finite-state control equipped with counters , on which three types of operations, namely, addition, subtraction, and
test-for-zero can be performed. A configuration of is a tuple - - , where is a state of and - - - 2 4W- 1 -C are the values of counters , respectively. The initial
configu-ration of is , where is the initial state of .
Let
be a relation defined as follows [14]: - - - - - - iff - - - 3 - - - $#+ - )K $#+ - . A relation
is said to be a lossiness relation if 1
, where1
is the identity relation. A
lossy counter machine (( , for short) is a counter machine whose transition relation is defined as O" O iff O O 'O" O O O , whereO O O O
are configurations, meaning that before and/or after a conventional counter machine transition (i.e., ), the counter value may spontaneously
decrease. The reader is referred to [14] for more about LCMs under various lossiness relations. In [14], for every lossiness relation the following problem was shown to be undecidable:
V
(Structural termination) Given an -counter LCM , does terminates for every initial state?
The negation of the problem is that given an -counter LCM with initial state , does there
exist- - N and a state such that there is an infinite run emanating from - - ?
In fact, as shown in [14] the undecidability result holds even when is restricted to contain five counters
and is strongly-cyclic and input-bounded.
Theorem 3.5. TheOPO problem for LCMs is undecidable for every lossiness relation.
Proof:
The proof is done by showing that, given an LCM , we can construct an LCM
in such a way that
is structurally nonterminating iff
is not self-stabilizing. The construction is depicted in Figure 4, in which and
are the initial states of
and
, respectively.
is constructed from by
adding two new states, namely,
and
, and the following transitions. For each state in , we add a
transition from to which is always executable (for example, adding zero to the first counter). In state , self-loops are attached each subtracts one from the respective counter. A transition is introduced
from to
which is enabled provided that all the counters are zero. Finally, from
to
there are transitions each of which subtracts one from the respective counter. Now it is not difficult to see the
following:
V
The reachability set of
is exactly
, since the transition from
to
can never
be executed from the initial configuration
.
V
The only dead configuration of
is . V
Every infinite computation of
must always begin and stay in , regardless of the counter
-1 from 2nd . . . counter -1 from n-th -1 from 1st counter counter p r q 0 q’ 0 add 0 to 1st counter
M
M’
test-for-zero on all counters . . . -1 from 1st counter counter -1 from n-thFigure 4. Reduction from structural nontermination to non-
.
In view of the above, we conclude that
has an infinite non-OPO computation iff is structurally
nonterminating with respect to every lossiness relation. This completes the proof of the theorem.
A lossy channel system [1] consists of a finite number of finite-state machines that communicate with each other over imperfect FIFO channels. Imperfect channels refer to those that are subject to loosing arbitrary amount of messages spontaneously in the course of a computation. See, e.g., [1, 4] for more about lossy channel systems and the related results. As lossy counter machines are special cases of lossy channel systems, theOPO problem for lossy channel systems is therefore undecidable, immediately
following the result of Theorem 3.5.
Corollary 3.1. TheOPO problem for lossy channel systems is undecidable.
4.
Conclusions and Future Research
We have studied, from the decidability viewpoint, the problem of determining whether a given system is self-stabilizing or not for a variety of infinite-state systems. To this end, we have developed a unified strategy through which the problems for one-counter machines, conflict-free Petri nets, and lossy vector
addition systems with states were shown to be decidable. The key behind our strategy is that for each of
the three classes of systems, the reachability set from an arbitrary configuration is effectively semilinear, and it suffices to consider infinite non-self-stabilizing computations with periodic behaviors.
It is interesting to see whether our strategy can be applied to a wider class of infinite-state systems, or a similar strategy (without relying on the reachability set being semilinear) can be extended to systems not enjoying the semilinearity property. An equally important direction of future research is to find out the exact complexity of the self-stabilization problem for the above classes of systems. Finally, self-stabilization for real-time systems deserves further investigation, as many real-world systems are
of real-time nature. For the model of timed automata [2], the region graph technique can easily be applied to showing the decidability (in fact, in PSPACE) of self-stabilization (in the sense defined in this paper). However, to cope with the nature of real-time systems, one might have to tailor the notion of self-stabilization to better capture the intuitive concept of ‘self-stabilizing in a certain amount of time,’ as opposed to ‘reaching a legitimate configuration eventually’ as defined in the conventional sense.
Acknowledgment: The authors would like to thank the anonymous referees for suggestions that greatly
improved the content as well as the presentation of our results.
References
[1] Abdulla, P., Jonsson, B.: Undecidable verification problems for programs with unreliable channels, Inform.
and Comput., 130, 1996, 71–90.
[2] Alur, R., Dill, D.: A theory of timed automata, Theoret. Comput. Sci., 126, 1994, 183–235.
[3] Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems, Proc. of STACS’99, 1563, 1999. [4] C´ec´e, G., Finkel, A., Iyer, S.: Unreliable channels are easier to verify than perfect channels, Inform. and
Comput., 124(1), 1996, 20–31.
[5] Cherkasova, L., Howell, R., Rosier, L.: Bounded self-stabilizing Petri nets, Acta Informat., 32, 1995, 189– 207.
[6] Dickson, L.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors,
Amer. J. Math., 35, 1913, 413–422.
[7] Dijkstra, E.: Self-stabilizing systems in spite of distributed control, C. ACM, 17, 1974, 643–644. [8] Ginsburg, S.: The mathematical theory of context-free languages, McGraw-Hill, 1966.
[9] Gouda, M., Howell, R., Rosier, L.: The instability of self-stabilization, Acta Informat., 27, 1990, 697–724. [10] Herman, T.: A comprehensive bibliography on self-stabilization, Chicago Journal of Theoretical Computer
Science, Available from http://www.cs.uiowa.edu/ftp/selfstab/bibliography, 1998.
[11] Hopcroft, J., Pansiot, J.: On the reachability problem for 5-dimensional vector addition systems, Theoret.
Comput. Sci., 8(2), 1979, 135–159.
[12] Howell, R., Rosier, L.: On questions of fairness and temporal logic for conflict-free Petri nets, Advances in
Petri Nets 1988 (G. Rozenberg, Ed.), 340, Springer-Verlag, Berlin, 1988.
[13] Landweber, L., Robertson, E.: Properties of conflict-free and persistent Petri nets, J. Assoc. Comput. Mach., 25, 1978, 352–364.
[14] Mayr, R.: Undecidable problems in unreliable computations, Theoret. Comput. Sci., 297(1-3), March 2003, 337–354.
[15] Presburger, M.: ¨Uber die vollst¨andigkeit eines gewissen systems der arithmetik ganzer Zahlen, Comptes
Rendus du I congres de Mathematiciens des Pays Slaves, 1929, 92–101.
[16] Rosier, L., Yen, H.: Logspace hierarchies, polynomial time and the complexity of fairness problems concern-ing -machines, SIAM J. Computing, 16(5), 1987, 779–807.
[17] Valk, R., Jantzen, M.: The residue of vector sets with applications to decidability in Petri nets, Acta
Infor-matica, 21, 1985, 643–674.
[18] Yen, H., Wang, B., Yang, M.: Deciding a class of path formulas for conflict-free Petri nets, Theory of