Decidability Analysis of SelfStabilization for InfiniteState Systems
HsuChun Yen
and LienPo 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 infinitestate systems, the problem of deciding whether a given system is selfstabilizing or not is investigated from the decidability viewpoint. We develop a unified strategy
through which checking selfstabilization is shown to be decidable for lossy vector addition systems
with states, onecounter machines, and conflictfree Petri nets. For lossy counter machines and lossy channel systems, in contrast, the selfstabilization problem is shown to be undecidable.
Keywords: Decidability, infinitestate systems, selfstabilization, Petri nets.
1.
Introduction
The notion of selfstabilization was introduced by Dijkstra [7] to describe a system having the behavior 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 selfstabilization is that a selfstabilizing 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, selfstabilizing systems exhibit tolerant behaviors to a certain degree. With the increased interest in designing faulttolerant systems, the study of selfstabilization 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 selfstabilization.
Research supported in part by NSC 932213E002003, and NSC 942213E002087, Taiwan
Following the seminal work of Dijkstra [7], the majority of research along the line of selfstabilization has been focusing on providing solutions (and their proofs) for selfstabilizing systems with a variety of properties and topologies (see [10] for a bibliography of selfstabilization). In a somewhat different direction of research, Gouda, Howell and Rosier ([9]) have showed that the property of selfstabilization 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
respect to the property of selfstabilization. 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 wellstudied 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, selfstabilization 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 selfstabilization to the model of Petri nets. In a subsequent paper [5], specific efforts have been devoted to reasoning about selfstabilization aspects of Petri nets from the computational complexity point of view. Among those complexity results derived in [5], detecting whether a Petri net is selfstabilizing is complete for polynomial time for bounded ordinary Petri nets, whereas it is PSPACEcomcomplete for bounded general Petri nets.
As far as we know, very little is known regarding the complexity of the selfstabilization problem (i.e., the problem of deciding whether a system is selfstabilizing or not) for infinitestate 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 infinitestate systems, in the hope of recognizing the key characteristics which govern the decidability/undecidability nature of the problem. An equally important goal is to, perhaps, come up with a unified framework through which decidability/undecidability of selfstabilization 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 selfstabilizing for a wide range of infinitestate systems, including
lossy vector addition systems with states, onecounter machines, conflictfree Petri nets, lossy counter machines, and lossy channel systems. As it turns out, the decidability of selfstabilization for lossy vector addition systems with states, onecounter machines, and conflictfree Petri nets can be established in
a unified setting, taking advantage of the existence of a periodic witness for nonselfstabilizing infinite computations. For lossy counter machines and lossy channel systems, however, the selfstabilization 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 selfstabilized or not from the decidability viewpoint for a variety of infinitestate systems. A conclusion is given in Section 4.
2.
Preliminaries
A transition system (or system, for short) is a fourtuple , 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 selfstabilizing (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 selfstabilizing 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 nonselfstabilizing (nonss) 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 selfstabilizing if for each configuration , none of the computations
emanating from is nonss. The selfstabilization problem is to determine, for a given (finite or infinite)
system, whether the system is selfstabilizing. In this paper, our main concern is to investigate the decidability issue of the selfstabilization problem for a variety of infinitestate systems for which the existence of a nonreachable dead configuration is decidable. The formal definitions of configurations and computations of each individual system will be clarified as our discussion progresses.
infinite nonss 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., /01, ) implies / , where the ordering  in N
is the componentwise extension of the natural ordering in N. Given an upwardclosed 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 downwardclosed set J is said to be maximal if there is no 4 .+3 J such that 4LKM3 . We writeA3 IJ to denote the set of maximal elements ofJ . From Dickson’s lemma, it is
wellknown that for each upwardclosed 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 infinitestate models, including lossy vector addition systems
with states, onecounter machines, and conflictfree 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 selfstabilizing iff either (i) a finite
computation ends up with a dead configuration being not reachable from the initial configuration, or (ii) an infinite nonOPO 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 nonOPO nature of a system, it is sufficient to search among only nonOPO computations
of periodic behaviors, and hopefully, the confinement to such computations admits a decidable checking of (ii). By nonOPO periodic computations we mean those nonOPO computations of the formORQSQPT TT, i.e.,
repeatingU fromO infinitely many times witnesses nonOPO . In our subsequent investigation, we
characterize the following two types of nonOPO 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 nonOPO
of its infinite repetition (i.e., QSQPT TT is nonOPO ).
V
The disparity between strongly and weakly periodic nonOPO computations is that in the former, a
finite computation of the form ‘ Q
with
2 and . ’ is guaranteed to conclude the
system’s nonOPO 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 sdecidability property (or simply called sdecidable) if the following
holds:
(1) has an infinite nonOPO 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 . !
Sdecidable systems correspond to systems whose nonss behaviors can be captured by nonss
computations of the strongly periodic type. What (1) says is that for sdecidable systems, infinite nonss behaviors are witnessed by the existence of a periodic computation. Furthermore, (2) suggests the legitimacy of repeating a finite sequence infinitely many times to yield an infinite nonss computation. As a result, any finite sequence satisfying the premise stated in (2) is sufficient to guarantee an infinite periodic nonss computation. Finally, (3) simply says that finding a finite sequence meeting Condition (2) is decidable.
V
System is said to have the wdecidability property (or simply called wdecidable) if the following
holds:
(1) has an infinite nonOPO 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 % . &
Wdecidable systems correspond to systems whose nonss behaviors can be captured by nonss
computations of the weakly periodic type. Like the case in sdecidability, (1) suggests that infinite nonss behaviors are witnessed by the existence of a periodic computation. Condition (2) further ensures that checking the existence of a periodic nonss 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 infinitestate systems for which the existence of a nonreachable 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 sdecidable or wdecidable, 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 nonreachable dead configuration exists or not. It remains to consider those systems for which nonss is witnessed by the existence of infinite nonss computations. First consider the case when is sdecidable. In this case, has infinite nonss computations
iff Condition (1) of the definition of sdecidability holds, meaning that the nonss is witnessed by a periodic computation. Furthermore, the formula in Condition (3) of the definition of sdecidability 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 sdecidability, the above implies the validity of the infinite nonss computation O
O O %
. Hence, is nonss. On the other hand,
if has an infinite nonss computation, then there is a finite computation O
O
satisfying
Condition (1) of the definition of sdecidability; hence, the O
above satisfy . In view of the above,
the formula holds iff has a nonss computation.
Now consider a wdecidable system . Our decision procedure for theOPO problem involves checking
whether the formula " in Condition (2) of the definition of wdecidability holds or not. Suppose "
holds and let O
be the values that satisfy " . Then clearly O
O! O! %
witnesses an infinite nonss computation. On the other hand, being nonss, in conjunction with
Condition (1) of the definition of wdecidability, 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,
onecounter machines and conflictfree Petri nets to be either sdecidable or wdecidable; 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 5tuple , 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 nonss is witnessed by infinite nonss
computations. In what follows, we show to be sdecidable.
Suppose has an infinite nonOPO computation ,
(for some transition
sequences
). 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
sdecidability hold.
Now we show Condition (3) of the definition of the sdecidability, i.e., the decidability of 9 O 9 O OF
O . . Consider the
set 2 PO O OW . Clearly, 2 is upwardclosed. In [17], it
was shown that for each upwardclosed 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 wellknown 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 AH , ,
. 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 sdecidability. Hence, is sdecidable. Theorem 3.1 implies the decidability of the
OPO problem.
Figure 2. Decidability proof of
?
3.2. OneCounter Machines
A onecounter machine consists of a finitestate control equipped with a counter on which three types
of operations, namely, addition, subtraction and testforzero 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 onecounter machine , we denote by
and
the sets of states and transitions of ,
respectively. A configuration of onecounter 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 testforzero 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 onecounter 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 onecounter machines in which the counter can only be incremented or decreincremented 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 onecounter machine model, up to can be added to or subtracted from the counter
in a single transition. Hence, our onecounter 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 onecounter machine and two states and
, is effectively semilinear. Proof:
is the union of the following two sets:
V =
and sequence does not use any testforzero moves . As
onecounter machines without testforzero moves are computationally equivalent to 1dimensional VASSs,
can be characterized as the reachability set of a 2dimensional VASS in the
following way. We construct a 2dimensional VASS with to
simulate 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
immediately from [11], which shows the reachability sets of 2dimensional VASSs to be effectively semilinear.
V =
and sequence uses some testforzero moves . Consider
a computation !
such that and
are testforzero moves, and sequences , and do not use any testforzero moves (here ! and
are the first and last, respectively, configurations along the above
computation at which testforzero 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 depthfirst search the relation
can effectively be computed. Now !
, which is expressible in Presburger Arithmetic.
Lemma 3.3. A onecounter machine (with initial state ) has an infinite nonOPO 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 testforzero transitions
are absent in).
Proof:
The if ( ) part is rather obvious; now we show the only if ( ) part.
Suppose 0
0 is a nonOPO 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 nonOPO 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 testforzero operation is never used after
), which contradicts the assumption that
be on a nonOPO computation
.
Theorem 3.3. TheOPO problem for onecounter machines is decidable.
Proof:
The proof is carried out through the use of the unified strategy stated in Theorem 3.1. For a onecounter 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 nonss 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 nonss computation, then the formula stated in Condition (2) of the
definition of wdecidability 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 wdecidability property of . According to Theorem 3.1, the OPO problem is decidable.
3.3. ConflictFree Petri Nets
A Petri Net (PN, for short) is a 3tuple (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 2tuple ( , ) 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
Conflictfree Petri nets:
A PN (P, T, ) is said to be conflictfree iff for every place , either
1. " 54 , or
2. , and are on a selfloop (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 conflictfree 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 conflictfree PNs to be decidable, we require the following lemmas.
Lemma 3.4. Given a conflictfree PN and a marking, , the set is effectively semilinear.
Proof:
The semilinearity of the reachability set for conflictfree PNs was originally illustrated in [13]. Subsequently, it has been shown in [12] that, given a conflictfree PN , reachability can be
characterized 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 conflictfree, 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 conflictfree PN = , can be rearranged 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 conflictfree PN into a ‘canonical 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 nonOPO computation exists in a conflictfree 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 nonOPO computation.
Proof:
Consider an arbitrary infinite nonOPO 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 conflictfreedom 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 nonOPO computation, we claim that,
TTT constitutes an infinite
nonOPO 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 conflictfreedom 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 conflictfree 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
wdecidability can be expressed in Presburger Arithmetic. This, together with Lemma 3.7 (which certifies
Condition (1) of the definition of wdecidability), establishes wdecidability of . The OPO problem is
3.4. Lossy Counter Machines and Lossy Channel Systems
Like onecounter machines, an counter machine consists of a finitestate control equipped with counters , on which three types of operations, namely, addition, subtraction, and
testforzero 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
configuration 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 stronglycyclic and inputbounded.
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 selfstabilizing. 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 , selfloops 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 nth 1 from 1st counter counter p r q 0 q’ 0 add 0 to 1st counter
M
M’
testforzero on all counters . . . 1 from 1st counter counter 1 from nthFigure 4. Reduction from structural nontermination to non
.
In view of the above, we conclude that
has an infinite nonOPO 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 finitestate 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 selfstabilizing or not for a variety of infinitestate systems. To this end, we have developed a unified strategy through which the problems for onecounter machines, conflictfree 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 nonselfstabilizing computations with periodic behaviors.
It is interesting to see whether our strategy can be applied to a wider class of infinitestate 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 selfstabilization problem for the above classes of systems. Finally, selfstabilization for realtime systems deserves further investigation, as many realworld systems are
of realtime 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 selfstabilization (in the sense defined in this paper). However, to cope with the nature of realtime systems, one might have to tailor the notion of selfstabilization to better capture the intuitive concept of ‘selfstabilizing 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 selfstabilizing 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.: Selfstabilizing systems in spite of distributed control, C. ACM, 17, 1974, 643–644. [8] Ginsburg, S.: The mathematical theory of contextfree languages, McGrawHill, 1966.
[9] Gouda, M., Howell, R., Rosier, L.: The instability of selfstabilization, Acta Informat., 27, 1990, 697–724. [10] Herman, T.: A comprehensive bibliography on selfstabilization, 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 5dimensional vector addition systems, Theoret.
Comput. Sci., 8(2), 1979, 135–159.
[12] Howell, R., Rosier, L.: On questions of fairness and temporal logic for conflictfree Petri nets, Advances in
Petri Nets 1988 (G. Rozenberg, Ed.), 340, SpringerVerlag, Berlin, 1988.
[13] Landweber, L., Robertson, E.: Properties of conflictfree and persistent Petri nets, J. Assoc. Comput. Mach., 25, 1978, 352–364.
[14] Mayr, R.: Undecidable problems in unreliable computations, Theoret. Comput. Sci., 297(13), 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 concerning 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
Informatica, 21, 1985, 643–674.
[18] Yen, H., Wang, B., Yang, M.: Deciding a class of path formulas for conflictfree Petri nets, Theory of