Coexisting mutations/polymorphisms of the long QT syndrome genes in patients with repaired Tetralogy of Fallot are associated with the risks of life-threatening events

16  Download (0)

全文

(1)

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



(2)

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

(3)

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

. . .

0

R(S,c )

0 c

(4)

Let ( ) 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

(5)

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 % .        &

(6)

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 '

(7)

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 





(8)

(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.

(9)

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.

(10)

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)   

(11)

σ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.,

(12)

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  

(13)

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

(14)

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

(15)

-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-th

Figure 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

(16)

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

數據

Figure 1. Non-self-stabilizing computations.

Figure 1.

Non-self-stabilizing computations. p.3
Figure 2. Decidability proof of 	


Figure 2.

Decidability proof of    p.8
Figure 3. A simple positive loop witnessing non-  .

Figure 3.

A simple positive loop witnessing non-  . p.11
Figure 4. Reduction from structural nontermination to non-  .

Figure 4.

Reduction from structural nontermination to non-  . p.15

參考文獻

相關主題 :