Dependability analysis of a class of probabilistic Petri nets

Dependability Analysis of a Class of Probabilistic Petri Nets

H

-C

Y

L

-P

Y

Dept. of Electrical Eng., National Taiwan University

Taipei, Taiwan 106, R.O.C.

E-mail: [email protected]

Fax: +886-2-2363 8247

Phone: + 886-2-2363 5251 ext. 540

Abstract

Verification of various properties associated with concurrent/distributed systems is critical in the process of designing and analyzing dependable systems. While techniques for the automatic verification of finite-state

systems are relatively well studied, one of the main

challenges in the domain of verification is concerned with the development of new techniques capable of cop-ing with problems beyond the finite state framework. In this paper, we investigate a number of problems closely related to dependability analysis in the context of prob-abilistic infinite-state systems modelled by probprob-abilistic

conflict-free Petri nets. Using a valuation method, we

are able to demonstrate effective procedures for solving the termination with probability 1, the self-stabilization

with probability 1, and the controllability with proba-bility 1 problems in a unified framework.

Keywords: Controllability, probabilistic Petri net,

reachability, self-stabilization, verification.

1. Introduction

As modern hardware and software systems are be-coming more complex and at the same time required to be more dependable, there is an ever-increasing need for new evaluation techniques; the advantage of an-alytical evaluation over experimental one lies in its usefulness in abstracting the essentials of systems (so that various levels of system details can be abstracted out) and analyzing or predicting system behaviors (es-pecially while a system is being designed or imple-mented), and its being generally far more cost effec-tive than its experiment-based counterpart. With the in-creasing interest in developing dependable systems, the ∗ Corresponding author

study of problems regarding termination,

controllabil-ity, and self-stabilization, among others, has also been

gaining increasing popularity in the computer science community due to the following reasons. Dependable systems are often associated with properties like safety (‘something bad never happens’), liveness (‘something good eventually happens’), fault-tolerance (error detec-tion, recovery and masking), etc. The safety property requires that undesired or failure states be avoided at all times during the course of a computation. The live-ness property asserts that a certain desired condition be true eventually. The notion of self-stabilization was in-troduced by Dijkstra [2] to describe a system having the behavior that regardless of its starting configuration, the computation is guaranteed to return to a legitimate

con-figuration eventually. By a legitimate concon-figuration we

mean a configuration reachable from its initial config-uration. Since a self-stabilizing system has the ability to ‘correct’ itself even in the presence of certain unpre-dictable errors leading itself to an illegitimate configu-ration, one can assert that a self-stabilizing system is, in a sense, fault-tolerant.

In view of the above, it becomes apparent that auto-matic verification of various properties associated with concurrent/distributed systems is critical in the process of designing and analyzing dependable systems. While techniques for the automatic verification of finite-state

systems are relatively well studied; see, for example,

Clarke, Grumberg and Long [1], one of the main chal-lenges in the domain of verification is concerned with the development of new techniques capable of coping with problems beyond the finite state framework.

The aim of this paper focuses on investigating the following problem. Given an infinite-state system, de-termine whether the system meets certain criteria (termination, controllability, and self-stabilization) fre-quently required in dependable computing environ-ments. Taking into consideration that many real-world

Producer m 00 00 11 11 00 00 11 11 00 00 11 11 p s r c Consumer p m m 1 s1 Producer 1

Figure 1. A conflict-free Petri net mod-elling a system of m producers and one consumer.

systems are nondeterministic (or stochastic, to be more precise) in nature, the system model under our inves-tigation is not only infinite-state but also

probabilis-tic, allowing us to ask questions such as ‘something

happens with probability 1’, for instance. The sys-tems under investigation are modelled as Petri nets, which have been regarded as one of the most success-ful models for describing the behaviors of systems of concurrent nature [9]. In spite of their popular-ity, the high expressive power of Petri nets renders most of the nontrivial problems for this model highly in-tractable or even unsolvable. As a result, it is of interest from the theoretical and practical viewpoints to inves-tigate problems with respect to restricted (either struc-turally or behaviorally) versions of Petri nets, in hope of making simpler solutions feasible and well as gain-ing more insights into the factors that make general Petri nets difficult to analyze.

A Petri net is conflict-free if every place which is an input of more than one transition is on a self-loop with each such transition [6]; therefore, once a transition be-comes enabled, the only way to disable it is to fire the transition itself. Figure 1 is a conflict-free Petri net mod-elling the m-producer-1-consumer problem.

Probabilistic techniques, capable of modelling unre-liable or unpredictable behaviors of systems, are exten-sively used in the analysis of the performance and de-pendability of hardware and software systems, see, for example, Marsan, Balbo, etc. [8]. In this paper, we con-sider a probabilistic version of conflict-free Petri nets, in which each marking (i.e., configuration) is associated with a transition probability function characterizing the firing of each enabled transition. We investigate through a technique recently developed in [11] (called the

val-uation method) a number of important

dependability-related problems, including termination with

probabil-ity 1, self-stabilization with probabilprobabil-ity 1, and controlla-bility with probacontrolla-bility 1, etc. The idea of the

valuation-based approach for Petri nets is to associate a valuation in{0, 1, 2, ...∞} with each marking, and if the set of markings of zero valuation is forward-closed, then the valuation along any computation is non-increasing, and in many cases, has the tendency to move towards the ground level (i.e., valuation zero) of which the marking sometimes constitute the set of states of interest, e.g., the termination set.

The main contribution of this paper lies in the devel-opment of a unified approach (extending of the work of [11]) for reasoning about various dependability-related problems for probabilistic conflict-free Petri nets. In addition to the results themselves, we feel that the valuation-based approach for the analysis of probabilis-tic conflict-free Petri net is also interesting in its own right, and may have other applications to the analysis of other probabilistic Petri net models. The remainder of this paper is organized as follows. In Section 2, we de-fine the probabilistic version of Petri nets on which the type of systems under consideration is based. The nota-tions and defininota-tions used throughout this paper as well as the dependability-related problems under investiga-tion are also explained in this secinvestiga-tion. In Secinvestiga-tion 3, we develop the basic theory behind the valuation-based ap-proach for probabilistic conflict-free Petri nets to solve those problems defined in Section 2 in a unified frame-work. Finally, a conclusion and directions for future re-search are given in Section 4.

2. Preliminaries

2.1. Definitions and notations

Let N denote the set of nonnegative integers, and Nk the set of vectors ofk nonnegative integers. 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}.

In this paper,k is reserved for |P| (the number of places

in P). A marking is a mappingµ : P → N. (µ assigns tokens to each place of the net.) Pictorially, Petri net

is a directed, bipartite graph consisting of two kinds of nodes: places (represented by circles within which each small black dot denotes a token) and transitions (repre-sented by bars or boxes), where each arc is either from a place to a transition or vice versa. See Figure 1.

A transitiont ∈ T is enabled at a marking µ iff for

everyp ∈ P, ϕ(p, t) ≤ µ(p). In a PN (P,T,ϕ), a

transi-tiont may fire at a marking µ if t is enabled at µ; we then

all p∈ P. (We also write µ → µ
to denote the reach-ability ofµ
fromµ in one step.) A sequence of

transi-tionsσ = t1...tnis a firing sequence fromµ0in a PN iffµ0−→ µt1 1 −→ · · ·t2 −→ µtn n, for some sequence of

markingsµ1,...,µn; we also writeµ0−→ µσ n. In a PN,

we writeµ0 −→ to denote that σ is enabled and canσ be fired fromµ0, i.e.,µ0−→ iff there exists a markingσ µ such that µ0 −→ µ. An infinite sequence σ is a fir-σ ing sequence fromµ, written as µ−→, iff for every fi-σ

nite prefixσ
ofσ, µ−→. We write µσ
−→ µ∗
to denote the existence of a firing sequenceσ such that µ−→ µσ
. The reachability set of a PNP with respect to ini-tial markingµ0is the setR(P, µ0) = {µ | µ0−→ µ forσ someσ ∈ T∗}. Given a set of markings S, the succes-sor (resp., predecessucces-sor) ofS, written as succ(S) (resp., pred(S)), is the set {µ | ∃t ∈ T, µ
∈ S, µ
−→t µ} (resp., {µ | ∃t ∈ T, µ
∈ S, µ −→ µt
}). Let pred∗(resp.,succ∗) be the reflexive and transitive clo-sure ofpred (resp., succ). (That is, succ∗(S) = {µ | ∃µ
_{∈ S, µ
−→ µ}, and pred}∗ ∗_{(S) = {µ | ∃µ
∈} S, µ −→ µ∗
}.) The sets succ∗(S) and pred∗(S) will

be referred to as the forward reachability set and the

backward reachability set ofS, respectively. Notice that R(P, µ0) = succ∗({µ0}). A set of markings S is said to be forward-closed if∀µ ∈ S, ∀t ∈ T, µ−→ µt
im-pliesµ
∈ S. An infinite computation µ1−→ µt1 2−→t2 · · · µi−→ µti i+1· · · is fair if for every transition t, if t is

enabled at infinitely manyµil (l ≥ 1), then there exist

infinitely manyjl(l ≥ 1) such that tjl = t. (In words,

if a transition is enabled infinitely many times, then the transition must occur infinitely often as well.) See, e.g., [9, 10] for more about Petri nets and their related prob-lems.

Our analytical model is based on the model of

prob-abilistic Petri nets, which is defined as a 4-tuple

(P ,T ,ϕ,p), where P, T, and ϕ are the same as those

de-fined earlier, and p : M × T → [0,1] is the tran-sition probability function such that ∀µ ∈ M,

t∈Tpµ(t) = 1. (Here M denotes the set of all

mark-ings.) In words, a probabilistic Petri net associates each markingµ ∈ M with an individual transition

probabil-ity function.

Of note is thatpµ(t) is indeed a conditional

prob-ability of firing a transitiont given the system being

at markingµ (sometimes denoted by P r(t | µ) as

of-ten seen in probability textbooks); hence it may differ frompµ
(t) once µ
= µ. A path of a probabilistic Petri

netP=(P, T, ϕ, p) is a nonempty (finite or infinite) se-quenceµ1−→ µt1 2−→ · · · µt2 i −→ µti i+1· · · of

alterna-tive markings and transitions, such thatµi∈ M, ti∈ T

andpµi(ti) > 0 for all i ≥ 0. For each µ ∈ M, let Πµ

denote the set of all infinite paths starting fromµ, and Bµ ⊆ 2Πµ the smallestσ-algebra of measurable

sub-sets that contains all the cylindrical sub-sets Πµ(σ1) ≡ {σ ∈ Πµ| σ1is a prefix ofσ},

whereσ1ranging over the finite paths starting fromµ. The probability measureπ on Bµis defined so that for

each cylindrical set containing prefix σ1, say µ1 −→t1 µ2−→ · · · µt2 n−1t−→ µn−1 n, we have

π(Πµ(σ1)) = P r(σ1), where P r(σ1) =

n−1_ i=1

pµi(ti).

Those probabilities for paths following a prefix give rise to a unique probability measure onBµ.

For ease of expression, the following notations will be used throughout the rest of this paper. Letσ, σ
be transition sequences, andt be a transition.

• #σ(t) represents the number of occurrences of t in σ.

• T r(σ) = {t|t ∈ T, #σ(t) > 0}, denoting the set

of transitions used inσ.

• σ . σ
_{is defined inductively as follows. Suppose} σ
= t₁...t_n. Letσ0be σ. If ti is in σi−1, letσi

beσi−1with the leftmost occurrence of tideleted;

otherwise, letσi= σi−1. Finally, letσ. σ
= σn. For instance, ifσ = t1t2t3t4t5andσ
= t1t3t4, then σ. σ
= t2t5. Intuitively,σ. σ
represents the transition sequence resulting from removing each transition ofσ
from the leftmost occurrence of such a transition inσ (if the transition exists).

Given a computationµ0 −→ µ, a sequence σσ
is said to be a rearrangement ofσ if #σ(t) = #σ
(t), ∀t ∈ T ,

andµ0 σ

−→ µ.

2.2. Dependability-related problems

In this paper, we focus on the following dependability-related problems:

• The termination with probability 1 problem:

Given a probabilistic PN P and a set of mark-ings S (called the termination set), and let

ΠS

µ represent the set of computations

reach-ing S from marking µ, the problem is to

com-pute the set TPr=1(P, S) = {µ | the

probabil-ity of reaching S from marking µ is one, i.e., P r(ΠSµ) = 1}.

• The self-stabilization with probability 1 problem:

In spite of having some non-self-stabilizing com-putations, in practice a system might be considered

. . .

infinite non−self−satbilizing computations

’dead’ marking

X

R(P, )µ

Figure 2. Non-self-stabilizing computa-tions. (See top two paths.)

fault-tolerant if the probability of the system be-ing self-stabilized equals one. Given a probabilis-tic PNP with initial marking µ₀, a computationσ

from markingµ1is said to be non-self-stabilizing iff one of the following holds:

(1) σ (µ1→ µ2→ · · · → µm, for somem) is

fi-nite such thatµm is a ‘dead’ marking (i.e., µm has no immediate successor inP) and µm∈ R(P, µ0), or

(2) σ (µ1→ µ2→ · · · → µi → · · ·) is infinite

such that∀i ≥ 1, µi∈ R(P, µ0).

See Figure 2. Let ΠNSS_µ denote the set of

non-self-stabilizing computations with respect to R(P, µ0) from marking µ. The self-stabilization with probability 1 problem is to compute the set SSPr=1(P, µ0) = {µ | the probability of reaching

R(P, µ0) from µ is one; or P r(Πµ\ ΠNSSµ ) = 1,

i.e., P r(ΠNSSµ ) = 0}, where the difference

Πµ\ ΠSµ≡ {σ | σ ∈ Πµ, σ /∈ Πsµ}.

• The controllability with probability 1 problem: A controlled PN is simply a PN (P, T, ϕ) with its

set of transitionsT being partitioned into Tc(the set of controllable transitions) andTu(the set of uncontrollable transitions). A control policy is a

mapping Nk → 2Tc_{. (What it means is that at}

each marking, the control policy selects a subset of controllable transitions from which the next tran-sition to fire must come, unless the next trantran-sition is an uncontrollable transition.) In order to cope with the situation when the probability-embedded controllable transitions are disabled, we have to

make an assumption about the restricted behavior of the pcf-PN under control. As a general setting, e.g., [7, 5], for supervisory control of probabilis-tic systems, the supervisor will dynamically dis-able certain set of controlldis-able transitions such that the occurrence probability of disabled transitions becomes zero, whereas the occurrence probability of the remaining enabled transitions, inclusive of uncontrollable transitions, is increased in propor-tion to their probability in the uncontrolled system. The same assumption is considered herein about probabilistic PNs in that the occurrence probabil-ity of the transitiont enabled by control policy h

at markingµ is given by

P r(t | h enables Γµ) = P r(t | t
∈ Γµ)

=
pµ(t)

t
_∈Γµpµ(t
) (1)

where Γ_µ is the set of transitions enabled under

h at marking µ. Let ΠS_µ¯(h) denote the set of the

infinite computations from markingµ that always

avoidS under the control policy h regardless of

how such computations are interleaved with tran-sitions inTu. The controllability with probability 1 problem is that of, given a controlled

probabilis-tic PN and a setS of forbidden markings,

com-puting the setCP r=1(P, S) = {µ | there exists

a control policyh under which the probability of

never reaching a marking inS from µ is one, i.e., P r(ΠSµ¯(h)) = 1}. Intuitively, CP r=1(P, S)

repre-sents the set of markings from which the computa-tion can be controlled with probability one to stay away fromS. The interested reader is referred to

[3] for more about controlled Petri nets and the re-lated issues.

3. Valuation-based Dependability Analysis

method is to devise a valuation function f : Nk → N ∪ {∞}, which maps each marking µ to a value

inN ∪ {∞}. Such a value f (µ) is called the valua-tion of the marking. Furthermore, if the set of

mark-ings of zero valuation is forward-closed, then the valua-tion along any Petri net computavalua-tion is non-increasing, and in many cases, has the tendency to move towards the ground level (i.e., valuation zero). A valuation func-tionf is said to be monotone if for every marking µ, if µ −→ µt
(for some markingµ
and transitiont), then f (µ) ≥ f (µ
). It is obvious that if f is monotone and µ−→ µσ
(whereσ ∈ T∗), thenf (µ) ≥ f (µ
).

In this paper, we mainly focus on the following subclass of probabilistic Petri nets named probabilistic

conflict-free Petri nets (pcf-PNs, for short):

1. |p•| ≤ 1, or ∀t ∈ p•,t and p are on a self-loop

(i.e.,t ∈ (p•∩ •p)),where p•={t | ϕ(p, t) > 0} (resp.,•p = {t | ϕ(t, p) > 0}) represents the set of

output (resp., input) transitions of placep, and

2. with each marking µ we associate a transition

probability distributionpµsuch thatpµ(t) > 0

rep-resents the probability of firing the enabled transi-tiont at µ, and
_t∈Tpµ(t) = 1.

As Condition 1 above indicates, a conflict-free PN re-quires every place being an input of more than one tran-sition to be in a self-loop with each such trantran-sition, hence if a transition becomes enabled, the only way to disable it is to fire itself [6] (i.e.,∀t, t
∈ T, t = t
,

µ−→ µt
andµ−→ implies µt

t−→.). In words, a pcf-

PN is a conflict-free PN extended with conditional prob-ability on the firing of each transition enabled at a given marking.

Example 1 Figure 1 illustrates a conflict-free PN

de-scribing a system consisting ofm producers and one consumer. Thei-th producer iterates a loop consisting

of a sequence of two actions, produce (denoted bypi)

followed by send (denoted by si), whereas the con-sumer iterates a loop containing the actions of receive (denoted byr) and consume (denoted by c).

Given a conflict-free PNP=(P, T, ϕ) and a set of markingsS, the following valuation function f will be

used throughout the rest of this paper:f (µ) is defined

to be the length of the shortest path fromµ to a

mark-ing inS; if µ cannot reach S, f (µ) is ∞. Notice that ∀µ ∈ S, f(µ) = 0 (i.e., S defines the set of markings

of zero valuation). What follows is another way to view such a valuation function. We partitionNk into a se-quence of disjoint sets of markingsU0, U1, ..., U∞such that

U0= S

U1= (pred(U0)) − U0 ...

Ui= (pred(Ui−1)) − (∪j=0,...,i−1Uj), i ≥ 1 U∞= Nk− (∪j≥0Uj)

It is not hard to see thatf (µ) = i iff µ ∈ Ui.

Before getting into the details of our analysis, we re-quire a lemma concerning conflict-free PNs as well as the valuation function defined above.

Lemma 1 (from Lemma 3.1 in [11]) Given a conflict-free PNP and a forward-closed set S, let f be the val-uation function based upon the shortest path criterion defined above. The following hold:

(1) f is always monotone,

(2) For an arbitrary µ and a path µ −→ µδ

, if µ −→ µσ
(µ
∈ S) is one of the short-est paths reachingS and T r(δ) ∩ T r(σ) = ∅, then f (µ

) < f(µ). What this statement says is that if δ uses some transition(s) belonging to the short-est path toS, then δ will constitute a drop in valu-ation.

Proof: For the sake of completeness, we provide a

proof sketch in the following. For (1), it suffices to show thatµ−→ µt 1impliesf (µ) ≥ f (µ1). Consider the fol-lowing cases:

(a) (f (µ) = ∞:) In this case, f (µ1) = ∞.

(b) (0 < f(µ) < ∞:) Let µ −→ µσ
be one of the shortest paths reachingS. Consider two cases:

(i) Ift ∈ T r(σ), ∃µ

such thatµ
−→ µt

and

µ

∈ S (since S is forward-closed). Clearly, µ1−→ µσ

, andf (µ1) ≤ f(µ) follows. (ii) Ift ∈ T r(σ), let µ−→ µσ1 2 −→ µt 3 −→ µσ2

for someµ2, µ3, andt is not in σ1. Due to PN being conflict-free,µ1 −→ µσ1 3 −→ µσ2
; hence,f (µ1) ≤ f(µ) − 1.

Figure 3 illustrates the monotone property of the valua-tion funcvalua-tion for paths in a conflict-free PN.

Now consider (2). Due toT r(δ) ∩ T r(σ) = ∅, there

must exist a first occurrence of transition, sayt ∈ T ,

alongδ as well as σ such that (see Figure 4)

• σ = σ1tσ2and µ −→ µσ1 1 −→ µt 2 −→ µσ2
, for someσ1,σ2∈ T∗, andµ1,µ2,and

• δ = δ1tδ2andµ−→ ¯µδ1 −→ ¯µt 1−→ µδ2

, for some

δ1,δ2∈ T∗, and¯µ, ¯µ1.

Again, due to PNP being conflict-free, it is not hard to see that ¯µ1 −→ ¯µσ1 2, for some ¯µ2, and ¯µ2 −→ ¯µσ2
for some¯µ
∈ S. Hence ¯µ1 σ−→ ¯µ1σ2
∈ S. (See Figure 4) Hence,f (¯µ1) ≤ |σ1σ2| = f(µ) − 1. Using the result of (1) and the fact that¯µ1−→ µδ2

, (2) follows.

It should be noticed that being conflict-free plays an important role in Lemma 1 as the following example in-dicates.

Example 2 Consider a non-conflict-free PNP shown

in Figure 5. (In P, t and t
are in conflict with each other.) The initial marking is(1, 0, 0, 0) (i.e., one to-ken inp1whilep2, p3, and p4are empty) and suppose

1 4 1 2 3

µ

µ

S

t

t

. . .

shortest path

σ

µ

Figure 3. Paths and the associated valua-tions.

¯µ

δ

µ

_¯µ

σ

¯µ

µ

forward closed

µ

¯

µ

t

t

σ

µ

σ

µ

σ

δ

δ

S:

δ

Figure 4. Illustration of the proof of Lemma 1.

S = {(0, 0, 0, 1)}, which is clearly forward-closed as

none of the transitions is enabled inS. From the easy

fact thatf ((1, 0, 0, 0)) = 1, (1, 0, 0, 0) −→ (0, 1, 0, 0)t

andf (0, 1, 0, 0) = 2, the monotonicity property does

not hold forP.

Now we are in a position to reason about the list of problems mentioned in Section 2 for pcf-PNs in the framework of the valuation method.

Theorem 1 Given a pcf-PN P=(P ,T ,ϕ,p), and a forward-closed termination set S, if there ex-ists no path fromµ leading to ‘dead’ marking beyond S, then µ ∈ TPr=1(P, S) iff µ ∈ pred∗(S).

p

t’

p

p

p

t

Figure 5. A non-conflict-free Petri net.

Proof: We let f (µ) = 0, ∀µ ∈ S. Clearly, if µ ∈ pred∗(S), then there exists no firing sequence σ such that µ −→ µσ
∈ S; hence µ /∈ TPr=1(P, S).

The only-if part follows. Now we show the if part, i.e.,

µ ∈ pred∗(S) =⇒ µ ∈ TPr=1(P, S). Suppose, in

con-trast, that µ ∈ pred∗(S), yet µ /∈ TPr=1(P, S);

i.e., P r(ΠS_µ) < 1 or P r(Πµ\ ΠSµ) > 0. Since no

‘dead’ markings reachable from µ beyond S,

ev-ery computation σ ∈ Πµ\ ΠSµ is infinite. According

to Lemma 1, there shall exist a markingµ1, and com-putations σ1 and σ2 such that µ −→ µσ1 1 −→,σ2 f (µ) ≥ f (µ1) > 0, and the valuation along µ1−→ re-σ2 mainsf (µ1). Let µ1 t1−→ µt2···ti
be one of the short-est paths reaching some marking inS. If t1∈ T r(σ2), then the valuation alongσ2must eventually drop below f (µ1) (Lemma 1), which is a contradiction. Now, con-sider the case for whicht1 ∈ T r(σ2). For the path of σ2, sayµ1 −→ µx1 2 −→ · · · µx2 n −→ · · ·, let Xxn ibe the random variable assuming the value of thei-th

transi-tion, namelyxi, along the path, andTµSithe set of

tran-sitions being able to transferµito markings inS when

fired. Since t1 ∈ T r(σ2), t1 would have been en-abled infinitely often without being fired along σ2. Hence, letC = maxσ∈Πµ\ΠSµ, σ=σ1σ2P r(σ1), we have

P r(Πµ\ ΠSµ) =  σ∈Πµ\ΠSµ, σ=σ1σ2 P r(σ1)P r(σ2) ≤ C ·  σ∈Πµ\ΠSµ, σ=σ1σ2 P r(σ2) = C · lim_n→∞ n  i=1 P r(Xi∈ (TµSi  {t1})) ≤ C · lim n→∞ n  i=1 P r(Xi= t1) ≤ C · 0 (as P r(Xi= t1) = 1 − Pµi(t1) < 1) = 0.

– again a contradiction. Our theorem follows.

Theorem 2 Given a pcf-PN P=(P ,T ,ϕ,p) and an initial marking µ0, µ ∈ SSPr=1(P, µ0) iff

µ ∈ pred∗(R(P, µ0)).

Proof: Clearly R(P, µ0) is forward-closed. We let the valuations of those markings in R(P, µ0) be zero. If µ ∈ pred∗(R(P, µ0)), none of the (finite or infinite) computations can reach R(P, µ0); hence µ ∈ SSPr=1(P, µ0). The only-if-part follows. Now

we prove the if-part, i.e.,µ ∈ pred∗(R(P, µ0)) =⇒ µ ∈ SSPr=1(P, µ0). Following an argument similar

to the proof of Theorem 1 withΠ_µ\ ΠS_µ being sub-stituted forΠNSS_µ , we have Pr(ΠNSS_µ )=0; or the proba-bility of reachingR(P, µ0) from µ is one. Hence µ ∈ SSPr=1(P, µ0).

Theorem 3 Given a controlled pcf-PNP=(P , T_u∪ T_c, ϕ,p) and a forward-closed set S of forbidden markings, µ ∈ CP r=1(P, S) iff µ ∈ pred∗(S).

Proof: It is obvious that ifµ ∈ pred∗(S), any

computation from µ (regardless of whether it is

con-trolled or not) never encountersS. It suffices to show

thatµ ∈ pred∗(S) =⇒ µ /∈ CP r=1(P, S); i.e., any

computation has the tendency to move towardsS with

nonzero probability, in spite of the presence of a con-trol policy. Suppose, in contrast, thatµ ∈ pred∗(S),

yetµ ∈ CP r=1(P, S); i.e., there exists a control

pol-icyh such that P r(ΠSµ¯(h)) = 1. It is clear that any σ ∈

ΠS¯

µ(h) can be decomposed into δ0σ1δ1· · · σmδmσm+1

such thatδ0, δ1, ..., δm ∈ (Tu)∗,σ1, ..., σm ∈ (Tc)∗, andσm+1is an infinite computation consisting of tran-sitions fromTc. (As transitions inTucannot be disabled by the control policy, one may view theδ0, δ1, ..., δm

segments as the steps performed by an ‘adversary’ try-ing to force the computation intoS. This explains why

the infinite suffix computationσm+1is assumed to use

transitions inTconly.) In words,σ can be decomposed

intoµ −→ µσ1 1 −→ for some marking µσ2 1, and compu-tationsσ1andσ2such thatf (µ) ≥ f (µ1) > 0, and the valuation alongµ1−→ remains f(µσ2 1). Using an argu-ment parallels to the proof of Theorem 1 withΠ_µ\ ΠS_µ being substituted forΠS_µ¯(h) and p_µi(t₁) being substi-tuted for
pµi(t1)

t∈Γµipµi(t)

(refer to equation (1)) in the derivation of occurrence probability ofσ2, the pathσ2 must eventually enterS under the control policy h – a

contradiction.

The following known result serves as a vehicle for us to compute the forward and backward reachability sets, which play a vital role in using the valuation method as our earlier theorems show.

Lemma 2 (Howell et al. [4]) Given a conflict-free PN P=(P, T, ϕ) and a marking µ0, we can construct in nondeterministic polynomial time a system of linear in-equalitiesL(P, µ₀, µ) (of size bounded by a polynomial in the size ofP) such that µ ∈ R(P, µ₀) iff L(P, µ₀, µ) has an integer solution. Furthermore,L(P, µ₀, µ) re-mains linear even if µ0 and µ are replaced by vari-ables. (The reader is referred to Lemma 4.3 in [4] for a detailed description of the system of linear inequali-ties associated withL(P, µ0, µ).)

What Lemma 2 says is that checking reachability for conflict-free PNs can be equated with solving the in-teger linear programming problem, which is known to be in NP. It is important to point out that, asµ0andµ

can be regarded as variables, the forward and backward reachability sets are readily expressible in terms of in-teger linear programming.

Theorems 1-3, in conjunction with Lemma 2, imme-diately yield the following result.

Theorem 4 Given a pcf-PN P and a forward-closed set S expressible in integer linear programming, the following sets are computable: TPr=1(P, S),

SSPr=1(P, µ0) (assuming P satisfies the

condi-tion stated in Theorem 1), andCPr=1(P, S).

4. Summary and directions for future

re-search

We have demonstrated, through a valuation-based strategy, effective procedures for solving problems as-sociated with a number of dependability-related properties such as termination with probability 1,

self-stabilization with probability 1, and controlla-bility with probacontrolla-bility 1 in a unified framework. One

direction of future research is to see whether the valuation-based strategy has applications to other sub-classes of probabilistic Petri nets. Another issue that deserves further investigation is the enhance-ment of probabilistic models and valuation methods for describing and reasoning about different dependabil-ity properties of real-time systems, as many real-world systems are of real-time nature.

References

[1] Clarke, E., Grumberg, O. and Long, D., Verifica-tion Tools for Finite-State Concurrent Systems, Lecture Notes in Computer Science 803, Springer-Verlag, 124– 175, 1994.

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

[3] Holloway, L. and Krogh, B., Controlled Petri nets: a tu-torial survey, Discrete Event Systems, Lecture Notes in

Control and Information Sciences 199, G. Cohen and J.-P. Quadrat (eds.), 158–168, Springer-Verlag, 1994. [4] Howell, R., Rosier, L. and Yen, H., Normal and sinkless

Petri nets, Journal of Computer and System Sciences 46, 1–26, 1993.

[5] Kumar, R. and Garg, V. K., Control of stochastic dis-crete event systems modeled by Probabilistic languages, IEEE Transaction on Automatic Control 46(4), 593– 606, 2001.

[6] Landweber, L. and Robertson, E., Properties of conflict-free and persistent Petri nets, JACM 25(3), 352–364, 1978.

[7] Lawford M. and Wonham, W. M., Supervisory control of probabilistic discrete event systems, Proc. 36th Mid-west Symp. Circuits Systems, 327–331, 1993.

[8] Marsan, M. A., Balbo, G., Conte, G., Donatelli, S., and Franceschinis, G., Modeling with generalized stochastic petri nets, John Wiley & Sons, 1995.

[9] Murata, T., Petri nets: properties, analysis and applica-tions, Proc. of the IEEE 77(4), 541–580, 1989. [10] Peterson, J., Petri Net Theory and the Modeling of

Sys-tems, Prentice Hall, Englewood Cliffs, NJ, 1981. [11] Yen, H. A valuation-based analysis of conflict-free Petri