Analysis of self-stabilization for infinite-state systems

(1)

Analysis of Self-stabilization for Infinite-State Systems

Hsu-Chun Yen

Dept. of Electrical Engineering

National Taiwan University

Taipei, Taiwan

106,

R.O.C.

[email protected]

Abstract

The problem of deciding whether an injinite-state sys- tem is self-stabilizing or not is investigated from the de- cidability viewpoint in this paper: We develop a unijied strategy through which checking self-stabilization is shown to be decidable for one-counter machines and conflict-free Petri nets. Our strategy relies on the reachability sets be- ing semilinear; as well as on the capability of extracting periodic behaviors of injinite computations, which, in turn, facilitates the expression of self-stabilization by Presburger

Arithmetic.

As fairness is frequently used as a qualitative measure to capture the notion of a quantitative measure of ‘something happens with probability one,’ it is of interest to examine the fair version of the self-stabilization problem, i.e., the problem of asking whether all ‘fair’ injinite computations eventually become self-stabilizing. We propose a potential method through which the problem is shown to be decidable for conjlict-free Petri nets.

Keywords: Decidability, infinite-state system, Petri net, self-stabilization.

1 Introduction

The notion

of

self-stabilization was introduced by Dijk- stra [ 3 ] to describe a system having the behavior that regard- less 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 motiva- tion 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 fault- 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.

Following the seminal work of Dijkstra [ 3 ] , the major- ity 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 topolo- gies. (See [ 6 ] for a bibliography of self-stabilization.) In a somewhat different direction of research, Gouda, How- ell and Rosier ( [ 5 ] ) 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 ba- sically 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 self-stabilization. (The simulation paradigm, simply speaking, is a methodol- ogy 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 [SI.) To our knowledge, [SI also pioneers the introduction of the notion of self-stabilization to the model

of Petri nets. In a subsequent paper [I], 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 [ 11, detecting whether a Petri net is self-stabilizing is complete for polynomial time for bounded ordinary Petri nets, whereas it is PSPACE-complete for bounded general Petri nets.

As far as we know, very little is known regarding the decidability/complexity issue of the self-stabilization problem (i.e., the problem of deciding whether a system is self-

(2)

stabilizing or not) for infinite-state systems. At this mo- ment, the best bounds of the problem for general Petri nets are a lower bound of exponential space and an up- per bound of I I 2 (the second level of the arithmetic hier- archy), whereas it is II2-complete for Turing machines [ 11.

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 decidabilityhndecidability nature of the problem. An equally important goal is to, perhaps, come up with a uni- fied framework through which decidabilityhndecidability of self-stabilization can be obtained. In this paper, we ex- tend the work of [ 11 by investigating, from the decidability viewpoint, the problem of deciding whether a given system is self-stabilizing for one-counter machines and conjlict- free Petri nets. As it turns out, the decidability of self- stabilization for these two computational models can be established in a unified setting, taking advantage of the following key properties:

1 . The reachability set as well as the set of ‘dead’ configurations are effectively semilinear,

2. The existence of a periodic witness for non-self- stabilizing infinite computations.

The above properties allow us to formulate self-stabilization in terms of formulas in Presburger Arithmetic, giving rise to the decidability result.

As ‘fairness’ is frequently used as a qualitative measure to capture the notion of a quantitative measure of ‘something happens with probability one,’ it is of interest to re- examine the self-stabilization problem by asking whether all ‘fair’ infinite computations eventually enter legitimate states. We propose a ‘potential method’ through which the problem is shown to be decidable for a restricted class of

Petri nets. The idea is to associate a value (called ‘potential’) with each marking in the Petri net in such a way that the potential along any Petri net computation is non- increasing, and in some cases, has the tendency to move towards the ground level (i.e., potential zero). To a certain degree, the basic idea of our potential method is analogous to the analysis of neural nets (in particular, Hopjield nets), in which an energy function is associated with a Hopfield net, and the energy of the net decreases as the computation proceeds (provided that the net meets certain conditions) which, in turn, guarantees the convergence of the net.

The rest of this paper is organized as follows. In Sec- tion 2, we give the definitions of transition systems and self-stabilization. Section 3 deals with the issue of deciding whether a given system is self-stabilized or not from the decidability viewpoint for infinite-state systems. A fair version of self-stabilization is investigated in Section 4. A conclusion is given in Section 5 .

2 Preliminaries

Let Z (N) denote the set of (nonnegative) integers, and

Z k

(Nk)

the set of vectors of k (nonnegative) integers. A transition system (or system, for short)

S

is a four- tuple ( X , C, 6, co), where X consists of a (possibly infinite) set of conjigurations, C is a (possibly infinite) set of transition symbols, 6 : X x C

-+

2 x

defines the tran- sition function, and C O ( € X ) is the initial configuration. we write c

f

c’ if c’ E ~ ( c , t ) . AISO let

i

(resp.,

3 )

be the reflexive and transitive closure (resp., transitive closure) of

+.

In words, c

i

c’ (resp., c

3

c’) iff c‘ can be reached from c through zero (resp., one) or more transitions. A computation a is a (finite or infinite) sequence c1

3

cz

9 . . .

c,

5

c,+l

. . ..

A configuration c is said to be a dead conjiguration if V t E

C,

6 ( c ,

t )

=

8,

i.e., c has no immediate successor in S. In this paper, we consider only those systems for which X can be encoded in such a way that X Q x

N k ,

for some finite set Q and integer

k

2

1.

(Q is referred to as the set of states of system S.)

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 conjiguru- tion 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 S be a (finite or infinite) system with CO as its initial configu-

ration. Also let

R ( S ,

C O ) (={c

I

CO c } ) denote the set of

reachable conjigurutions from CO. A computation CT from

configuration c1 is said to be non-self-stabilizing (non-ss)

iff one of the following holds:

I . 0 is finite ( a : c1

9

c2

41

...cm-l t ~ c,, l for some m ) such that c, is a dead configuration and c, $

2. a is infinite ( a : c1

3

c2

3 . . .

c,

5

c,+1

.

. .) such

See Figure 1. A system is said to be self-stabilizing if for each configuration c, none of the computations emanating from c is non-ss. The self-stabilization problem is to de- termine, 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. The formal definitions of conjigurations and computations of each indi- vidual system will be clarified as our discussion progresses. For a vector v E Nk and a finite set p (= (211,

...,

wn}, for some n)

N k ,

the set

L ( v ;

p ) = {wl3a1..., a , E N, w =

v

+

a,

*

w,}

is called the linear set with base v over the R ( S , C O ) ,

or

that V i

2

1, c, $

R ( S ,

C O ) .

n

(3)

infinite non-ss computation

the set of

(

initial configuration

\

computation leading to

a ‘legitimate’ configuration

Figure 1. Non-self-stabilizing computations.

set of periods p. A semilinear set ( S L S ) (cf. [4]) is a finite union of linear sets. It is known that semilinear sets are exactly those that can be expressed in Presburger Arithmetic [IO], which is a decidable theory.

3 Decidability analysis

In this section, the ss problem for one-counter ma-

chines and conjlict-free Petri nets will be shown to be de- cidable. 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 ss that a system

S

is not self-stabilizing iff either (i) a dead configuration is not reachable from the initial configuration, or (ii) an infinite non-ss computation exists. As we shall see later, (i) is rel- atively easy to check as long as certain properties of

S

are decidable. The idea behind our approach of checking (ii) is built upon showing that to demonstrate the non-ss nature of

a system, it is sufficient to search among only non-ss com- putations of periodic behaviors, and hopefully, the confine- ment

to

such computations admits a decidable checking

of

(ii). By non-ss periodic computations we mean those non- ss computations of the form s T?., i.e., repeating T from s infinitely many times witnesses non-ss. In our subsequent investigation, we characterize the following two types of non-ss periodic behaviors, through which a unified strategy is developed serving as a foundation for our decidability results of the ss problem.

a (Strongly periodic:) Every finite computation

c

4 c’

with c’

2

c and

c

#

R ( S , c o )

ensures non-ss of its infinite repetition (i.e.,

c

TT...

+

is non-ss). .

(Weakly periodic:) If an infinite non-ss computation

exists, there must exist a witness T which is in a computable finite set, and

c

%’

constitutes an infinite non- ss computation.

The disparity between strongly and weakly periodic non- ss computations is that in the former, a finite computation of the form ‘c

4

c‘ with c’

2

c and

c

$!

R ( S ,

Q)’ is guar- anteed to conclude the system’s non-ss behavior, whereas in the latter, however, not every finite computation of the above form is extendible to render

ss;

nevertheless, there does exist such a witness which is computable. (The

mean-

ing of

‘>’

will become clear as our discussion progresses.) Before going into the details, we require the following notations. Let

S = ( X ,

C ,

6,

Q) be a transition system, where X

C

Q x

N k ,

c E

X ,

and q,q’ E

Q. SUCC(S,q,q‘)

= {(s,s‘)

I

( q , s )

f

(q’,s’), for

REACH+(S,q,q’)

= {(s,s’)

I

( q , s )

3.

( q ’ , s ’ ) } ; some transition

t

E

E},

R E A C H ( S , q , q ‘ )

= {(s,s’)

I

4

( q ’ , s ’ ) } ;

Reach(S,

c , q’) = {s’

I

c

4

(q’, s’)},

R ( S , c )

=

{c’

I

c

4 c’},

a

D E A D ( S ,

q ) = {s

I

( q , s) is a dead configuration}. As we shall see later, decidability of the ss problem for each of the aforementioned computational models is based upon the following unified strategy:

Theorem 3.1 Let X be a computational model f o r which the ss problem is considered.

If

f o r each system

S

= ( X , C, 6, cg) in X , where X

( I ) (Semilinear condition) Vq,q’ E

Q,

the sets

SUCC(S,

q , q’),

R E A C H ( S ,

q , q’) and

D E A D ( S ,

q ) are effectively semilineal; and Q x

N k ,

we have

(2) (Periodic condition)

S

has an infinite non-ss compu-

+

tation irthere exists an injinite computation (q, s)

+

( q , s + d )

f

( q , s + 2 d ) . . - , f o r s o m e ( q , s ) E X a n d d E

N k ,

such that either ( a ) o r ( b ) below holds:

(a) s

#

Reach(S,co,q),

a (s

#

Reach(S,

C O , q ) ) implies (Vn

2 0,

s

+

a ( ( q , s)

f

( q , s+d)) implies ( V n

2

0, (q, s+

a V n

2

0, s

+

n

*

d

#

Reach(S,

C O , q), and

0 d belongs to a computable finite set

D

n

*

d

#

Reach(S,

Q, q ) ) , and n

*

d )

f

(4,s

+

( n

+

l)d)), ( b )

N k ,

then the ss problem is decidable f o r

X .

(Notice that types ( a ) and (b) characterize strongly and weakly periodic non-

(4)

Proof: First notice that if Vq, q’ E

Q , R E A C H ( S ,

q , 4’)

is semilinear, so is

Reach(S,c,q’),

Vc

E X and q‘ E Q.

According to the definition of ss, system

S

is

not

ss iff either (i) a dead configuration is not reachable, or (ii) an infinite non-ss computation exists. The (i) case can be checked by testing (3q E

Q) ( D E A D ( S , q )

n

Reach(S,co,q)

#

8),

which is decidable because of the semilinearity assump- tion of (1). To check (ii), assumption (2) suggests that it is sufficient to look for an infinite non-ss computation of type (a) or (b). Deciding the existence of such a path can be formulated as follows.

Type (a) (i.e., stronglyperiodic case):

VQE&

( 3 S E N k )

(3

d E

N k )

((s,

+

4

E

REACH+(S,

4 , q ) A ( S

$! Reach(S,

CO, 4 ) ) )

which can be expressed in Presburger Arithmetic (due to assumption ( I ) ) .

0 Type (b) (i.e., weaklyperiodic case):

((s

+ n * d , s

+

( n

+ l ) * d ) E

REACH+(S,q,q))

A (s

+

n

*

d $! R e a c h ( S , C O , 4))

,

which can be expressed in Presburger Arithmetic (due to assumption

(1) and the fact that (s,s’) E

REACH+(S,q,q’)

iff (3s’’ E N k ) (3q” E &) ( ( s , ~ ’ ’ ) E S U C C ( S , q , q ” ) ) A

( ( s ” , ~ ’ ) E

REACH(S,q”,q’)).

I

v p ~ Q V d c D

(3

E

Nk)

(v

2

O )

We are in a position to show why each of the models of one-counter machines and conjlict-free Petri nets falls into a special case of Theorem 3.1.

3.1 One-counter machines

A one-counter machine M 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) ( q , q ’ , n ) ,

n

2

0 (resp.,

n

<

0), meaning that

M

can go from state q to state q‘ by adding

n

to the counter (resp., by subtracting In1 from the counter, provided that the value of the counter is greater than or equal to

14)

(2) (4, q‘, = 0), meaning that M can go from state q to state q’ provided that the value of the counter is zero. Given a one-counter machine M , we denote by Mstate and M,, the sets of states and transitions of

M ,

respectively. A conjguration of one-counter machine

M

is a pair (4,

n ) ,

where q E M s t a t e , and

n

E

N

(indicating the value of the counter). Suppose qo is the initial state of

M ,

the configu- ration (qo, 0) is called the initial conjguration of M . Given two configurations (q, m ) , (q’, m’), and a transition

t ,

we write ( q , m )

5

( q ’ ,

m’)

iff one of the following holds:

1

1. t = ( q , q ’ , n ) , n E Z a n d m ’ = m + n , 2.

t

= ( q , q‘, = 0) and m‘ =

m

= 0.

A short positive loop in M is a sequence of transitions such that for all 1

5 i

#

j

5 m,

qi

#

q j , and

(Czl

ni)

>

0. (In words, a short positive loop is a cycle (without test- for-zero transitions) in M’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 [ 113.

Lemma 3.2 Let

M

be a one-counter machine of size

z

(when a binary encoding scheme is used).

If

(q,m) (q’,m’), then there exists a computation T :

(q,m)

4

( q ’ ,

m’),

for some transition sequence

s,

along which every conjguration ( p ,

h )

in T has h

5

3*

( ~ 2 ’ ) ~

+maz{m, m’}.

Proof: In Lemma 4.3 of [ 111, it was shown that for one- counter machines in which the counter can only be incre- mented or decremented by 1, the reachability of (q’,m’) from ( q , m ) is witnessed by a short computation along which the counter never exceeds 3

*

( n ) 3

+

maz{m,m’),

where n is the number of transitions of the machine. In our

one-counter machine model, up to

2’

can be added to or

subtracted from the counter in a single transition. Hence, our one-counter machines of size z can easily be simulated by those defined in [ 111 using at most 22’ transitions. The

lemma follows immediately.

I

(q11q2,~1)(q2,q3,~2)’..(q,tq1,~,) , for Some

m

2

Lemma3.3 Given a one-counter machine

M

and two states q and q’,

R E A C H ( M ,

q , 4’) is effectively semilin- ear:

Proof: two sets:

R E A C H ( M ,

q , 4’) is the union of the following

R ’ ( M , 4 , Q’)={(cId)l(ql

c)

4

( q ‘ , d ) and sequence T does not use any test-for-

zero moves}. As one-counter machines without test-for-zero moves are computationally equivalent to

1 -dimensional VASSs,

R1

(MI

q , 9’) can be characterized as the reachability set of a 2-dimensional VASS in the following way. We construct a 2-dimensional VASS

P

=

( w o , A , ~ o , Q , S )

with W O = (0,O) to

simulate the computation of

M

in such a way that

(c,d)

E

R 1 ( M ,

q , q ’ ) is witnessed by the following computation of

P: (PO,

(0,O))

+

(PO,

( c , c ) )

+

( q , ( c ,

c ) )

4

( q ’ , ( c , d ) ) , where repeating transition

t

: po

-+

(PO, (1,l)) c times is to initialize the counter value, and in the course of 0,

P

simulates

A

(5)

M ' s transitions using the second vector position to keep track of

M ' s

counter value while keeping the first vector position intact. The semilinearity of

R ' ( M ,

q , q') follows immediately from [7], which shows the reachability sets of 2-dimensional VASSs to be effectively semilinear.

.

R 2 ( M , P , q ) = { ( c , d ) l ( p ,

c )

i

( q , d ) and sequence r uses some test-for-zero moves}. Consider a computation ( p ,

c)

1

( P I , c1)

-%

( p i ,

4)

3

(132, c2)

3

( p i , c l )

3

( q , d ) such that

z

and z' are test-for-zero moves, and sequences r1

and 7-3 d o not use any test-for-zero moves. (Here

( P I , c1) and ( p 2 , cg) are the first and last, respectively, configurations along the above computation at which test-for-zero moves are carried out. Also notice that ( p l , c1) may be equal to ( p g , cg) and z to z'.) We define a binary relation

R

on Mstate such that p72q iff

(p,O)

( q , O ) in M . According to Lemma 3.2, using a depth-first search the relation

R

can effectively be computed. Now R 2 ( M , p , q ) = { ( ~ d )

I

3P74

E M s t a t e r

(PRq)

A ( ( ( P , c ) ,

( P , O ) >

E

R ' ( M , P , l ? N A ( ( ( q , O ) , ( q , d ) ) E ~ l ( ~ , w ) } y which is expressible in Presburger Arithmetic.

If (A) is the case, then condition (1) follows immediately. Consider case (B). Let (q,

r )

4

(4,

r

+

d ) , for some d

>

0.

We claim that ( q , r )

4,

( q , r

+

d )

4,

( q , r

+

2 d )

...

4

( q , r

+

3 d )

. . .

constitutes an infinite non-ss computation. If this is not the case, there must exist an integer j

>

0

such that ( q , r + j

*

d ) E

R ( M ,

(qo, 0 ) ) . Consider Figure 2, where d h is the configuration such that 1 appears j times in d i d h . Clearly, ( q , r

+

j

*

d )

-+

d h is executable (for the test-for-zero operation is never used after d i ) , which contradicts the assumption that d h be on a non-ss computation U .

I

U, U2 "'Uj

Figure 2. A short positive loop witnessing non-ss.

Theorem 3.5 The ss 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. First consider Con- dition ( 1 ) of Theorem 3.1. For a one-counter machine

I

Lemma 3.4 A one-counter machine M (with initial state

40) has an infinite non-ss computation g o n e of the follow- ing holds:

( 1 ) there exists a configuration (4, r ) such that ( q , r )

3

( q , r ) and ( Q I . )

#

R ( M ,

( 4 0 , O ) ) .

( 2 ) there exist a configuration ( q , r ) and a short positive loop 1 starting from state y such that ( q , r ) -+ ( q , r'), r'

>

r, and V j

2

O,(q,r

+

j

*

(r' - r ) )

#

R( M ,

( q 0 , O ) ) . (Notice that test-for-Zero transitions

are absent in 1.)

1

Proof: The if ( G ) part is rather obvious; now we show the only if (*) part.

Suppose U : d l

-+

d2

+

...

-+

di

-+

. . .

is a non-ss computation of infinite length. Then one of the following must hold:

(A) there exist indices

i,

j

(i

<

j ) such that d i = d j , or

(B) the counter grows unboundedly and there exists an

i

such that the counter never becomes zero after d i ( = (4, r ) ) and there exists a short positive loop

1

: q -+ q

(in M ' s transition diagram) appears infinitely often in

1

U .

M , Lemma 3.3 establishes the effective semilinearity of trivially semilinear, for the finiteness of Mt,. Vq E Mstate. an r E N is in D E A D ( M , q ) iff the following hold: (i) implies (Vq' E M s t a t , ) ( ( q , q', = 0)

@

Mt,), and (iii) ( r

2

Mt,); hence, D E A D ( M , q ) is clearly effectively semilinear. Condition ( 2 ) of Theorem 3.1 is established in Lemma

3.4. In view of the above, the ss problem

is

decidable.

1 R E A C H ( M ,

4 , q ' ) ,

v

q,q' E M s t a t e .

S u C C ( M ,

974') is

(vd

E M s t a t e )

(vn

2

O ) ( ( q , q ' , n )

@

M t r ) , (ii) ( r = 0)

0) implies (Vq' E M s t a t e ) ( h r

>

n

2

O ) ( ( q , q ' ,

-.I

#

3.2 Conflict-free Petri nets

A Petri Net (PN, for short) is a 3-tuple (P,T,'p), where P is a finite set of places, T is a finite set of transitions, and 'p is ajowfunction 'p : (P x T) U (T x P)

-+

(0, I}. A marking (or conjiguration) is a mapping p : P

-+

N. A marked PN is a 2-tuple

( P ,

P O ) where

P

(=(P,T,(p)) is a PN and po is a marking (po : P

-+

N ) called the initial marking. A transition t E T is enabled at a marking p iff for every p E P, cp(p,t)

5

p(p). A transition t mayfire at a marking p if

(6)

t is enabled at p. We then write p

4

p‘, where p‘(p) = p(p)

-

cp(p,t)

+

cp(t,p) for all p E P. A sequence of transitions (T =

tl

...

tn is afiring sequence from p iff p

3

p1

-3

. .

.

1

pn for some sequence of markings p1, ...,p,.

For ease of expression, the following notations will be used throughout the rest of this paper. Let U , 0’ be transition

sequences, and

t

be a transition.

# u ( t ) represents the number of occurrences o f t in U

0

T T ( u )

=

{tlt

E

T,#,(t)

>

0 } , denoting the set of

(T A o’ is defined inductively as follows. Suppose or =

t1

...

tn. Let go be n. If t, is in ci-1, let ui be ~ ~ - 1

with the leftmost occurrence o f t , deleted; otherwise, let 0% = ( ~ i - 1 . Finally, let CT 2

d

= cn. For example,

if 0 =

tlt~t&t5

and

d

=

t4t3t1,

then 0 A 0‘ =

t2t5.

For firing sequences U and U ’ , u’ is said to be a rearrange- m e n t o f a i f # , ( t )

= # u j ( t ) , V t ~ T .

To simplify our notations,

R E A C H ( P ,

q , q’),

REACH+(P,

q , q’),

Rreach(P,

q , q’),

SUCC(P,

q, 4‘) and

DEAD(P,

q ) are abbreviated as

REACH( P ) , REACH+ ( P ) , Reach(P), SUCC(P),

and

D E A D ( P ) ,

respectively, since configurations (i.e., markings) of Petri nets belong to the set

N“

t

transitions used in U .

Conjict-free Petri nets:

A PN

P

=(P, T, cp) is said to be conflict-free iff for every place p, either

1. IP’)

5 Lor

2.

Vt

E p’,

t

and p are on a self-loop (i.e.,

t

E (p’

n

wherep’={t

I

cp(p,t)

>

O}(resp.,’p={t

I

cp(t,p)

>

0 ) ) represents the set of output (resp., input) transitions of placep. In words, a PN is conflict-free if every place which is an input of more than one transition is also an output of each such transition [9]. 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,

Vt, t’

E T,

t

#

t’,

p

f

p’ and p

4;

implies

‘P)h

p‘ $.)

To show the ss problem for conflict-free PNs to be decidable, we require the following lemmas.

Lemma 3.6 Given a conflict-jjree PN

P= ( P ,

T ,

cp), we can construct in nondeterministic polynomial time a system of linear inequalities

C(P,po,p)

in such a way that p E

R ( P ,

po) iff

L ( P ,

po, p ) has an integer solution. Further- more,

C ( P ,

po, p) remains linear even ifpo and p are re- placed by variables. (The reader is referred to Lemma 4.3 in

(81

f o r a detailed description of the system of linear in- equalities associated with

C(P,

p o , p).)

Proof: (Sketch) The semilinearity of the reachability set for conflict-free PNs was originally illustrated in [9]. Sub- sequently, it has been shown in [8] that, given a conflict- free PN

P

=

( P I

T I

cp), reachability can be characterized as a system of linear inequalities

I L P ( P )

over variables q ,

...,

W J P J , U :

, ...,

w;pl

,

z1

, ...,

X I T I , among others, such that the size of

I L P ( P )

is bounded by a polynomial in the size of

P ,

given two markings p and p’, p

4

p‘, for some sequence IS,

if

and only if

I L P ( P )

has an integer solution while assigning p to (211,

...,

w l p l ) and p’ to

(vi,

...,

wipl), and

for each transition

t

E

T ,

the solutiuon of variable zt in

I L P ( P )

exactly equals the number of times transition

t

fires in D .

As a result,

R E A C H ( P )

is clearly effectively semilinear.

Lemma 3.7 Given a PN

P=(P,

T ,

cp), the set

DEAD(P)

is effectively semilinear: (Here

P

can be a general Petri net (not necessarily conjict-free) for which the range of

cp

is

N.)

Proof: Let

T

=

{ t 1 , t 2 , . . . , t m } .

We define

R=

h,cp(pj,ti)

>

0 ) (For each

H

E ‘N and

ti

E

T , ti

has at least one input place in

H.) R

is clearly a finite set. We also let p~ = { p E

N k

I

Vti

E

T ,

3pj E

H I

cp(pj,

t Z )

>

p ( p j ) and Vp‘ $! H , p ( p ‘ ) = 0}, for a given H E

R.

No- tice that p~ is finite, which contains dead markings only.

If p’ is a marking such that (p’(pj) = p ( p j ) , V l

5

j

I

h ) , and (p’(p’)

2

p ( p ’ ) , V p ’ $!

H ) ,

then p’ is a dead marking as well. Hence the set of dead markings equals which is semilinear since

R

and p~ range over finite sets. {{Pl1P2,...,Ph}

c

p

I

i

F

m131

I

j

I

U H E H U @ E P H b ’

I

(P’

L

P ) A (P’(P) = P(P)IVP E

H ) } ,

I

Lemma 3.8 (From [ 1 2 ] ) For an arbitrary path p

4 F

in a conflict-free PN

P=(P,T,cp),

U can be rearranged

into

bl...(T;-.

. ’ ffd . . ’ (Td, for some sequences ( T ~ , O J ~ ,

...,

o d and integers l l , l z l

...,

l d . 1

5

d

5 IT/,

such

that

11 12

-

l d c

(7)

The above lemma allows us to rearrange an arbitrary fir- ing sequence in a conflict-free PN into a ‘canonical form’ satisfying conditions (1) and (2), in which (1) ensures that for each oi, no transition will appear more than once (hence, Ioil

5 [TI,

for all

i),

and (2) says that T r ( o 1 ) T r ( o 2 ) .

. .

T r ( a d ) forms a ‘shrinking’ sequence of sets in the sense that if a transition, say

t ,

occurs in oi, for some

i,

then

t

is guaranteed to appear in oj, V l

5

j

5 i.

Symmetrically, if

t

does not appear in oi, then it will never b e f o u n d i n a j , V i

5 j

5

d.

Lemma 3.9 If an injinite non-ss computation exists in a conjlict-free PN

P=(P,

T ,

cp) (with initial marking P O ) , then there exist markings p,p’ and a ‘short’ sequence r (i.e., # T ( t )

5

1,Vt E T ) s u c h t h a t p

4

p‘, p’

2

p, a n d p

+

is an injinite non-ss computation.

TTT...

Proof Consider an arbitrary infinite non-ss computation b from p1. Suppose we consider the suffix compu-

tation 13‘ along which all the transitions appear infinitely many times. By applying Dickson’s Lemma [2] to

8, 6

can be written as 61062 such that p1

3

p

4

p“

1

with p”

2

p, and all the transitions in (T occur infinitely of-

ten in

6.

Let

.

--

. .-

be the canonical rearrangement of (T guaranteed by Lemma 3.8. Clearly

01 must be that if p

1

p’, then p’

2

p ; otherwise, 3 p , p ” ( p )

<

p ( p ) due to Condition (2) of Lemma 3.8. (To see this, the conflict-freedom property and (2) of Lemma 3.8, together with the fact that V p E P, t E T , cp(p,

t )

5

1,

imply that no transitions will deposit tokens to a place p in any of the segments 0 1 ,

...,

od if $(I))

<

p ( p ) . ) Finally, since all the transitions in o1 occur infinitely often in the infinite non-ss computation, we claim that p

uluql”‘

constitutes an infinite non-ss computation. Suppose, in con- trast, that for some n, p p n and p n E

R ( P ,

P O ) . Let ‘ i ~ = 0 1 . . . o1. Let 63 be a prefix of 062 such that

# = ( t )

5

#,5,(t),Vt E T (i.e., all the transitions of ‘ i ~ oc-

cur in 63). Assume that p

3 fi,

for some

fi

61 R(P,po)

. Due to the conflict-freedom property of

P ,

p

4,

p

3 ,

and

( # = ( t )

5

#b3 ( t ) , V t E

T )

imply the existence of a 6 4 such that 7r64 is a permutation of 63, and p

J

p n rfq

fi

(see [9]),

contradicting the assumption that

fi R ( P ,

PO). By letting T = o l , our result follows.

11 12 l d

-

+

n

-

We are now in a position to show the ss problem to be decidable.

Theorem 3.10 The ss problem for conjlict-free PNs is de- cidable.

Proof Again, the proof is done through the use of Theorem 3.1. The semilinearity of

REACH(P)

and

DEAD(P)

follows from Lemmas 3.6 and 3.7, respectively. T being finite clearly implies the semilinearity of

S V C C ( P ) .

As a consequence, Condition (1) of Theorem 3.1 holds. Finally, Condition

(2)

of Theorem 3.1 follows immediately from Lemma 3.9. This completes the proof of the theorem.

I

4 Fair self-stabilization

Given a PN

P

with initial marking po, an infinite computation p1

3

1.12

4

. .

.

pi

3

pi+l

. . .

is said to be fair

if for every transition

t ,

if

t

is enabled at infinitely many pi,

( I 2

l), then there exist infinitely many jl (1

2

1) such that t j , =

t .

(In words, if a transition is enabled infinitely many times, then the transition must occur infinitely often as well.) A computation o from marking p1 is said to be fair non-selj-stabilizing iff one of the following holds:

(1) (T (p1

+

p2 -+

. . .

+

p m , for some

m)

is finite such

that p m is a ‘dead’ marking (i.e., p m has no immediate successor in

P )

and p m

61 R ( P ,

PO),

or

(2) o (p1

+

p2

+

...

+

pi

--+

..e) is infinite and fair

such that V i

2

1, pi

#

R ( P ,

P O ) .

We let

F S S ( P ,

po) = { p

1

none of the computations emanating from p is fair non-self-stabilizing}. The fair self- stabilization problem is that of deciding whether starting from an arbitrary marking p , none of its computations is fair non-self-stabilizing, i.e.,

F S S ( P ,

po) =

N k .

Given a set of markings

S ,

the successor (resp., prede- cessor) of

S ,

written as s u c c ( S ) (resp., pred(S)), is the set { p

I

3t E ~ , p / E s,p’

f

p } (resp., { p

I

3t E

T , p’ E

S ,

p

f

p ’ } ) . Let pred* (resp., s u c c * ) be the reflexive and transitive closure of p r e d (resp., succ). (That is, s u c c * ( S ) = { p

I

3p’ E S,p’ p } , a n d p r e d * ( S ) = { p

I

3p’ E

S ,

p

i

p ’ } . ) The sets s u c c * ( S ) and

**pred*(S)**

will be referred to as the forward reachability set and the backward reachability set of

S ,

respectively. Notice that

R ( P ,

po) = succ* ({ p o } ) . A set of markings

S

is said to be forward-closed if V p E

S ,

V t E

T ,

p

f

p‘ implies

,U‘

E

S .

Given a PN

P

=(P, T, cp), a potential function

f

is a mapping N k -+ N U {CO}, i.e.,

f

maps each marking p to a number in

N

U {CO}. (The value of f ( p ) is called the

potential of marking p.) A potential function

f

is said to be monotone if for every marking p, if p

f

p‘ (for some marking p’ and transition

t ) ,

then f ( p )

2

f ( p ’ ) .

Given a conflict-free PN

P=(P,

T ,

cp) and a set of markings

s,

the following potential function

f

will be used throughout the rest of this paper: f(p) is defined to be the

(8)

length of the shortest path from p to a marking in S; if p cannot reach

S ,

f(p) is 00. Notice that V p E

S,

f ( p ) = 0

(i.e., S defines the set of markings of zero potential). What follows is another way to view such a potential function. We partition N k into a sequence

o f

disjoint sets of markings Uo, U1,

...,

U ,

such that

U0 =

s

U1 =

(pred(U0))

- U0

...

Vi

= (pred(Ui-1)) - (Uj=o, ,..,i-iuj),i

L

1

U ,

= N k - (Uj>OUj)

It is not hard to see that f(p) =

i

iff p E Vi.

Lemma4.1 Given a conjlict-free PN

P

and a forward- closed set

s,

let f be the potential function based upon the shortest path criterion dejined above. The following hold:

( I ) f is always monotone.

( 2 ) For an arbitrary p and a path p

+

p1, $ p

4

p’ (p’ E

S )

is one of the shortest paths reaching

S

and T r ( 6 )

n

T T ( ( T )

#

0,

then f ( p i )

<

f(p).

6

Proof

p1 implies f ( p )

>_

f ( p 1 ) . Consider the following cases:

We first consider (1). It suffices to show that p

4

(a) ( f ( p ) = CO:) In this case, f ( p 1 ) = CO; otherwise,

p

4,

p1

4

p f ’ , p” E S , violating the assumption that

f ( P ) = 03.

(b) (0

<

f(p)

<

CO:) Let p

4

p’(p‘ E

S )

be one of the shortest paths reaching S . Consider two cases:

(i)

t $

T T ( ( T ) . Since the PN is conflict-free,

t

is enabled at p’. Suppose p’

3

p”, for some p” E

S (since

S is

forward-closed). Clearly, p1

4

p”,

(ii)

t

E ~ r ( a ) . Suppose p

3

p2

f

p3

3

p’ (for some p2, p3), where (T = alto2 and

t

is not in 0 1 . Again due to the conflict-freedom property of the PN, p1

3

p3

3

p ’ ; hence, f(p1)

5

yielding f(P1)

5 fb).

f ( P ) - 1.

Figure 3 illustrates the monotone property of the potential function for paths in a conflict-free PN.

Now consider (2). Let (T = 0 1 t 0 2 , where

t

is the first occurrence of a transition that is also in 6. Suppose

6

= 61t&

(t

$ &), and p

4

p2

f

p3

9

pl. (Notice that the selection o f t ensures that Tr(61)

n

T r ( u ) =

0.)

It is not hard to see that ( T I is enabled at pug, since Tr(a1)

n

6

shoi

Figure 3. Paths and the associated potentials.

T r ( 6 l t ) =

0

and PN

P

is conflict-free. We immediately have p3

“q2

p4, for some p4 E S (since p’

3

p4 and

S

is forward-closed). Hence, f ( p 3 )

5

Iu1ugI = f ( p )

-

1. See Figures 3 and

4.

Using the result of (l), (2) follows.

_I

Figure 4. Proof of Lemma 4.1.

Theorem 4.2 Given a conjlict-free PN

P=(P, T ,

9) and an initial marking po, p E

FSS(P,.po)

i f f p E

pred(R(P,*

Po)).

Proof: Let S be

R ( P , p o ) ,

which is clearly forward- closed. We let the potentials

o f

those markings in

S

be zero. If p

$ pred(S),*

none of the (finite or infinite) computations can reach

R ( S ) ;

hence p

$ F S S ( S ) .

Suppose p E pred*(S). If p has a fair (infinite) path which never reaches

S ,

then there must exist a marking p1

and sequences 01 and ( ~ 2 such that p

3

p1

3,

f ( p )

2

f ( p 1 )

>

0 and 1-11

3

is fair along which the potential never drops. Let p1

tit%'ti

p’(,d E

S )

be one of the shortest paths reaching some marking in

S .

The fairness assumption

(9)

ensures that

tl E

Tr(02); otherwise, tl would have been enabled infinitely often without being fired. By Lemma 4.1, the potential along 02 eventually drops - a contradiction. As a consequence, from p all infinite computations avoiding

S

are unfair. Using a similar argument, we can show that if p p’ and p’ is a dead marking, then p’ E S.

I

According to Lemma 3.6, checking reachability for conflict-free PNs can be equated with solving the integer linear programming problem, which is known to be in NP. It is important to point out that, as po and p in Lemma 3.6 can be regarded as variables, the backward reachability set

**pred*(R(P,po)**

is readily expressible in terms of integer linear programming. Hence, the following is obvious. Corollary 4.3 The fair self-stabilization problem f o r

conflict-free Petri nets is decidable.

5 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 infinite-state systems including one-

counter machines and conflict-free Petri nets. The key be- hind 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. We have also studied the fair version of self-stabilization, and a decidability result was shown for the class of conflict-free Petri nets.

Another issue that deserves further investigation is to consider the problem with respect to the notion of ‘self- stabilization with probability one.’ In spite of having some non-self-stabilizing computations, in practice a sys-

tem

might be considered ‘fault-tolerant’ if the probability of self-stabilization equals one. 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, 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). How- ever, 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.

References

[ l ] Cherkasova, L., Howell, R. and Rosier, L. Bounded self-stabilizing Petri nets, Acta Infornzat., 32: 189-207,

1995.

[2] Dickson, L., Finiteness of the odd perfect and prim- itive abundant numbers with n distinct prime factors,

Amel: J. Math., 35:413-422, 1913.

[3] Dijkstra, E. Self-stabilizing systems in spite of dis- tributed control, C. ACM, 17, pp. 643-644, 1974.

[4] Ginsburg, S . , The mathematical theory of context-free

languages, McGraw-Hill, 1966.

[5] Gouda, M., Howell, R. and Rosier, L. The instability of self-stabilization, Acta Informat., 27, pp. 697-724,

1990.

[6] Herman, T., A comprehensive bibliography on self-stabilization, Chicago Jour- nal of Theoretical Computer Science,

(http://www.cs.uiowa.edu/ftp/selfstab/bibliography), 1998.

[7] Hopcroft, J. and Pansiot, J., On the reachability prob- lem for 5-dimensional vector addition systems, Theo-

ret. Compur. Sci., 8(2):135-159, 1979.

[8] Howell, R. and Rosier, L. and H. Yen, Normal and sinkless Petri nets, Journal of Computer and System

Sciences, 46: 1-26, 1993.

[9] Landweber, L. and Robertson, E., Properties of conflict-free and persistent Petri nets, J. Assoc. Com- put. Mach., 25:352-364, 1978.

[ 101 Presburger, M., Uber die vollstandigkeit eines gewis- sen systems der arithmetik

...,

Comptes rendues du premier Congres des Math. des Pays Slaves, Warsaw, 92-101,395, 1929.

[ 111 Rosier, L. and Yen, H., Logspace hierarchies, polynomial time and the complexity of fairness prob- lems concerning w-machines.

SIAM J.

Computing,

16(5):779-807, 1987.

[ 121 Yen, H., Wang, B. and Yang, M., Deciding a class of path formulas for conflict-free Petri nets, Theory of