Open access peer-reviewed chapter

A Forward On-The-Fly Approach in Controller Synthesis of Time Petri Nets

Written By

Parisa Heidari and Hanifa Boucheneb

Submitted: December 5th, 2011 Reviewed: April 26th, 2012 Published: August 29th, 2012

DOI: 10.5772/47744

Chapter metrics overview

1,595 Chapter Downloads

View Full Metrics

1. Introduction

Controller synthesis refers to finding a controller which is running in parallel with the system under study and preventing any violation from the given properties. Such a controller guarantees satisfaction of the desired properties; a controller makes an open-loop system to be closed-loop.

Controller synthesis can also be explained by game theory as a timed game with two players: environment and the controller. The strategy of the game determines the sequence of actions to be executed. In this context, the objective of controller synthesis is to find a strategy such that no matter what action is executed by the environment, the controller wins absolutely the game. Two main questions arise for the controller: the existence and possibility of implementation. The first question, Control Problemsays given a system Sand a propertyφ, does a controller Cexist for the system Ssuch that Crunning in parallel with Ssatisfies the property φ(S||Cφ). And the second one is the Controller Synthesis Problem; if the mentioned controller exists, is there a solution to implement it? First, a system should be modeled and then, synthesized regarding the desired property.

Among various models used to describe the behavior ofS, Timed Automata (TAin short) and Time Petri Nets (TPNin short) are the well-known. The properties studied in the TPN and TA for control purposes are classified in two main categories:

  1. Safety properties: Whatever path is traveled, for all situations, a given set of forbidden states (or bad states) are never reached.

  2. Reachability properties: Whatever path is traveled, for all situations, a state of a given set of states (good states) will eventually be reached.

Some research has been done to find algorithms to control these kinds of properties for timed models (TA and TPN), such as [10, 11, 20]. Two known methods in the literature are the backward fix pointmethod and the backward/forward on-the-flymethod. Both methods are based on computing controllable predecessors of abstract states (state zones). This computation involves some expensive operations such as computing differences between abstract states (state zones).

In this chapter, we discuss an efficient approach to check whether a safety / reachability controller in time Petri nets exists or not [13]. Our approach is a completely forward on-the-fly algorithm based on the state class graph method. Unlike approaches proposed in [10, 11, 20] based on the state zone graph method, our approach does not need to compute controllable predecessors. It consists of exploring the state class graph while extracting sequences leading to undesired states and determining subclasses to be avoided. The state class graph is a suitable choice for the forward on-the-fly exploration. Using the state class graph method, the exploration algorithm converges fast and does not need any over-approximation operation to enforce the convergence.

This chapter is organized as follows: The definition of time Petri nets and its semantics as well as the state graph method come in Section 2. In Section 3, after a short survey on the control theory, previous algorithms and related work are discussed. The algorithm proposed in this chapter is developed in Section 4. Finally, Section 5 presents the conclusion and future work.


2. Time Petri nets

2.1. Definition and behavior

A time Petri net [14] is a Petri net augmented with time intervals associated with transitions. Among the different semantics proposed for time Petri nets [18], here we focus on the classical one, called intermediate semantics in [18], in the context of mono-server and strong-semantics [7].

Formally, a TPNis a tuple (P,T,Pre,Post,M0,Is)where:

  • PT(PT=)
  • PrePost(Pre,Post:P×T,
  • M0M0:P
  • IsIs:T+×(+{}))+IsttIs(t)Is(t)Is(t)t

In a controllable time Petri net, transitions are partitioned into controllable and uncontrollable transitions, denoted TcandTu, respectively (with TcTu=andT=TcTu). For the sake of simplicity and clarification, in this manuscript the controllable transitions are depicted as white bars, while the uncontrollable ones as black bars.

ATPN, is called bounded if for every reachable markingM, there is a bound bpwhere Mbholds. In this condition pstands for the number of places inP.Let Mbe a marking and ta transition. Transition tis enabled for Miff all required tokens for firing tare present inM, i.e.,pP,M(p)Pre(p,t). In this case, the firing of tleads to the marking Mdefined by: pP,M(p)=M(p)Pre(p,t)+Post(p,t).We denote En(M)the set of transitions enabled forM:
FortEn(M), we denote CF(M,t)the set of transitions enabled in Mbut in conflict witht:
Let tEn(M)and Mthe successor marking of Mbyt, a transition tis said to be newly enabled in Miff tis not enabled in the intermediate marking (i.e.,MPre(.,t)) ort=t. We denote New(M,t)the set of transitions newly enabledM, by firing tfromM:

There are two known characterizations for the TPN state. The first one, based on clocks, associates with each transition tiof the model a clockto measure the time elapsed since tibecame enabled most recently. The TPN clock state is a couple(M,ν), where M is a marking and νis a clock valuation function,ν:En(M)+. For a clock state (M,ν)andtiEn(M), ν(ti)is the value of the clock associated with transitionti. The initial clock state is q0=(M0,ν0)whereν0(ti)=0, for alltiEn(M0). The TPN clock state evolves either by time progression or by firing transitions. When a transition tibecomes enabled, its clock is initialized to zero. The value of this clock increases synchronously with time until tiis fired or disabled by the firing of another transition. tican fire, if the value of its clock is inside its static firing intervalIs(ti). It must be fired immediately, without any additional delay, when the clock reachesIs(ti). The firing of a transition takes no time, but may lead to another marking (required tokens disappear while produced ones appear).

Let q=(M,ν)and q0=(M0,ν0)be two clock states of the TPN model, θ+andtfT. We writeqθq, also denotedq+θ, iff state qis reachable from state qafter a time progression of θtime units, i.e.:

We write qtfqiff state qis immediately reachable from state qby firing transitiontf, i.e.:tfEn(M), ν(tf)Is(tf), pP,M(p)=M(p)Pre(p,tf)+Post(p,tf), andtiEn(M), ν(ti)=0, iftiNew(M,tf), ν(ti)=ν(ti)otherwise.

The second characterization, based on intervals, defines the TPN state as a marking and a function which associates with each enabled transition the time interval in which the transition can fire [5].

The TPN state is defined as a pair(M,Id), where Mis a marking and Idis a firing interval function(Id:En(M)+×(+{})). The initial state is (M0,Id0)where M0is the initial marking andId0(t)=Is(t), fortEn(M0).

Let (M,Id)and (M,Id)be two states of the TPN model, θ+andtT. The transition relation over states is defined as follows:
  • (M,Id)θ(M,Id)(M,Id)+θ(M,Id)(M,Id)θtEn(M)θId(t),M=MtEn(M),Id(t)=[Max(Id(t)θ,0),Id(t)θ]
  • (M,Id)t(M,Id)(M,Id)(M,Id)ttEn(M),Id(t)=0pP,M(p)=M(p)Pre(p,t)+Post(p,t)tEn(M),Id(t)=Is(t)tNew(M,t),Id(t)=Id(t)

The TPN state space is the structure(Q,,q0), where q0=(M0,Id0)is the initial state of the TPN and Q={q|q0*q}(*being the reflexive and transitive closure of the relation defined above) is the set of reachable states of the model.

A runin the TPN state space(Q,,q0), of a stateqQ, is a maximal sequenceρ=q1θ1q1+θ1t1q2θ2q2+θ2t2q3..., such thatq1=q. By convention, for any stateqi, relation qi0qiholds. The sequence θ1t1θ called the timed trace ofρ. The sequence called the firing sequence (untimed trace) ofρ. A marking Mis reachable iff qQs.t. its marking isM. Runs (resp. timed / untimed traces) of the TPN are all runs (resp. timed / untimed traces) of the initial stateq0.

To use enumerative analysis techniques with time Petri nets, an extra effort is required to abstract their generally infinite state spaces. Abstraction techniques aim to construct by removing some irrelevant details, a finite contraction of the state space of the model, which preserves properties of interest. For best performances, the contraction should also be the smallest possible and computed with minor resources too (time and space). The preserved properties are usually verified using standard analysis techniques on the abstractions [16].

Several state space abstraction methods have been proposed, in the literature, for time Petri nets like the state class graph (SCG)[4], the zone based graph (ZBG)[6], and etc. These abstractions may differ mainly in the characterization of states (interval states or clock states), the agglomeration criteria of states, the representation of the agglomerated states (abstract states), the kind of properties they preserve (markings, linear or branching properties) and their size.

These abstractions are finite for all bounded time Petri nets. However, if only linear properties are of interest, abstractions based on clocks are less interesting than the interval based abstractions. Indeed, abstractions based on intervals are finite for bounded TPN with unbounded intervals, while this is not true for abstraction based on clocks. The finiteness is enforced using an approximation operation, which may involve some overhead computation.

2.2. Zone Based Graph

In the Zone Based Graph (ZBG) [6], all clock states reachable by runs supporting the same firing sequence are agglomerated in the same node and considered modulo some over-approximation operation [2.12]. This operation is used to ensure the finiteness of the ZBG for Bounded TPNs with unbounded firing intervals. An abstract state, called state zone, is defined as a pair β=(M,FZ)combining a marking Mand a formula FZwhich characterizes the clock domains of all states agglomerated in the state zone. InFZ, the clock of each enabled transition for Mis represented by a variable with the same name. The domain of FZis convex and has a unique canonical form represented by the pair(M,Z), where Zis a DBM of order |En(M){o}defined by:(x,y)(En(M){o})2, zxy=SupFZ(xy), where orepresents the value 0. State zones of the ZBG are in relaxed form.

The initial state zone is the pairβ0=(M0,FZ0), where M0is the initial marking andFZ0=ti,tjEn(M0)0ti=tjtuEn(M0)Is(tu).

As an example, consider the TPN given in [11] and reported at Figure 1, its state zone graph is reported at Figure 2 and its state zones are reported in Table 1.

In this document, we consider the state class method and study the possibility to enforce the behavior of a given TPN so that to satisfy a safety / reachability property. The idea is to construct on-the-fly the reachable state classes of the TPN while collecting progressively firing subintervals to be avoided so that to satisfy the properties of interest.

2.3. The state class graph method

In the state class graph method [4], all states reachable by the same firing sequence from the initial state are agglomerated in the same node and considered modulo the relation of equivalence defined by: Two sets of states are equivalent iff they have the same marking and the same firing domain. The firing domain of a set of states is the union of the firing domains of its states. All equivalent sets are agglomerated in the same node called a state classdefined as a pairα=(M,F), where Mis a marking and Fis a formula which characterizes the firing domain ofα. For each transition tienabled inM, there is a variablet_i, inF, representing its firing delay. Fcan be rewritten as a set of atomic constraints of the form

For economy of notation, we use operator even if .

:t_it_jc, t_icort_jc, whereti, tjare transitions, c{}and is the set of rational numbers.

Though the same domain may be expressed by different conjunctions of atomic constraints (i.e., different formulas), all equivalent formulas have a unique form, called canonical form that is usually encoded by a difference bound matrix (DBM) [3]. The canonical form of Fis encoded by the DBM D(a square matrix) of order |En(M)|+1defined by: ti,tjEn(M){t0},dij=(,SupF(t_it_j)),where t0(t0T) represents a fictitious transition whose delay is always equal to 0and SupF(t_it_j)is the largest value of t_it_jin the domain ofF. Its computation is based on the shortest path Floyd-Warshall’s algorithm and is considered as the most costly operation (cubic in the number of variables inF). The canonical form of a DBM makes easier some operations over formulas like the test of equivalence. Two formulas are equivalent iff the canonical forms of their DBMs are identical.

The initial state class isα0=(M0,F0), whereF0=tiEn(M0)Is(ti)t_iIs(ti).

Let α=(M,F)be a state class and tfa transition and succ(α,tf)the set of states defined by:

The state class αhas a successor by tf(i.e.succ(α,tf)), iff tfis enabled in Mand can be fired before any other enabled transition, i.e., the following formula is consistent

A formula F is consistent iff there is, at least, one tuple of values that satisfies, at once, all constraints of F.

:F(tiEn(M)t_fti_). In this case, the firing of tfleads to the state class α=(M,F)=succ(α,tf)computed as follows [4]:

  1. Replace in Feacht_it_f, by (t_i+t_f).

  2. Eliminate by substitution t_fand each t_iof transition conflicting with tfinM.

  3. Add constraintIs(tn)t_nIs(tn), for each transitiontnNew(M,tf).

Formally, the SCG of a TPN model is a structure(CC,,α0), where α0=(M0,F0)is the initial state class, tiT,αtiαiff α=succ(α,ti)andCC={α|α0*α}.

The SCG is finite for all bounded TPNs and preserves linear properties [5]. As an example, Figure 2 shows the state class graph of the TPN presented at Figure 1. Its state classes are reported in Table 2. For this example, state class graph and state zone based graph of the system are identical while classes and zones are different.

Figure 1.

A simple Petri net withTc={t1}

Figure 2.

The State Graph of the TPN presented atFigure 1


Table 1.

able 1.State zones of the TPN presented at Figure 2

Table 2.

able 2.The state classes of the TPN presented at Figure 2

2.4. A forward method for computing predecessors of state classes

Let α=(M,F)be a state class and ωT+a sequence of transitions firable fromα. We denote succ(α,ω)the state class reachable from αby firing successively transitions ofω. We define inductively this set as follows: succ(α,ω)=α,ifω=εandsucc(α,ω)=succ(succ(α,ω),ti),ifω=ω.ti.

During the firing of a sequence of transitions ωfromα, the same transition may be newly enabled several times. To distinguish between different enabling of the same transitionti, we denote tikfor k>0the transition ti(newly) enabled by the kthtransition of the sequence; ti0denotes the transition tienabled inM. Let ω=t1k1....tmkmT+with m>0be a sequence of transitions firable from α(i.e.,succ(α,ω)). We denote Fire(α,ω)the largest subclass αof α(i.e.,αα) s.t. ωis firable from all its states, i.e.,

Proposition 1 Fire(α,ω)is the state class(M,F)whereM=MandFcan be computed as follows

We suppose that the truth value of an empty set of constraints is always .

: LetM1=MandMf+1, forf[1,m], be the marking reached fromMby the subsequencet1k1....tfkfof
  1. Initialize Fwith the formula obtained from Fby renaming all variables t_iint_i0.

  2. Add the following constraints:

  1. Put the resulting formula in canonical form and eliminate all variables t_ijsuch thatj>0, rename all variables t_i0int_i.

Note that Fire(α,ω)(i.e., ωis firable fromα) iff ωis feasible in the underlying untimed model and the formula obtained at step 2) above is consistent.

Proof. By step 1) all variables associated with transitions of En(M)are renamed (t_iis renamed int_i0). This step allows us to distinguish between delays of transitions enabled in Mfrom those that are newly enabled by the transitions of the firing sequence.

Step 2) adds the firing constraints of transitions of the sequence (forf[1,m]). For each transition tfkfof the sequence, three blocks of constraints are added. The two first blocks mean that the delay of tfkfmust be less or equal to the delays of all transitions enabled in Mf(i.e., transitions of En(M)and those enabled by tj(New(Mj+1,tj),1j<f) that are maintained continuously enabled at least until firing tfkf). Transitions of En(M)that are maintained continuously enabled at least until firing tfkfare transitions of En(M)which are not in conflict with t1k1inM1, and,..., and not in conflict with tf1kf1inMf1. Similarly, transitions of New(Mj,tj)(with1j<f) that are maintained continuously enabled at least until firing tfkfare transitions of New(Mj+1,tj)which are not in conflict with tj+1kj+1inMj+1, and,..., and not in conflict with tf1kf1inMf1. The third block of constraints specifies the firing delays of transitions that are newly enabled bytfkf.

Step 3) isolates the largest subclass of αsuch that ωis firable from all its states.

As an example, consider the TPN depicted at Figure 1 and its state class graph shown at Figure 2. Let us show how to computeFire(α0,t10t20t31). We haveEn(M0)={t1,t2}, CF(M0,t1)={t1}, CF(M1,t2)={t2}, New(M0,t1)={t3}andNew(M1,t2)={t4}. The subclass (p1+p2,F)=Fire(α0,t10t20t31)is computed as follows:

  1. Initialize Fwith the formula obtained from 0t_142t_23by renaming all variables t_iint_i0: 0t_1042t_203

  2. Add the firing constraints of t1beforet2, t2before t3and constraints on the firing intervals of transitions enabled by these firings (i.e., t3andt4):

  1. Put the resulting formula in canonical form and eliminate all variables t_ijsuch thatj>0, rename all variables t_i0int_i:0t_122t_231t_2t_13.

The subclass Fire(α0,t10t20t31)consists of all states of α0from which the sequence t1t2t3is firable. If t1is controllable, to avoid reaching the marking p4by the sequencet1t2t3, it suffices to choose the firing interval of t1in α0outside its firing interval in Fire(α0,t10t20t31)(i.e.,]2,4]).

Note that this forward method of computing predecessors can also be adapted and applied to the clock based abstractions. For instance, using the zone based graph, the initial state zone of the TPN shown at Figure 1 isβ0=(p1+p2,0t_1=t_23). The sub-zone β0ofβ0, from which the sequence t1t2t3is firable, can be computed in a similar way as the previous procedure where delay constraints are replaced by clock constraints:

β0=(p1+p2,0t_1=t_22). To avoid reaching by the sequence t1t2t3the markingp4, it suffices to delay the firing of t1until when its clocks overpasses2, which means that its firing interval should be]2,4].

3. Related work

The theory of control was initially introduced by Ramadge and Wonham in [17]. They have formalized, in terms of formal languages, the notion of control and the existence of a controller that forces a discrete event system (DES) to behave as expected. The concept of control has been afterwards extended to various models such as timed automata [21] and time Petri nets [19], where the control specification is expressed on the model states rather than the model language. Thus, for every system modeled by a controllable language, timed automata or time Petri nets, controller synthesis is used to restrict the behavior of the system making it to satisfy the desired safety or reachability properties. The typical procedure is: a system is modeled, the desired properties are defined, then, the existence and the implementation of the appropriate controller (control problem and controller synthesis problem respectively [1]) are investigated.

Several approaches of controller synthesis have been proposed in the literature. They may differ in the model they are working on (various types of Petri nets or automata), the approach they are based on (analytical as in [22], structural as in [9], semantic as in [10, 11, 20]), and finally the property to be controlled.

In [22], the authors have considered a particular type of capacity timed Petri net, where timing constraints are associated with transitions and some places, and all transitions are controllable. This timed Petri net is used to model a cluster tool with wafer residency time constraints. The wafers and their time constraints are represented by timed places. Using analytical approaches of schedulability and the particular structure of their model (model of the cluster tool), the authors have established an algorithm for finding, if it exists, an optimal periodic schedule which respects residency time constraints of wafers. The control consists of limiting timing constraints of transitions and some places so as to respect residency time constraints of wafers.

In [8, 9], the authors have considered safe and live time Petri nets where deadlines can be associated with some transition firings. The control consists of enforcing the model to meet deadlines of transition firings. The controller has the possibility to disable any transition twhich prevents to meet the deadline of a transitiontd. A transition tis allowed to fire only if its latency (the maximum delay between firing tand the next firing oftd) is not greater than the current deadline oftd. The latencies of transitions are computed by constructing an unfolding Petri net of the underlying untimed Petri net. This approach does not need to explore the state space. However, in general, the resulting controller is not maximally permissive (i.e. meaning that the controller may disable a net behavior that does not violate the properties of interest).

In [10, 11, 20], the authors have considered timed models (TA or TPN) with two kinds of transitions (controllable and uncontrollable) and investigated the control problem for safety or reachability properties. To prevent some undesired states, the controller can act on any firable and controllable transition by delaying or forcing its firing but it cannot disable transitions. The control problem is addressed by computing the winning states of the model, i.e. states which will not lead, by an uncontrollable transition, to an undesired state. The computation of the winning states is based on the concept of controllable predecessors of states. In the literature, the set of controllable predecessors is usually denoted byπ(X), where Xis a set of states satisfying the desired property (safe/goal states). The set π(X)is defined by [11]:


Intuitively, π(X)is the set of predecessors of Xwhich will not bring the system out ofX. Figure 3 clarifies this concept. If the environment can execute an uncontrollable transition after δtime units, leading the system out of X(denoted byX¯), then the controller should be able to execute a controllable action to keep the system in Xbefore δtime units. In addition, in the context of timed models with strong semantics (a transition must be fired, without any additional delay, when the upper bound of its firing interval is reached), the controller should not be forced to execute a controllable transition leading the system out ofX.

Figure 3.

Controllable Predecessors

Let AGϕbe a safety property and X0=Sat(ϕ)the set of states which satisfy the property ϕ(safe states). The fix point of Xi+1=h(Xi)=Xiπ(Xi),i0gives the largest set of safe states whose behaviors can be controlled so as to maintain the system inside this set of states (i.e., winning states). If the largest fix point of hincludes the initial state then, it gives a controller which forces the system to stay in safe states (i.e., a winning strategy).

Similarly, the fix point method is also used for reachability properties. Let AFψbe a reachability property and X0=Sat(ψ)the set of goal states. The least fix point of Xi+1=h(Xi)=Xiπ(Xi),i0is the set of states whose behaviors can be controlled so as to reach one of the goal states (i.e., winning states) [10, 20].

In the context of a timed model, this technique is applied on a state space abstraction of the timed model. In this case, Xiis a set of abstract states. If Xiis a finite set of abstract states, then the controllable predecessors of Xiis also a finite set of abstract states. The computation of the fix point of hwill converge after a finite number of steps if the state space abstraction is finite [10, 11, 20].

Note that the state space abstractions used in [10, 11, 20] are based on clocks but the state space abstraction used in [11] is not necessarily complete. The fix point method cannot guarantee to give the safety controller when it exists, unless the state space abstraction is both sound and complete. A state space abstraction of a given model is sound and complete iff it captures all firing sequences of the model and each firing sequence in the state space abstraction reflects a firing sequence of the model. Indeed, a synthesis may fail because of some unreachable states, while for the reachable state space the safety controller exists. However, the cost of processing is increased as a sound and complete state space abstraction should be entirely calculated before applying the fix point algorithm.

Let us explain by means of an example how to compute the fix point of hfor a safety property. Consider the TPN given in [11] and reported in Figure 1. The state class graph (SCG) and the zone based graph (ZBG) of this TPN are equal, except that nodes are defined differently (state classes or state zones). The state class graph is depicted in Figure 2. Its state zones and state classes are reported in Table 1 and Table 2, respectively.

Consider the state zone graph and suppose that we are interested to force the following safety property: AGΣi=14pi=2which means that the number of tokens in the TPN is always2. The transition t1is the only controllable transition and the forbidden markings is determined byΣi=14pi2. As the state class graph shows, if t2happens before t1the right path happens which is safe and the controller has nothing to do. On the other hand, if t1happens beforet2, two state classes having forbidden markings may be reached (α4,α6).

To verify whether or not there is a controller for such a property, we compute the fix point ofXi+1=h(Xi)=Xiπ(Xi), where X0={β0,β1,β2,β3,β5}is the set of state zones which satisfy the propertynotp1+p3=0. Such a controller exists iff the initial state of the model is a winning state (i.e., belongs to the fix point ofh). The fix point is computed, in 3iterations, as follows:

  1. Iteration1:X1=X0π(X0)={β0,β1,β2,β3,β5}. In this iteration, all states of β1andβ3, which are uncontrollable predecessors of bad state classes β4and β6are eliminated:

  1. Iteration2:X2=X1π(X1)={β0,β1,β2,β3,β5}. This iteration eliminates from β1all states, which are uncontrollable predecessors of bad states ofβ3β3:

  1. Iteration3:X2=X2π(X2)={β0,β1,β2,β3,β5}. The fix point X2is then the set of winning states. Since the initial state zone belongs toX2, there is a controller for forcing the propertyAGnotp1+p3=0. To keep the model in safe states (in states ofX2), the controller must delay, inβ0, the firing of t1until its clock overpasses the value2. Doing so, the successor of β0by t1will beβ1.

This approach needs however to construct a state space abstraction before computing the set of winning states. To overcome this limitation, in [10, 20], the authors have investigated the use of on-the-fly algorithms besides the fix point to compute the winning states for timed game automata (timed automata with controllable and uncontrollable transitions). We report, in Fig 4, the on-the-fly algorithm given in [10] for the case of reachability properties and timed game automata. This algorithm uses three lists Passedcontaining all state zones explored so far, Waiting, containing the set of edges to be processed and Dependindicating, for each state zoneS, the set of edges to be reevaluated in case the set of the winning states in S(Win[S]) is updated. Using this on-the-fly method, in each step, a part of the state zone graph is constructed and an edge e=(S,a,S)of the Waitinglist is processed. If the state zone Sis not in Passedand there is, inS, some states which satisfy the desired reachability property, then these states are added to the winning states of S(Win[S]). The winning states of Swill be recomputed later (the edge eis added to the Waitinglist). If Sis inPassed, the set of the winning states of S(Win[S]) is recomputed and possibly those of its predecessors and so on. The set Win[S]is the largest subset of Swhich is included in the controllable predecessors of the winning states of all its successors.

Figure 4.

On-the-fly algorithm for timed game automata proposed in [10]

This on-the-fly algorithm, based on computing controllable predecessors, requires some expensive operations such as the difference between abstract states (state zones). The difference between two state zones is not necessarily a state zone and then may result in several state zones which need to be handled separately.

In this chapter, we propose another on-the-fly approach which does not need this expensive operation. Our approach differs from the previous ones by the fact it computes bad states (i.e.: states which may lead to an undesired state) instead of computing the winning states and it constructs a state class graph instead of a state zone graph. In addition, the bad states are computed, using a forward approach, for only state classes containing at least a controllable transition.


4. An on-the-fly algorithm for investigating the existence of a controller for a TPN

This chapter aims to propose an efficient forward on-the-fly method based on the state class graph for checking the existence of a safety/reachability controller for a TPN. As discussed earlier, the state class graph is a good alternative for the on-the-fly algorithms as the exploration converges fast and does not need any over-approximation operation to enforce the convergence. The method, proposed here, is completely a forward and does not compute controllable predecessors (which is considered as an expensive operation). To explain the method, we start with safety properties.

Let us introduce informally the principle of our approach by means of the previous example. Consider the TPN shown in Figure 1, its state class graph depicted in Figure 2 and its state classes reported in Table 2. Our goal is to avoid to reach bad states (i.e., state classes α4andα6) by choosing appropriately the firing intervals for controllable transitions.

From the initial state classα0, there are two elementary paths α0t1α1t3α4and α0t1α1t2α3t3α6that lead to bad states. In both paths, there is only one state class (α0) where the controllable transition t1is firable. To avoid these bad paths, we propose to compute all states of α0from which t1t3or t1t2t3is firable, i.e., B(α0)=Fire(α0,t1t3)Fire(α0,t1t2t3), where:


To avoid these bad states, it suffices to replace inα0, the firing interval of t1with]2,4]. This interval is the complement of [0,2][0,1]in the firing interval of t1in α0([0,4]).

The approach we propose in the following section, is a combination of this principle with a forward on-the-fly method. 1.07

4.1. Controller for safety properties

A controller for safety properties running in parallel with the system should satisfy the property ’AGnotbad’ where ’bad’ stands for the set of states having a forbidden marking and it means that ’bad’ states will never happen. We introduce here an algorithm to re-constrain the controllable transitions and reach a safe net.

The idea is to construct, using a forward on-the-fly method, the state class graph of the TPN to determine whether controllable transitions have to be constrained, in order to avoid forbidden markings. This method computes and explores, path by path, the state class graph of a TPN looking for the sequences leading the system to any forbidden marking (bad sequences or bad paths). And using Proposition 1, we get the subclasses causing the bad states happening later through the found sequences (bad subclasses). We restrict the domain of controllable transitions in the state class where they were enabled so as to avoid its bad subclasses. The restriction of the interval of a controllable transition tof a state class αis obtained by subtracting from its interval in α(INT(α,t)), intervals of tin its bad subclasses.

Figure 5.

Path satisfying or not a safety property. Black states should be avoided.

Before describing the procedure formally, we define an auxiliary operation over intervals to be used in the algorithm. Let Iand Ibe two nonempty (real) intervals. We denote IIintervals defined by:


As an example, for I=[1,4]andI=]2,5],II=]3,9]. And also


This method is presented in the algorithms 6 and 7. The symbol Tcrefers to the set of controllable transitions and all forbidden markings of the net are saved in a set called, bad. The list Passedis used to retrieve the set of state classes processed so far, their bad sequences, and the bad intervals of controllable transitions (their domains in bad subclasses). Function mainconsists of an initialization step and a calling to the recursive functionexplore. The call explore(α0,,{α0})returns the set of bad sequences that cannot be avoided, fromα0, by restricting firing domains of controllable transitions. If this set is nonempty, it means that such a controller does not exist. Otherwise, it exists and the algorithm guarantees that for each state class αwith some bad sequences, there is a possibility to choose appropriately the firing intervals of some controllable transitions so as to avoid all bad subclasses ofα. The control of αconsists of eliminating, from the firing intervals of such controllable transitions, all parts figuring in its bad subclasses. The restriction of domains is also applied on firing delays between two controllable transitions ofα. We get inCtrl, all possibilities of controlling each state class. In case there is only one controllable transition inα, its delay with a fictitious transition whose time variable is fixed at 0is considered.

Each element of Passedis a triplet (α,Ω(α),LI(α))where α=(M,F)is a state class s.t.Mbad, Ω(α)is the set of bad sequences ofα, which cannot be avoided, independently ofα, from its successors, and LI(α)gives the intervals of controllable transitions in bad subclasses of α(bad intervals). The set LI(α)allows to retrieve the safe intervals of controllable transitions, by computing the complements, inα, of the forbidden intervals (i.e., all possibilities of controllingα,Ctrl(α)).

The function explorereceives parameters αbeing the class under process, tthe transition leading to αand Cthe set of traveled classes in the current path. It uses functions succ(α,t)and Fire(α,ω)already explained by equations (5) and (6) (in sections 2.3 and 2.4, respectively). It distinguishes 3cases:

  1. ααPassedtααααααtDep(α,t,LI)αt
  2. ααtα
  3. In other cases, the function exploreis called for each successor ofα, not already encountered in the current path (see Figure 5), to collect, inΩ, the bad sequences of its successors. Once all successors are processed, Ωis checked:

3.1. IfΩ=, it means that αdoes not lead to any bad state class or its bad sequences can be avoided later by controlling its successors, then(α,,) is added to Passedand the function returns with.

3.2. IfΩ, the function exploredetermines intervals of controllable transitions in bad subclasses, which do not cover their intervals inα. It gets such intervals, identifying states to be avoided, in LI(bad intervals). It adds (α,Ω,LI)to Passedand then verifies whether or not αis controllable independently of its predecessor state class in the current path. In such a case, there is no need to start the control before reaching αand then the empty set is returned by the function. Otherwise, it is needed to propagate the control to its predecessor byt. The set of sequences, obtained by prefixing with tsequences ofΩ, is then returned by the function.

This algorithm tries to control the system behavior starting from the last to the first state classes of bad paths. If it fails to control a state class of a path, so as to avoid all bad state classes, the algorithm tries to control its previous state classes. If it succeeds to control a state class, there is no need to control its predecessors. The aim is to limit as little as possible the behavior of the system (more permissive controller).

Figure 6.

Figure 7.

4.2. Example

To explain the procedure, we trace the algorithm on the TPN shown in Figure 1. Its SCG and its state classes are reported in Figure 2 and Table 2, respectively. For this example, we haveTc={t1}, bad={p2,p4}, Passed=andα0=(p1+p2,0t_142t_23).

Figure 8.

Applying Algorithms 6 & 7 on the TPN atFigure 1forAGnotp1+p3=0

The process starts by calling explore(α0,ε,{α0})(see Figure 6). Since α0is not in Passedand its marking is not forbidden, exploreis successively called for the successors ofα0: explore(α1,t1,{α0,α1})andexplore(α2,t2,{α0,α2}). In exploreofα1, function exploreis successively called for α3andα4. In exploreofα3, function exploreis called for the successor α6of α3byt3:explore(α6,t3,{α0,α1,α3,α6}). For the successor of α3by t4(i.e.,α0), there is no need to call exploreas it belongs to the current path. Since α6has a forbidden marking, exploreof α6returns to exploreof α3with{t3}, which, in turn, adds (α3,{t2t3},)to Passedand returns to exploreof α1with{t2t3}.

In exploreofα1, function exploreis called for α4(explore(α4,t3,{α0,α1,α4})). This call returns, to exploreofα1, with{t3}, since α4has a forbidden marking. In exploreofα1, the tuple (α1,{t2t3,t3},)is added to Passedand {t1t2t3,t1t3}is returned to exploreofα0. Then, exploreof α0callsexplore(α2,t2,{α0,α2}), which in turn callsexplore(α5,t1,{α0,α2,α5}). Since α5has only one successor (α0) and this successor belongs to the current path, the call of explorefor α5adds (α5,,)to Passedand returns to exploreof α2with, which, in turn, returns to exploreofα0.

After exploring both successors ofα0, in exploreofα0, we get in Ω={t1t2t3,t1t3}the set of bad paths ofα0. As the state class α0has a controllable transitiont1, its bad subclasses are computed: Fire(α0,t1t2t3)={(p1+p2,0t_122t_231t_2t_13)andFire(α0,t1t3)=(p1+p2,0t_112t_232t_2t_13)}. The firing interval of t1in α0([0,4]) is not covered by the union of intervals of t1in bad subclasses of α0([0,2][0,1][0,4]). Then, (α0,{t1t2t3,t1t3},{(t1,t0,{[0,2]})})is added toPassed. As t1is newly enabled, the empty set is returned to the functionmain, which concludes that a controller exists. According with the listPassed, α0needs to be controlled (Ctrl[α0]={(t1,t0,{[0,4][0,2]})}). For all others, there is nothing to do.

Note that for this example, it is possible to carry out a static controller, which is, in this case, a mapping over controllable transitions. Indeed, it suffices to replace the static interval of t1with]2,4]. Such a controller is in general less permissive than the state dependent controller. However, its implementation is static and very simple as if the model is corrected rather than controlled.

It is also possible to carry out a marking dependent controller (a mapping over markings). Such a controller can be represented by duplicatingt1, each of them being associated with an interval and conditioned to a marking (see Table 3 and Figure 7).

Figure 9.

The controlled TPN obtained for the TPN atFigure 1forAGnotp1+p3=0

MarkingConstraint to be applied ont1

Table 3.

able 3.A marking dependent controller for the TPN at Figure 1

This algorithm is able to determine whether a safety controller exists or not. If the algorithm fails to determine a controller, then the controller does not exist. This failure may have two reasons: no class having enabled controllable transitions exists in a bad path; or, calculated bad subclasses covers entire domain of controllable transitions. Note that, in a time Petri net [15] it is impossible to cancel a transition. Thus, if the entire domain of a controllable transition leads to bad states, as it cannot be canceled or delayed, the state class cannot be controlled so as to avoid bad states.

In the algorithms presented here, a state class is declared to be uncontrollable if it does not contain controllable transitions or it cannot be controlled so as to avoid all bad state classes. Note that if a state class cannot be controlled to avoid all bad classes, it can be however controlled to avoid some bad classes. To limit as little as possible the behavior of the system, the set of bad sequences of a state class αcan be partitioned in two subsets: the set of bad sequences that can be avoided from αand the set of bad sequences that cannot to be avoided fromα. The former set is avoided from αwhile the latter is let to be controlled by the predecessors ofα. The function explorein this case should return the set of bad sequences that cannot be controlled fromα. In this way, we increase the permissiveness of the controller.

The most significant advantage of this algorithm is the possibility of choosing the level of control. Three levels of control can be carried out:

1) Static controller: The control is independent of markings and states of the system. For each controllable transition, the intersection of all safe intervals is considered. Let tcbe a controllable transition whose interval needs to be restricted andSIr(tc)={Ir|(α,Ω,L)Passed,(tc,SI)Ctrl[α],IrSIIr}. The static firing interval of tcshould be replaced with any interval ofSIr(tc). Note that SIr(tc)may be empty. In this case, such a controller does not exist. Otherwise, it exists and its implementation is static as if the model is corrected rather than controlled. On the other hand, the permissiveness is sacrificed for the sake of simplicity of implementation. Albeit being simple, the controller has a high impact on performance of the system. For the previous example, such a controller exists and consists of replacing the static interval of t1with[2,4].2) Marking dependent controller: The controller is a function of marking. The intersection of all safe intervals of controllable state classes with the same marking is considered, causing loss of permissiveness. Let tcbe a controllable transition whose interval needs to be restricted andSIm(M,tc)={Im|((M,I),Ω,L)Passed,(tc,SI)Ctrl[(M,I)],ImSIIm}. For each markingM, the firing interval of each controllable transition tcenabled in Mshould be any interval ofSIm(M,tc). The set SIm(M,tc)may be empty and then such a controller does not exist. Otherwise, it exists and can be represented by duplicating some controllable transitions, each of them being associated with an interval and conditioned to a marking. Such a controller exists for the previous example and is given in Table 3 and the controlled TPN is what comes in Figure 7. 3) State dependent controller: The third level is the most permissive. A controllable transition is limited depending on the class the system is. In fact, making decision is delayed as much as possible. When the algorithm is being synthesized, different scenarios are considered. During the execution, the controller decides upon the scenario the system is (the current state class).

4.3. Controller for reachability properties

The algorithm proposed here for the safety properties, is also adaptable to reachability properties. A reachability controller running in parallel with the system should satisfy the property AFgoalmeaning that a goal state will certainly be reached, where ’goal’ is an atomic proposition specifying the goal states (Figure 8). For reachability properties, the controller should prevent all paths which terminates without reaching a goal state, or contains a loop on none goal states (Figure 8.b). Then, if we define state classes leading to such cases as bad states, a safety controller is able to control this system to satisfy the given reachability property. Thus, the algorithm proposed to safety properties is extensible to reachability properties with some minor modification and is presented in the algorithms 4.3 and 4.3. Note that, in this case, the set goalstands for the set of markings of goal states.

Figure 10.

Figure 11.

Figure 12.

Paths satisfying or not a reachability property. Black states should be avoided.


5. Conclusion

In this chapter, we have proposed a completely forward on-the-fly algorithm for synthesizing safety and reachability controllers for time Petri nets. This approach guarantees to find a controller if it exists as it explores all possible state classes in the state graph and collects paths which do not satisfy the properties (bad paths).

To limit as little as possible the behavior of the system (more permissive controller), this algorithm tries to control the system behavior starting from the last to the first state classes of bad paths. If it fails to control a state class of a path, so as to avoid all bad paths, the algorithm tries to control its previous state classes. If it succeed to control a state class, there is no need to control its predecessors. The control of a state class consists of restricting the firing intervals of controllable transitions and does not need to compute any controllable predecessor.

Computing controllable predecessors involves some expensive operations such as the difference between time domains. Three levels of control can be carried out from the algorithm: the first level being independent from marking and state is static but not permissive. Second and third levels being dependent of marking and state, respectively are more permissive. One can choose to control the system during execution (third level), modify the model and make transitions conditioned to marking (second level), or re-constraining the intervals, correct the system statically before execution(first level). Correcting the system statically before the execution can reduce the impact of controller interference and solve the problem of synchronization between the controller and system.

The algorithm proposed here is decidable for a bounded TPN because the state class graph is finite and the algorithm explores, path by path, the state class graph (the exploration of a path is abandoned as soon as a loop is detected or a bad state class is reached).

One perspective of this work is the investigation of the use of more compact abstraction (abstraction by inclusion, abstraction by convex-combination) and then, extend the devised and optimized algorithm to large scale and modular systems.


  1. 1. AltisenK.BouyerP.CachatT.CassezF.GardeyG.2005Introduction au contrôle des systèmes temps-réelJournal Européen des Systemes Automatises39(1-3):367 EOF380 EOF
  2. 2. BehrmannG.BouyerP.LarsenK.PelanekR.2006Lower and upper bounds in zone-based abstractions of timed automataInternational Journal on Software Tools for Technology Transfer8320415
  3. 3. BengtssonJ.2002Clocks, DBMs and states in timed systemsdissertation, Uppsala Universitet (Sweden).
  4. 4. BerthomieuB.DiazM.1991Modeling and verification of time dependent systems using time Petri netsIEEE Transactions on Software Engineering173259273
  5. 5. BerthomieuB.VernadatF.2003State class constructions for branching analysis of time Petri netsth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),442457
  6. 6. BouchenebH.GardeyG.RouxO. H.2009TCTL model checking of time Petri netsJournal of Logic and Computation61915091540
  7. 7. BoyerM.VernadatF.2000Language and bisimulation relations between subclasses of timed petri nets with strong timing semantic,Technical report, LAAS.
  8. 8. BuyU.DarabiH.2003Deadline-enforcing supervisory control for time Petri nets.,IMACS Multiconference on Computational Engineering in Systems Applications (CESA).
  9. 9. BuyU.DarabiH.LeheneM.VenepallyV.2005Supervisory control of time Petri nets using net unfolding297100
  10. 10. CassezF.DavidA.FleuryE.LarsenK. G.LimeD.2005Efficient on-the-fly algorithms for the analysis of timed gamesth International Conference on concurrency theory,6680
  11. 11. GardeyG.RouxO. E.RouxO. H.2006aSafety control synthesis for time Petri netsth International Workshop on Discrete Event Systems,2228
  12. 12. GardeyG.RouxO.RouxO.2006bState space computation and analysis of time petri netsTheory and Practice of Logic Programming630120
  13. 13. HeidariP.BouchenebH.2010Efficient method for checking the existence of a safety/ reachability controller for time Petri netsth International Conference on Application of Concurrency to System Design(ACSD),201210
  14. 14. MerlinP. M.1974A study of the recoverability of computing systemsPh.d. dissertation, University of California, Irvine, United States.
  15. 15. MerlinP. M.FarverD.1976Recoverability of communications protocols-implication of a theoretical study.,IEEE Trans. on Communications24910361043
  16. 16. PenczekW.PolrolaA.2004Specification and model checking of temporal properties in time Petri nets and timed automatath International conference on application and theory of Petri nets,3099of LNCS,3776
  17. 17. RamadgeP. J.WonhamW. M.1987Supervisory control of a class of discrete event processesSIAM Journal on Control and Optimization251206230
  18. 18. RouxO.H.LimeD.HaddadS.CassezF.BérardB.2005Comparison of different semantics for time Petri netsrd Automated Technology for Verification and Analysis3707of LNCS:293 EOF307 EOF
  19. 19. SathayeA. S.KroghB. H.1993Synthesis of real-time supervisors for controlled time Petri netsnd Conference on Decision and Control,1235236
  20. 20. TripakisS.1998L’Analyse Formelle des Systèmes Temporisés en Pratique, PhD thesis, Université Joseph Fourier- Grenoble 1 Sciences et Geographie.
  21. 21. Wong-ToiH.HoffmannG.1991The control of dense real-time discrete event systemsth IEEE Conference on Decision and Control Part 2 (of 3),215271528
  22. 22. WuN.ChuC.ChuF.ZhouM.2008Modeling and schedulability analysis of single-arm cluster tools with wafer residency time constraints using Petri net,8489


  • For economy of notation, we use operator even if .
  • A formula F is consistent iff there is, at least, one tuple of values that satisfies, at once, all constraints of F.
  • We suppose that the truth value of an empty set of constraints is always .

Written By

Parisa Heidari and Hanifa Boucheneb

Submitted: December 5th, 2011 Reviewed: April 26th, 2012 Published: August 29th, 2012