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

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 Problem says given a system $$\mathcal{S}$$ and a property$$\phi$$, does a controller $$C$$ exist for the system $$\mathcal{S}$$ such that $$C$$ running in parallel with $$\mathcal{S}$$ satisfies the property $$\phi$$ ($$\mathcal{S}\mathrm{<mo>|</mo><mo>|</mo>}C\models \phi$$). 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 of$$\mathcal{S}$$, Timed Automata ($$TA$$in short) and Time Petri Nets ($$TPN$$in 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 point method and the backward/forward on-the-fly method. 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 $$TPN$$ is a tuple $$\mathrm{<mo\; stretchy="false">(</mo>}P\mathrm{,}T\mathrm{,}Pre\mathrm{,}Post\mathrm{,}{M}_0\mathrm{,}Is\mathrm{<mo\; stretchy="false">)</mo>}$$ where:

• $$P$$$$T$$$$\mathrm{<mo\; stretchy="false">(</mo>}P\cap T\mathrm{<mo>=</mo>}\varnothing \mathrm{<mo\; stretchy="false">)</mo>}$$
• $$Pre$$$$Post$$$$\mathrm{<mo\; stretchy="false">(</mo>}Pre\mathrm{,}Post\mathrm{<mo>:</mo>}P\times T\to \mathbb{N}\mathrm{,}\mathbb{N}$$
• $$M_0$$$$M_0\mathrm{<mo>:</mo>}P\to \mathbb{N}$$
• $$Is$$$$Is\mathrm{<mo>:</mo>}T\to {\mathbb{Q}}^{+}\times \mathrm{<mo\; stretchy="false">(</mo>}{\mathbb{Q}}^{+}\cup \mathrm{<mo>\{</mo>}\infty \mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo><mo\; stretchy="false">)</mo>}$$$${\mathbb{Q}}^{+}$$$$Is$$$$t$$$$t$$$$\downarrow Is\mathrm{<mo\; stretchy="false">(</mo>}t\mathrm{<mo\; stretchy="false">)</mo>}$$$$\uparrow Is\mathrm{<mo\; stretchy="false">(</mo>}t\mathrm{<mo\; stretchy="false">)</mo>}$$$$Is\mathrm{<mo\; stretchy="false">(</mo>}t\mathrm{<mo\; stretchy="false">)</mo>}$$$$t$$

In a controllable time Petri net, transitions are partitioned into controllable and uncontrollable transitions, denoted $$T_c$$ and$$T_u$$, respectively (with $$T_c\cap T_u\mathrm{<mo>=</mo>}\varnothing$$ and$$T\mathrm{<mo>=</mo>}{T}_c\cup T_u$$). 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.

A$$TPN$$, is called bounded if for every reachable marking$$M$$, there is a bound $$b\in {\mathbb{N}}^p$$ where $$M\le b$$ holds. In this condition $$p$$ stands for the number of places in$$P$$.Let $$M$$ be a marking and $$t$$ a transition. Transition $$t$$ is enabled for $$M$$ iff all required tokens for firing $$t$$ are present in$$M$$, i.e.,$$\forall p\in P\mathrm{,}M\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo>}\ge Pre\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>}$$. In this case, the firing of $$t$$ leads to the marking $$M^{\prime }$$ defined by: $$\forall p\in P\mathrm{,}{M}^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}M\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo>}-Pre\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>}+Post\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>.}$$We denote $$En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}$$ the set of transitions enabled for$$M$$:

$$En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}t\in T\mathrm{<mo>|</mo>}\forall p\in P\mathrm{,}Pre\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>}\le M\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo>.}$$E1

For$$t\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}$$, we denote $$CF\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>}$$ the set of transitions enabled in $$M$$ but in conflict with$$t$$:

$$CF\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}{t}^{\prime }\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo><mo>|</mo>}{t}^{\prime }\mathrm{<mo>=</mo>}t\vee \exists p\in P\mathrm{,}M\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo><mo><</mo>}Pre\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}{t}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}+Pre\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>.}$$E2

Let $$t\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}$$ and $$M^{\prime }$$ the successor marking of $$M$$ by$$t$$, a transition $$t^{\prime }$$ is said to be newly enabled in $$M^{\prime }$$ iff $$t^{\prime }$$ is not enabled in the intermediate marking (i.e.,$$M-Pre\mathrm{<mo\; stretchy="false">(</mo>.,}t\mathrm{<mo\; stretchy="false">)</mo>}$$) or$$t^{\prime }\mathrm{<mo>=</mo>}t$$. We denote $$New\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>}$$ the set of transitions newly enabled$$M^{\prime }$$, by firing $$t$$ from$$M$$:

$$New\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{t}^{\prime }\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{<mo\; stretchy="false">)</mo><mo>|</mo>}t\mathrm{<mo>=</mo>}{t}^{\prime }\vee \exists p\in P\mathrm{,}{M}^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo>}-Post\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo><mo><</mo>}Pre\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}{t}^{\prime }\mathrm{<mo\; stretchy="false">)</mo><mo>\}</mo>.}$$E3

There are two known characterizations for the TPN state. The first one, based on clocks, associates with each transition $$t_i$$ of the model a $$clock$$ to measure the time elapsed since $$t_i$$ became enabled most recently. The TPN clock state is a couple$$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}\nu \mathrm{<mo\; stretchy="false">)</mo>}$$, where M is a marking and $$\nu$$ is a clock valuation function,$$\nu \mathrm{<mo>:</mo>}En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}\to {ℝ}^{+}$$. For a clock state $$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}\nu \mathrm{<mo\; stretchy="false">)</mo>}$$ and$$t_i\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}$$, $$\nu \mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo>}$$is the value of the clock associated with transition$$t_i$$. The initial clock state is $$q_0\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{M}_0\mathrm{,}{\nu }_0\mathrm{<mo\; stretchy="false">)</mo>}$$ where$${\nu }_0\mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>0}$$, for all$$t_i\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}_0\mathrm{<mo\; stretchy="false">)</mo>}$$. The TPN clock state evolves either by time progression or by firing transitions. When a transition $$t_i$$ becomes enabled, its clock is initialized to zero. The value of this clock increases synchronously with time until $$t_i$$ is fired or disabled by the firing of another transition. $$t_i$$can fire, if the value of its clock is inside its static firing interval$$Is\mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo>}$$. It must be fired immediately, without any additional delay, when the clock reaches$$\uparrow Is\mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo>}$$. The firing of a transition takes no time, but may lead to another marking (required tokens disappear while produced ones appear).

Let $$q\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}M\mathrm{,}\nu \mathrm{<mo\; stretchy="false">)</mo>}$$ and $$q_0\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{M}_0\mathrm{,}{\nu }_0\mathrm{<mo\; stretchy="false">)</mo>}$$ be two clock states of the TPN model, $$\theta \in {ℝ}^{+}$$and$$t_f\in T$$. We write$$q\stackrel{\theta }{\to }{q}^{\prime }$$, also denoted$$q+\theta$$, iff state $$q^{\prime }$$ is reachable from state $$q$$ after a time progression of $$\theta$$ time units, i.e.:

$$\underset{t^{\prime }\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}}{\underset{}{{\displaystyle \wedge }}}\nu \mathrm{<mo\; stretchy="false">(</mo>}t\mathrm{<mo\; stretchy="false">)</mo>}+\theta \le \uparrow Id\mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo>,}{M}^{\prime }\mathrm{<mo>=</mo>}M\mathrm{,}and\forall t_j\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>,}{\nu }^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}{t}_j\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}\nu \mathrm{<mo\; stretchy="false">(</mo>}{t}_j\mathrm{<mo\; stretchy="false">)</mo>}+\theta \mathrm{.}$$E4

We write $$q\stackrel{t_f}{\to }{q}^{\prime }$$ iff state $$q^{\prime }$$ is immediately reachable from state $$q$$ by firing transition$$t_f$$, i.e.:$$t_f\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}$$, $$\nu \mathrm{<mo\; stretchy="false">(</mo>}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}\ge \downarrow Is\mathrm{<mo\; stretchy="false">(</mo>}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}$$, $$\forall p\in P\mathrm{,}{M}^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}M\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo>}-Pre\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}+Post\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}$$, and$$\forall t_i\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$, $${\nu }^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>0}$$, if$$t_i\in New\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}$$, $${\nu }^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}\nu \mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo>}$$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$$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}Id\mathrm{<mo\; stretchy="false">)</mo>}$$, where $$M$$ is a marking and $$Id$$ is a firing interval function$$\mathrm{<mo\; stretchy="false">(</mo>}Id\mathrm{<mo>:</mo>}En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}\to {\mathbb{Q}}^{+}\times \mathrm{<mo\; stretchy="false">(</mo>}{\mathbb{Q}}^{+}\cup \mathrm{<mo>\{</mo>}\infty \mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo><mo\; stretchy="false">)</mo>}$$. The initial state is $$\mathrm{<mo\; stretchy="false">(</mo>}{M}_0\mathrm{,}I{d}_0\mathrm{<mo\; stretchy="false">)</mo>}$$ where $$M_0$$ is the initial marking and$$I{d}_0\mathrm{<mo\; stretchy="false">(</mo>}t\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}Is\mathrm{<mo\; stretchy="false">(</mo>}t\mathrm{<mo\; stretchy="false">)</mo>}$$, for$$t\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}_0\mathrm{<mo\; stretchy="false">)</mo>}$$.

Let $$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}Id\mathrm{<mo\; stretchy="false">)</mo>}$$ and $$\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}I{d}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$ be two states of the TPN model, $$\theta \in {ℝ}^{+}$$and$$t\in T$$. The transition relation $$\to$$ over states is defined as follows:

• $$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}Id\mathrm{<mo\; stretchy="false">)</mo>}\stackrel{\theta }{\to }\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}I{d}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$$$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}Id\mathrm{<mo\; stretchy="false">)</mo>}+\theta$$$$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}Id\mathrm{<mo\; stretchy="false">)</mo>}$$$$\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}I{d}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$$$\theta$$$$\underset{t^{\prime }\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}}{{{\displaystyle \wedge }}_{}}\theta \le \uparrow Id\mathrm{<mo\; stretchy="false">(</mo>}{t}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>,}{M}^{\prime }\mathrm{<mo>=</mo>}M$$$$\forall {t^{\prime }}^{\prime }\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>,}I{d}^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}{t^{\prime }}^{\prime }\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo\; stretchy="false">[</mo>}Max\mathrm{<mo\; stretchy="false">(</mo>}\downarrow Id\mathrm{<mo\; stretchy="false">(</mo>}{t^{\prime }}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}-\theta \mathrm{,0<mo\; stretchy="false">)</mo>,}\uparrow Id\mathrm{<mo\; stretchy="false">(</mo>}{t^{\prime }}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}-\theta \mathrm{<mo\; stretchy="false">]</mo>}$$
• $$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}Id\mathrm{<mo\; stretchy="false">)</mo>}\stackrel{t}{\to }\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}I{d}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$$$\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}I{d}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$$$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}Id\mathrm{<mo\; stretchy="false">)</mo>}$$$$t$$$$t\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>,}\downarrow Id\mathrm{<mo\; stretchy="false">(</mo>}t\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>0}$$$$\forall p\in P\mathrm{,}{M}^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}M\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{<mo\; stretchy="false">)</mo>}-Pre\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>}+Post\mathrm{<mo\; stretchy="false">(</mo>}p\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>}$$$$\forall t^{\prime }\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>,}I{d}^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}{t}^{\prime }\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}Is\mathrm{<mo\; stretchy="false">(</mo>}{t}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$$$t^{\prime }\in New\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>,}I{d}^{\prime }\mathrm{<mo\; stretchy="false">(</mo>}{t}^{\prime }\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}Id\mathrm{<mo\; stretchy="false">(</mo>}{t}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$

The TPN state space is the structure$$\mathrm{<mo\; stretchy="false">(</mo>}\mathcal{Q}\mathrm{,}\to \mathrm{,}{q}_0\mathrm{<mo\; stretchy="false">)</mo>}$$, where $$q_0\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{M}_0\mathrm{,}I{d}_0\mathrm{<mo\; stretchy="false">)</mo>}$$ is the initial state of the TPN and $$\mathcal{Q}\mathrm{<mo>=</mo><mo>\{</mo>}q\mathrm{<mo>|</mo>}{q}_0\stackrel{\mathrm{<mo>*</mo>}}{\to }q\mathrm{<mo>\}</mo><mo\; stretchy="false">(</mo>}\stackrel{\mathrm{<mo>*</mo>}}{\to }$$ being the reflexive and transitive closure of the relation $$\to$$ defined above) is the set of reachable states of the model.

A $$run$$ in the TPN state space$$\mathrm{<mo\; stretchy="false">(</mo>}\mathcal{Q}\mathrm{,}\to \mathrm{,}{q}_0\mathrm{<mo\; stretchy="false">)</mo>}$$, of a state$$q\in \mathcal{Q}$$, is a maximal sequence$$\rho \mathrm{<mo>=</mo>}{q}_1\stackrel{{\theta }_1}{\to }{q}_1+{\theta }_1\stackrel{t_1}{\to }{q}_2\stackrel{{\theta }_2}{\to }{q}_2+{\theta }_2\stackrel{t_2}{\to }{q}_3\mathrm{...}$$, such that$$q_1\mathrm{<mo>=</mo>}q$$. By convention, for any state$$q_i$$, relation $$q_i\stackrel{0}{\to }{q}_i$$ holds. The sequence $${\theta }_1{t}_1{\theta }_2{t}_2\mathrm{...}$$ is called the timed trace of$$\rho$$. The sequence $$t_1{t}_2\mathrm{...}$$ is called the firing sequence (untimed trace) of$$\rho$$. A marking $$M$$ is reachable iff $$\exists q\in \mathcal{Q}$$ s.t. its marking is$$M$$. Runs (resp. timed / untimed traces) of the TPN are all runs (resp. timed / untimed traces) of the initial state$$q_0$$.

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 $$\beta \mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}M\mathrm{,}FZ\mathrm{<mo\; stretchy="false">)</mo>}$$ combining a marking $$M$$ and a formula $$FZ$$ which characterizes the clock domains of all states agglomerated in the state zone. In$$FZ$$, the clock of each enabled transition for $$M$$ is represented by a variable with the same name. The domain of $$FZ$$ is convex and has a unique canonical form represented by the pair$$\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}Z\mathrm{<mo\; stretchy="false">)</mo>}$$, where $$Z$$ is a DBM of order $$\mathrm{<mo>|</mo>}En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}\cup \mathrm{<mo>\{</mo>}o\mathrm{<mo>\}</mo>}$$ defined by:$$\forall \mathrm{<mo\; stretchy="false">(</mo>}x\mathrm{,}y\mathrm{<mo\; stretchy="false">)</mo>}\in {\mathrm{<mo\; stretchy="false">(</mo>}En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}\cup \mathrm{<mo>\{</mo>}o\mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo>}}^2$$, $$z_{xy}\mathrm{<mo>=</mo>}Su{p}_{FZ}\mathrm{<mo\; stretchy="false">(</mo>}x-y\mathrm{<mo\; stretchy="false">)</mo>}$$, where $$o$$ represents the value 0. State zones of the ZBG are in relaxed form.

The initial state zone is the pair$${\beta }_0\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{M}_0\mathrm{,}F{Z}_0\mathrm{<mo\; stretchy="false">)</mo>}$$, where $$M_0$$ is the initial marking and$$F{Z}_0\mathrm{<mo>=</mo>}\underset{t_i\mathrm{,}{t}_j\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}_0\mathrm{<mo\; stretchy="false">)</mo>}}{{{\displaystyle \wedge }}_{}}0\le ti\mathrm{<mo>=</mo>}tj\le \underset{t_u\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}_0\mathrm{<mo\; stretchy="false">)</mo>}}{\uparrow }{I}_s\mathrm{<mo\; stretchy="false">(</mo>}{t}_u\mathrm{<mo\; stretchy="false">)</mo>}$$.

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 class defined as a pair$$\alpha \mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}M\mathrm{,}F\mathrm{<mo\; stretchy="false">)</mo>}$$, where $$M$$ is a marking and $$F$$ is a formula which characterizes the firing domain of$$\alpha$$. For each transition $$t_i$$ enabled in$$M$$, there is a variable$${\underset{\_}{t}}_i$$, in$$F$$, representing its firing delay. $$F$$can be rewritten as a set of atomic constraints of the form

For economy of notation, we use operator even if .

:$${\underset{\_}{t}}_i-{\underset{\_}{t}}_j\le c$$, $${\underset{\_}{t}}_i\le c$$or$$-{\underset{\_}{t}}_j\le c$$, where$$t_i$$, $$t_j$$are transitions, $$c\in \mathbb{Q}\cup \mathrm{<mo>\{</mo>}\infty \mathrm{<mo>\}</mo>}$$and $$\mathbb{Q}$$ 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 $$F$$ is encoded by the DBM $$D$$ (a square matrix) of order $$\mathrm{<mo>|</mo>}En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo><mo>|</mo>}+1$$ defined by: $$\forall t_i\mathrm{,}{t}_j\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}\cup \mathrm{<mo>\{</mo>}{t}_0\mathrm{<mo>\}</mo>,}{d}_{ij}\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}\le \mathrm{,}Su{p}_F\mathrm{<mo\; stretchy="false">(</mo>}{\underset{\_}{t}}_i-{\underset{\_}{t}}_j\mathrm{<mo\; stretchy="false">)</mo><mo\; stretchy="false">)</mo>,}$$where $$t_0$$ ($$t_0\notin T$$) represents a fictitious transition whose delay is always equal to $$0$$ and $$Su{p}_F\mathrm{<mo\; stretchy="false">(</mo>}{\underset{\_}{t}}_i-{\underset{\_}{t}}_j\mathrm{<mo\; stretchy="false">)</mo>}$$ is the largest value of $${\underset{\_}{t}}_i-{\underset{\_}{t}}_j$$ in the domain of$$F$$. 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 in$$F$$). 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$${\alpha }_0\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{M}_0\mathrm{,}{F}_0\mathrm{<mo\; stretchy="false">)</mo>}$$, where$$F_0\mathrm{<mo>=</mo>}\underset{t_i\in En\mathrm{<mo\; stretchy="false">(</mo>}{M}_0\mathrm{<mo\; stretchy="false">)</mo>}}{{{\displaystyle \wedge }}_{}}\downarrow Is\mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo>}\le {\underset{\_}{t}}_i\le \uparrow Is\mathrm{<mo\; stretchy="false">(</mo>}{t}_i\mathrm{<mo\; stretchy="false">)</mo>}$$.

Let $$\alpha \mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}M\mathrm{,}F\mathrm{<mo\; stretchy="false">)</mo>}$$ be a state class and $$t_f$$ a transition and $$succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}$$ the set of states defined by:

$$succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}{t}_f\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{q}^{\prime }\in \mathcal{Q}\mathrm{<mo>|</mo>}\exists q\in \alpha \mathrm{,}\exists \theta \in {ℝ}^{+}\text{s}\text{.t}\text{.}q\stackrel{\theta }{\to }q+\theta \stackrel{t_f}{\to }{q}^{\prime }\mathrm{<mo>\}</mo>}$$E5

The state class $$\alpha$$ has a successor by $$t_f$$ (i.e.$$succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}\ne \varnothing \mathrm{<mo\; stretchy="false">)</mo>}$$, iff $$t_f$$ is enabled in $$M$$ and 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\wedge \mathrm{<mo\; stretchy="false">(</mo>}\underset{t_i\in En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}}{{{\displaystyle \wedge }}_{}}{\underset{\_}{t}}_f\le \underset{\_}{t_i}\mathrm{<mo\; stretchy="false">)</mo>}$$. In this case, the firing of $$t_f$$ leads to the state class $${\alpha }^{\prime }\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}{F}^{\prime }\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}$$ computed as follows [4]:

2. Replace in $$F^{\prime }$$ each$${\underset{\_}{t}}_i\ne {\underset{\_}{t}}_f$$, by ($${\underset{\_}{t}}_i+{\underset{\_}{t}}_f$$).

3. Eliminate by substitution $${\underset{\_}{t}}_f$$ and each $${\underset{\_}{t}}_i$$ of transition conflicting with $$t_f$$ in$$M$$.

4. Add constraint$$\downarrow Is\mathrm{<mo\; stretchy="false">(</mo>}{t}_n\mathrm{<mo\; stretchy="false">)</mo>}\le {\underset{\_}{t}}_n\le \uparrow Is\mathrm{<mo\; stretchy="false">(</mo>}{t}_n\mathrm{<mo\; stretchy="false">)</mo>}$$, for each transition$$t_n\in New\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}$$.

Formally, the SCG of a TPN model is a structure$$\mathrm{<mo\; stretchy="false">(</mo>}\mathcal{C}\mathcal{C}\mathrm{,}\to \mathrm{,}{\alpha }_0\mathrm{<mo\; stretchy="false">)</mo>}$$, where $${\alpha }_0\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{M}_0\mathrm{,}{F}_0\mathrm{<mo\; stretchy="false">)</mo>}$$ is the initial state class, $$\forall t_i\in T\mathrm{,}\alpha \stackrel{t_i}{\to }{\alpha }^{\prime }$$iff $${\alpha }^{\prime }\mathrm{<mo>=</mo>}succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}{t}_i\mathrm{<mo\; stretchy="false">)</mo>}\ne \varnothing$$ and$$\mathcal{C}\mathcal{C}\mathrm{<mo>=</mo><mo>\{</mo>}\alpha \mathrm{<mo>|</mo>}{\alpha }_0\stackrel{\mathrm{<mo>*</mo>}}{\to }\alpha \mathrm{<mo>\}</mo>}$$.

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 with $$T_c\mathrm{<mo>=</mo><mo>\{</mo>}{t}_1\mathrm{<mo>\}</mo>}$$

Figure 2.

The State Graph of the TPN presented at Figure 1

$${\beta }_0\mathrm{<mo>:</mo>}{p}_1+p_2$$	$$0\le {\underset{\_}{t}}_1\mathrm{<mo>=</mo>}{\underset{\_}{t}}_2\le 3$$
$${\beta }_1\mathrm{<mo>:</mo>}{p}_2+p_3$$	$$0\le {\underset{\_}{t}}_2\le 3\wedge 0\le {\underset{\_}{t}}_3\le 3\wedge 0\le {\underset{\_}{t}}_2-{\underset{\_}{t}}_3\le 3$$
$${\beta }_2\mathrm{<mo>:</mo>}{p}_1+p_4$$	$$2\le {\underset{\_}{t}}_1\le 4$$
$${\beta }_3\mathrm{<mo>:</mo>}{p}_3+p_4$$	$$0\le {\underset{\_}{t}}_3\le 3\wedge 0\le {\underset{\_}{t}}_4\le 1\wedge 0\le {\underset{\_}{t}}_3-{\underset{\_}{t}}_4\le 3$$
$${\beta }_4\mathrm{<mo>:</mo>}{p}_2$$	$$2\le {\underset{\_}{t}}_2\le 3$$
$${\beta }_5\mathrm{<mo>:</mo>}{p}_3+p_4$$	$$0\le {\underset{\_}{t}}_3\mathrm{<mo>=</mo>}{\underset{\_}{t}}_4\le 2$$
$${\beta }_6\mathrm{<mo>:</mo>}{p}_4$$

Table 1.

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

$${\alpha }_0\mathrm{<mo>:</mo>}{p}_1+p_2$$	$$0\le {\underset{\_}{t}}_1\le 4\wedge 2\le {\underset{\_}{t}}_2\le 3$$
$${\alpha }_1\mathrm{<mo>:</mo>}{p}_2+p_3$$	$$0\le {\underset{\_}{t}}_2\le 3\wedge 2\le {\underset{\_}{t}}_3$$
$${\alpha }_2\mathrm{<mo>:</mo>}{p}_1+p_4$$	$$0\le {\underset{\_}{t}}_1\le 2$$
$${\alpha }_3\mathrm{<mo>:</mo>}{p}_3+p_4$$	$$0\le {\underset{\_}{t}}_3\wedge 0\le {\underset{\_}{t}}_4\le 1$$
$${\alpha }_4\mathrm{<mo>:</mo>}{p}_2$$	$$0\le {\underset{\_}{t}}_2\le 1$$
$${\alpha }_5\mathrm{<mo>:</mo>}{p}_3+p_4$$	$$2\le {\underset{\_}{t}}_3\mathrm{<mo><</mo>}\infty \wedge 0\le {\underset{\_}{t}}_4\le 1$$
$${\alpha }_6\mathrm{<mo>:</mo>}{p}_4$$

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 $$\alpha \mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}M\mathrm{,}F\mathrm{<mo\; stretchy="false">)</mo>}$$ be a state class and $$\omega \in T^{+}$$ a sequence of transitions firable from$$\alpha$$. We denote $$succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo>}$$ the state class reachable from $$\alpha$$ by firing successively transitions of$$\omega$$. We define inductively this set as follows: $$succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}\alpha \mathrm{,}\text{if}\omega \mathrm{<mo>=</mo>}\epsilon$$and$$succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}succ\mathrm{<mo\; stretchy="false">(</mo>}succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}{\omega }^{\prime }\mathrm{<mo\; stretchy="false">)</mo>,}{t}_i\mathrm{<mo\; stretchy="false">)</mo>,}\text{if}\omega \mathrm{<mo>=</mo>}{\omega }^{\prime }\mathrm{.}{t}_i$$.

During the firing of a sequence of transitions $$\omega$$ from$$\alpha$$, the same transition may be newly enabled several times. To distinguish between different enabling of the same transition$$t_i$$, we denote $$t_i^k$$ for $$k\mathrm{<mo>></mo>0}$$ the transition $$t_i$$ (newly) enabled by the $$k^{th}$$ transition of the sequence; $$t_i^0$$denotes the transition $$t_i$$ enabled in$$M$$. Let $$\omega \mathrm{<mo>=</mo>}{t}_1^{k_1}\mathrm{....}{t}_m^{k_m}\in T^{+}$$ with $$m\mathrm{<mo>></mo>0}$$ be a sequence of transitions firable from $$\alpha$$ (i.e.,$$succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo>}\ne \varnothing$$). We denote $$Fire\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo>}$$ the largest subclass $${\alpha }^{\prime }$$ of $$\alpha$$ (i.e.,$${\alpha }^{\prime }\subseteq \alpha$$) s.t. $$\omega$$is firable from all its states, i.e.,

$$Fire\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{q}_1\in \alpha \mathrm{<mo>|</mo>}\exists {\theta }_1\mathrm{,...,}{\theta }_m\mathrm{,}{q}_1\stackrel{{\theta }_1}{\to }{q}_1+{\theta }_1\stackrel{t_1^{k_1}}{\to }{q}_2\mathrm{...}{q}_m+{\theta }_m\stackrel{t_m^{k_m}}{\to }{q}_{m+1}\mathrm{<mo>\}</mo>}$$E8

Proposition 1 $$Fire\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo>}$$ is the state class $$\mathrm{<mo\; stretchy="false">(</mo>}{M}^{\prime }\mathrm{,}{F}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$ where $$M^{\prime }\mathrm{<mo>=</mo>}M$$ and $$F^{\prime }$$ can be computed as follows

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

: Let $$M_1\mathrm{<mo>=</mo>}M$$ and$$M_{f+1}$$, for$$f\in \mathrm{<mo\; stretchy="false">[</mo>1,}m\mathrm{<mo\; stretchy="false">]</mo>}$$, be the marking reached from $$M$$ by the subsequence $$t_1^{k_1}\mathrm{....}{t}_f^{k_f}$$ of$$\omega$$.

1. Initialize $$F^{\prime }$$ with the formula obtained from $$F$$ by renaming all variables $${\underset{\_}{t}}_i$$ in$${\underset{\_}{t}}_i^0$$.

2. Add the following constraints:

$$\begin{array}{l}\underset{f\in \mathrm{<mo\; stretchy="false">[</mo>1,}m\mathrm{<mo\; stretchy="false">]</mo>}}{\underset{}{{\displaystyle \wedge }}}\mathrm{<mo\; stretchy="false">(</mo>}\underset{t_i\in \mathrm{<mo\; stretchy="false">(</mo>}En\mathrm{<mo\; stretchy="false">(</mo>}{M}_1\mathrm{<mo\; stretchy="false">)</mo>}-\underset{j\in \mathrm{<mo\; stretchy="false">[</mo>1,}f\mathrm{<mo\; stretchy="false">[</mo>}}{{\displaystyle \cup }}CF\mathrm{<mo\; stretchy="false">(</mo>}{M}_j\mathrm{,}{t}_j\mathrm{<mo\; stretchy="false">)</mo><mo\; stretchy="false">)</mo>}}{\underset{}{{\displaystyle \wedge }}}{\underset{\_}{t}}_f^{k_f}-{\underset{\_}{t}}_i^0\le 0\wedge \hfill \\ \underset{j\in \mathrm{<mo\; stretchy="false">[</mo>1,}f\mathrm{<mo\; stretchy="false">[</mo>,}{t}_n\in \mathrm{<mo\; stretchy="false">(</mo>}New\mathrm{<mo\; stretchy="false">(</mo>}{M}_{j+1}\mathrm{,}{t}_j\mathrm{<mo\; stretchy="false">)</mo>}-\underset{k\in \mathrm{<mo\; stretchy="false">]</mo>}j\mathrm{,}f\mathrm{<mo\; stretchy="false">[</mo>}}{{\displaystyle \cup }}CF\mathrm{<mo\; stretchy="false">(</mo>}{M}_k\mathrm{,}{t}_k\mathrm{<mo\; stretchy="false">)</mo><mo\; stretchy="false">)</mo>}}{\underset{}{{\displaystyle \wedge }}}{\underset{\_}{t}}_f^{k_f}-{\underset{\_}{t}}_n^j\le 0\wedge \hfill \\ \underset{t_n\in New\mathrm{<mo\; stretchy="false">(</mo>}{M}_{f+1}\mathrm{,}{t}_f\mathrm{<mo\; stretchy="false">)</mo>}}{\underset{}{{\displaystyle \wedge }}}\downarrow Is\mathrm{<mo\; stretchy="false">(</mo>}{t}_n\mathrm{<mo\; stretchy="false">)</mo>}\le {\underset{\_}{t}}_n^f-{\underset{\_}{t}}_f^{k_f}\le \uparrow Is\mathrm{<mo\; stretchy="false">(</mo>}{t}_n\mathrm{<mo\; stretchy="false">)</mo><mo\; stretchy="false">)</mo>}\hfill \end{array}$$E9

1. Put the resulting formula in canonical form and eliminate all variables $${\underset{\_}{t}}_i^j$$ such that$$j\mathrm{<mo>></mo>0}$$, rename all variables $${\underset{\_}{t}}_i^0$$ in$${\underset{\_}{t}}_i$$.

Note that $$Fire\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo>}\ne \varnothing$$ (i.e., $$\omega$$is firable from$$\alpha$$) iff $$\omega$$ 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\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}$$ are renamed ($${\underset{\_}{t}}_i$$is renamed in$${\underset{\_}{t}}_i^0$$). This step allows us to distinguish between delays of transitions enabled in $$M$$ from those that are newly enabled by the transitions of the firing sequence.

Step 2) adds the firing constraints of transitions of the sequence (for$$f\in \mathrm{<mo\; stretchy="false">[</mo>1,}m\mathrm{<mo\; stretchy="false">]</mo>}$$). For each transition $$t_f^{k_f}$$ of the sequence, three blocks of constraints are added. The two first blocks mean that the delay of $$t_f^{k_f}$$ must be less or equal to the delays of all transitions enabled in $$M_f$$ (i.e., transitions of $$En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}$$ and those enabled by $$t_j$$ ($$New\mathrm{<mo\; stretchy="false">(</mo>}{M}_{j+1}\mathrm{,}{t}_j\mathrm{<mo\; stretchy="false">)</mo>,1}\le j\mathrm{<mo><</mo>}f$$) that are maintained continuously enabled at least until firing $$t_f^{k_f}$$ ). Transitions of $$En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}$$ that are maintained continuously enabled at least until firing $$t_f^{k_f}$$ are transitions of $$En\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>}$$ which are not in conflict with $$t_1^{k_1}$$ in$$M_1$$, and,..., and not in conflict with $$t_{f-1}^{k_{f-1}}$$ in$$M_{f-1}$$. Similarly, transitions of $$New\mathrm{<mo\; stretchy="false">(</mo>}{M}_j\mathrm{,}{t}_j\mathrm{<mo\; stretchy="false">)</mo>}$$ (with$$1\le j\mathrm{<mo><</mo>}f$$) that are maintained continuously enabled at least until firing $$t_f^{k_f}$$ are transitions of $$New\mathrm{<mo\; stretchy="false">(</mo>}{M}_{j+1}\mathrm{,}{t}_j\mathrm{<mo\; stretchy="false">)</mo>}$$ which are not in conflict with $$t_{j+1}^{k_{j+1}}$$ in$$M_{j+1}$$, and,..., and not in conflict with $$t_{f-1}^{k_{f-1}}$$ in$$M_{f-1}$$. The third block of constraints specifies the firing delays of transitions that are newly enabled by$$t_f^{k_f}$$.

Step 3) isolates the largest subclass of $$\alpha$$ such that $$\omega$$ 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 compute$$Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1^0{t}_2^0{t}_3^1\mathrm{<mo\; stretchy="false">)</mo>}$$. We have$$En\mathrm{<mo\; stretchy="false">(</mo>}{M}_0\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{t}_1\mathrm{,}{t}_2\mathrm{<mo>\}</mo>}$$, $$CF\mathrm{<mo\; stretchy="false">(</mo>}{M}_0\mathrm{,}{t}_1\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{t}_1\mathrm{<mo>\}</mo>}$$, $$CF\mathrm{<mo\; stretchy="false">(</mo>}{M}_1\mathrm{,}{t}_2\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{t}_2\mathrm{<mo>\}</mo>}$$, $$New\mathrm{<mo\; stretchy="false">(</mo>}{M}_0\mathrm{,}{t}_1\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{t}_3\mathrm{<mo>\}</mo>}$$and$$New\mathrm{<mo\; stretchy="false">(</mo>}{M}_1\mathrm{,}{t}_2\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{t}_4\mathrm{<mo>\}</mo>}$$. The subclass $$\mathrm{<mo\; stretchy="false">(</mo>}{p}_1+p_2\mathrm{,}{F}^{\prime }\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1^0{t}_2^0{t}_3^1\mathrm{<mo\; stretchy="false">)</mo>}$$ is computed as follows:

1. Initialize $$F^{\prime }$$ with the formula obtained from $$0\le {\underset{\_}{t}}_1\le 4\wedge 2\le {\underset{\_}{t}}_2\le 3$$ by renaming all variables $${\underset{\_}{t}}_i$$ in$${\underset{\_}{t}}_i^0$$: $$0\le {\underset{\_}{t}}_1^0\le 4\wedge 2\le {\underset{\_}{t}}_2^0\le 3$$

2. Add the firing constraints of $$t_1$$ before$$t_2$$, $$t_2$$before $$t_3$$ and constraints on the firing intervals of transitions enabled by these firings (i.e., $$t_3$$and$$t_4$$):

$${\underset{\_}{t}}_1^0-{\underset{\_}{t}}_2^0\le 0\wedge {\underset{\_}{t}}_2^0-{\underset{\_}{t}}_3^1\le 0\wedge 2\le {\underset{\_}{t}}_3^1-{\underset{\_}{t}}_1^0\wedge 0\le {\underset{\_}{t}}_4^2-{\underset{\_}{t}}_2^0\le 1$$E10

1. Put the resulting formula in canonical form and eliminate all variables $${\underset{\_}{t}}_i^j$$ such that$$j\mathrm{<mo>></mo>0}$$, rename all variables $${\underset{\_}{t}}_i^0$$ in$${\underset{\_}{t}}_i$$:$$0\le {\underset{\_}{t}}_1\le 2\wedge 2\le {\underset{\_}{t}}_2\le 3\wedge 1\le {\underset{\_}{t}}_2-{\underset{\_}{t}}_1\le 3$$.

The subclass $$Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1^0{t}_2^0{t}_3^1\mathrm{<mo\; stretchy="false">)</mo>}$$ consists of all states of $${\alpha }_0$$ from which the sequence $$t_1{t}_2{t}_3$$ is firable. If $$t_1$$ is controllable, to avoid reaching the marking $$p_4$$ by the sequence$$t_1{t}_2{t}_3$$, it suffices to choose the firing interval of $$t_1$$ in $${\alpha }_0$$ outside its firing interval in $$Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1^0{t}_2^0{t}_3^1\mathrm{<mo\; stretchy="false">)</mo>}$$ (i.e.,$$\mathrm{<mo\; stretchy="false">]</mo>2,4<mo\; stretchy="false">]</mo>}$$).

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$${\beta }_0\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{p}_1+p_2\mathrm{,0}\le {\underset{\_}{t}}_1\mathrm{<mo>=</mo>}{\underset{\_}{t}}_2\le \mathrm{3<mo\; stretchy="false">)</mo>}$$. The sub-zone $${\beta }_{0^{\prime }}$$ of$${\beta }_0$$, from which the sequence $$t_1{t}_2{t}_3$$ is firable, can be computed in a similar way as the previous procedure where delay constraints are replaced by clock constraints:

$${\beta }_{0^{\prime }}\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{p}_1+p_2\mathrm{,0}\le {\underset{\_}{t}}_1\mathrm{<mo>=</mo>}{\underset{\_}{t}}_2\le \mathrm{2<mo\; stretchy="false">)</mo>}$$. To avoid reaching by the sequence $$t_1{t}_2{t}_3$$ the marking$$p_4$$, it suffices to delay the firing of $$t_1$$ until when its clocks overpasses$$2$$, which means that its firing interval should be$$\mathrm{<mo\; stretchy="false">]</mo>2,4<mo\; stretchy="false">]</mo>}$$.

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 $$t$$ which prevents to meet the deadline of a transition$$t_d$$. A transition $$t$$ is allowed to fire only if its latency (the maximum delay between firing $$t$$ and the next firing of$$t_d$$) is not greater than the current deadline of$$t_d$$. 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$$\pi \mathrm{<mo\; stretchy="false">(</mo>}X\mathrm{<mo\; stretchy="false">)</mo>}$$, where $$X$$ is a set of states satisfying the desired property (safe/goal states). The set $$\pi \mathrm{<mo\; stretchy="false">(</mo>}X\mathrm{<mo\; stretchy="false">)</mo>}$$ is defined by [11]:

$$\begin{array}{l}\pi \mathrm{<mo\; stretchy="false">(</mo>}X\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}q\in \mathcal{Q}\mathrm{<mo>|</mo><mo\; stretchy="false">(</mo><mo\; stretchy="false">(</mo>}\exists \delta \in {ℝ}_{\ge 0}\mathrm{,}t\in T{q}^{\prime }\in Xq\stackrel{\delta }{\to }\stackrel{t}{\to }{q}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}\vee \hfill \\ \mathrm{<mo\; stretchy="false">(</mo>}\exists \delta \in {ℝ}_{\ge 0}\mathrm{,}{q}^{\prime }\in Xq\stackrel{\delta }{\to }{q}^{\prime }\mathrm{<mo\; stretchy="false">)</mo><mo\; stretchy="false">)</mo>}\wedge \hfill \\ \forall \delta \in {ℝ}_{\ge 0}if\exists t\in T\mathrm{,}{q}^{\prime }\notin Xq\stackrel{\delta }{\to }\stackrel{t}{\to }{q}^{\prime }\hfill \\ then\exists {\delta }_c\mathrm{<mo><</mo>}\delta \mathrm{,}{t}_c\in T_c\mathrm{,}{q}_c\in Xq\stackrel{{\delta }_c}{\to }\stackrel{t_c}{\to }{q}_c\mathrm{<mo>\}</mo>}\hfill \\ \hfill \end{array}$$E11

Intuitively, $$\pi \mathrm{<mo\; stretchy="false">(</mo>}X\mathrm{<mo\; stretchy="false">)</mo>}$$is the set of predecessors of $$X$$ which will not bring the system out of$$X$$. Figure 3 clarifies this concept. If the environment can execute an uncontrollable transition after $$\delta$$ time units, leading the system out of $$X$$ (denoted by$$\overline{X}$$), then the controller should be able to execute a controllable action to keep the system in $$X$$ before $$\delta$$ 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 of$$X$$.

Figure 3.

Controllable Predecessors

Let $$AG\varphi$$ be a safety property and $$X_0\mathrm{<mo>=</mo>}Sat\mathrm{<mo\; stretchy="false">(</mo>}\varphi \mathrm{<mo\; stretchy="false">)</mo>}$$ the set of states which satisfy the property $$\varphi$$ (safe states). The fix point of $$X_{i+1}\mathrm{<mo>=</mo>}h\mathrm{<mo\; stretchy="false">(</mo>}{X}_i\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}{X}_i\cap \pi \mathrm{<mo\; stretchy="false">(</mo>}{X}_i\mathrm{<mo\; stretchy="false">)</mo>,}i\ge 0$$ gives 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 $$h$$ includes 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\psi$$ be a reachability property and $$X_0\mathrm{<mo>=</mo>}Sat\mathrm{<mo\; stretchy="false">(</mo>}\psi \mathrm{<mo\; stretchy="false">)</mo>}$$ the set of goal states. The least fix point of $$X_{i+1}\mathrm{<mo>=</mo>}h\mathrm{<mo\; stretchy="false">(</mo>}{X}_i\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}{X}_i\cup \pi \mathrm{<mo\; stretchy="false">(</mo>}{X}_i\mathrm{<mo\; stretchy="false">)</mo>,}i\ge 0$$ is 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, $$X_i$$is a set of abstract states. If $$X_i$$ is a finite set of abstract states, then the controllable predecessors of $$X_i$$ is also a finite set of abstract states. The computation of the fix point of $$h$$ will 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 $$h$$ for 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{\Sigma }_{i\mathrm{<mo>=</mo>1}}^4{p}_i\mathrm{<mo>=</mo>2}$$which means that the number of tokens in the TPN is always$$2$$. The transition $$t_1$$ is the only controllable transition and the forbidden markings is determined by$${\Sigma }_{i\mathrm{<mo>=</mo>1}}^4{p}_i\ne 2$$. As the state class graph shows, if $$t_2$$ happens before $$t_1$$ the right path happens which is safe and the controller has nothing to do. On the other hand, if $$t_1$$ happens before$$t_2$$, two state classes having forbidden markings may be reached ($${\alpha }_4\mathrm{,}{\alpha }_6$$).

To verify whether or not there is a controller for such a property, we compute the fix point of$$X_{i+1}\mathrm{<mo>=</mo>}h\mathrm{<mo\; stretchy="false">(</mo>}{X}_i\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}{X}_i\cap \pi \mathrm{<mo\; stretchy="false">(</mo>}{X}_i\mathrm{<mo\; stretchy="false">)</mo>}$$, where $$X_0\mathrm{<mo>=</mo><mo>\{</mo>}{\beta }_0\mathrm{,}{\beta }_1\mathrm{,}{\beta }_2\mathrm{,}{\beta }_3\mathrm{,}{\beta }_5\mathrm{<mo>\}</mo>}$$ is the set of state zones which satisfy the property$$not{p}_1+p_3\mathrm{<mo>=</mo>0}$$. Such a controller exists iff the initial state of the model is a winning state (i.e., belongs to the fix point of$$h$$). The fix point is computed, in $$3$$ iterations, as follows:

1. Iteration$$1$$:$$X_1\mathrm{<mo>=</mo>}{X}_0\cap \pi \mathrm{<mo\; stretchy="false">(</mo>}{X}_0\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{\beta }_0\mathrm{,}{{\beta }^{\prime }}_1\mathrm{,}{\beta }_2\mathrm{,}{{\beta }^{\prime }}_3\mathrm{,}{\beta }_5\mathrm{<mo>\}</mo>}$$. In this iteration, all states of $${\beta }_1$$ and$${\beta }_3$$, which are uncontrollable predecessors of bad state classes $${\beta }_4$$ and $${\beta }_6$$ are eliminated:

$${{\beta }^{\prime }}_1\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{p}_2+p_3\mathrm{,1<mo><</mo>}{\underset{\_}{t}}_2\le 3\wedge 0\le {\underset{\_}{t}}_3\mathrm{<mo><</mo>2}\wedge \mathrm{1<mo><</mo>}{\underset{\_}{t}}_2-{\underset{\_}{t}}_3\le \mathrm{3<mo\; stretchy="false">)</mo>}$$E12

and

$${{\beta }^{\prime }}_3\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{p}_3+p_4\mathrm{,1}\le {\underset{\_}{t}}_3\mathrm{<mo><</mo>}\le 3\wedge \mathrm{0<mo><</mo>}{t}_4\le 1\wedge 1\le {\underset{\_}{t}}_3-{\underset{\_}{t}}_4\le \mathrm{3<mo\; stretchy="false">)</mo>}$$E13

.

1. Iteration$$2$$:$$X_2\mathrm{<mo>=</mo>}{X}_1\cap \pi \mathrm{<mo\; stretchy="false">(</mo>}{X}_1\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{\beta }_0\mathrm{,}{{{\beta }^{\prime }}^{\prime }}_1\mathrm{,}{\beta }_2\mathrm{,}{{\beta }^{\prime }}_3\mathrm{,}{\beta }_5\mathrm{<mo>\}</mo>}$$. This iteration eliminates from $${{\beta }^{\prime }}_1$$ all states, which are uncontrollable predecessors of bad states of$${\beta }_3-{{\beta }^{\prime }}_3$$:

$${{{\beta }^{\prime }}^{\prime }}_1\mathrm{<mo>=</mo><mo>\{</mo>}{p}_2+p_3\mathrm{,2<mo><</mo>}{\underset{\_}{t}}_2\le 3\wedge 0\le {\underset{\_}{t}}_3\mathrm{<mo><</mo>1}\wedge 2\le {\underset{\_}{t}}_2-{\underset{\_}{t}}_3\le \mathrm{3<mo>\}</mo>}$$E14

.

1. Iteration$$3$$:$$X_2\mathrm{<mo>=</mo>}{X}_2\cap \pi \mathrm{<mo\; stretchy="false">(</mo>}{X}_2\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}{\beta }_0\mathrm{,}{{{\beta }^{\prime }}^{\prime }}_1\mathrm{,}{\beta }_2\mathrm{,}{{\beta }^{\prime }}_3\mathrm{,}{\beta }_5\mathrm{<mo>\}</mo>}$$. The fix point $$X_2$$ is then the set of winning states. Since the initial state zone belongs to$$X_2$$, there is a controller for forcing the property$$AGnot{p}_1+p_3\mathrm{<mo>=</mo>0}$$. To keep the model in safe states (in states of$$X_2$$), the controller must delay, in$${\beta }_0$$, the firing of $$t_1$$ until its clock overpasses the value$$2$$. Doing so, the successor of $${\beta }_0$$ by $$t_1$$ will be$${{{\beta }^{\prime }}^{\prime }}_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 $$Passed$$ containing all state zones explored so far, $$Waiting$$, containing the set of edges to be processed and $$Depend$$ indicating, for each state zone$$S$$, the set of edges to be reevaluated in case the set of the winning states in $$S$$ ($$Win\mathrm{<mo\; stretchy="false">[</mo>}S\mathrm{<mo\; stretchy="false">]</mo>}$$) is updated. Using this on-the-fly method, in each step, a part of the state zone graph is constructed and an edge $$e\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}S\mathrm{,}a\mathrm{,}{S}^{\prime }\mathrm{<mo\; stretchy="false">)</mo>}$$ of the $$Waiting$$ list is processed. If the state zone $$S^{\prime }$$ is not in $$Passed$$ and there is, in$$S^{\prime }$$, some states which satisfy the desired reachability property, then these states are added to the winning states of $$S^{\prime }$$ ($$Win\mathrm{<mo\; stretchy="false">[</mo>}{S}^{\prime }\mathrm{<mo\; stretchy="false">]</mo>}$$). The winning states of $$S$$ will be recomputed later (the edge $$e$$ is added to the $$Waiting$$ list). If $$S^{\prime }$$ is in$$Passed$$, the set of the winning states of $$S$$ ($$Win\mathrm{<mo\; stretchy="false">[</mo>}S\mathrm{<mo\; stretchy="false">]</mo>}$$) is recomputed and possibly those of its predecessors and so on. The set $$Win\mathrm{<mo\; stretchy="false">[</mo>}S\mathrm{<mo\; stretchy="false">]</mo>}$$ is the largest subset of $$S$$ which 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 $${\alpha }_4$$ and$${\alpha }_6$$) by choosing appropriately the firing intervals for controllable transitions.

From the initial state class$${\alpha }_0$$, there are two elementary paths $${\alpha }_0{t}_1{\alpha }_1{t}_3{\alpha }_4$$ and $${\alpha }_0{t}_1{\alpha }_1{t}_2{\alpha }_3{t}_3{\alpha }_6$$ that lead to bad states. In both paths, there is only one state class ($${\alpha }_0$$) where the controllable transition $$t_1$$ is firable. To avoid these bad paths, we propose to compute all states of $${\alpha }_0$$ from which $$t_1{t}_3$$ or $$t_1{t}_2{t}_3$$ is firable, i.e., $$B\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo>}Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1{t}_3\mathrm{<mo\; stretchy="false">)</mo>}\cup Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1{t}_2{t}_3\mathrm{<mo\; stretchy="false">)</mo>}$$, where:

$$Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1{t}_3\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo\; stretchy="false">(</mo>}{p}_1+p_2\mathrm{,0}\le {\underset{\_}{t}}_1\le 1\wedge 2\le {\underset{\_}{t}}_2\le 3\wedge 2\le {\underset{\_}{t}}_2-{\underset{\_}{t}}_1\le \mathrm{3<mo\; stretchy="false">)</mo>}$$E15

and

$$Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1{t}_2{t}_3\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo\; stretchy="false">(</mo>}{p}_1+p_2\mathrm{,0}\le {\underset{\_}{t}}_1\le 2\wedge 2\le {\underset{\_}{t}}_2\le 3\wedge 1\le {\underset{\_}{t}}_2-{\underset{\_}{t}}_1\le \mathrm{3<mo\; stretchy="false">)</mo>}$$E16

.

To avoid these bad states, it suffices to replace in$${\alpha }_0$$, the firing interval of $$t_1$$ with$$\mathrm{<mo\; stretchy="false">]</mo>2,4<mo\; stretchy="false">]</mo>}$$. This interval is the complement of $$\mathrm{<mo\; stretchy="false">[</mo>0,2<mo\; stretchy="false">]</mo>}\cup \mathrm{<mo\; stretchy="false">[</mo>0,1<mo\; stretchy="false">]</mo>}$$ in the firing interval of $$t_1$$ in $${\alpha }_0$$ ($$\mathrm{<mo\; stretchy="false">[</mo>0,4<mo\; stretchy="false">]</mo>}$$).

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 $$t$$ of a state class $$\alpha$$ is obtained by subtracting from its interval in $$\alpha$$ ($$INT\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>}$$), intervals of $$t$$ in 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 $$I$$ and $$I^{\prime }$$ be two nonempty (real) intervals. We denote $$I\oplus I^{\prime }$$ intervals defined by:

$$\forall a\in ℝ\mathrm{,}a\in I\oplus I^{\prime }iff\exists b\in I\mathrm{,}\exists c\in I^{\prime }\mathrm{,}a\mathrm{<mo>=</mo>}b+c\mathrm{.}$$E17

As an example, for $$I\mathrm{<mo>=</mo><mo\; stretchy="false">[</mo>1,4<mo\; stretchy="false">]</mo>}$$ and$$I^{\prime }\mathrm{<mo>=</mo><mo\; stretchy="false">]</mo>2,5<mo\; stretchy="false">]</mo>}$$,$$I\oplus I^{\prime }\mathrm{<mo>=</mo><mo\; stretchy="false">]</mo>3,9<mo\; stretchy="false">]</mo>}$$. And also

$$LI\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo><mo\; stretchy="false">(</mo>}{t}_c\mathrm{,}{t}_s\mathrm{,}BI\mathrm{<mo\; stretchy="false">)</mo><mo>|</mo>}{t}_c\in E{n}_c\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo>,}{t}_s\in E{n}_c^0\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{<mo\; stretchy="false">)</mo><mo>;</mo>}BI\mathrm{<mo>=</mo>}\underset{\omega \in \Omega \mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{<mo\; stretchy="false">)</mo>}}{{\displaystyle \cup }}INT\mathrm{<mo\; stretchy="false">(</mo>}Fire\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo>,}{\underset{\_}{t}}_c-{\underset{\_}{t}}_s\mathrm{<mo\; stretchy="false">)</mo>}\ne INT\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}{\underset{\_}{t}}_c-{\underset{\_}{t}}_s\mathrm{<mo\; stretchy="false">)</mo><mo>\}</mo>}$$E18

This method is presented in the algorithms 6 and 7. The symbol $$T_c$$ refers to the set of controllable transitions and all forbidden markings of the net are saved in a set called, bad. The list $$Passed$$ is 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 $$main$$ consists of an initialization step and a calling to the recursive function$$explore$$. The call $$explore\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}\varnothing \mathrm{,<mo>\{</mo>}{\alpha }_0\mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo>}$$ returns the set of bad sequences that cannot be avoided, from$${\alpha }_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 $$\alpha$$ 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$$\alpha$$. The control of $$\alpha$$ 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$$\alpha$$. We get in$$Ctrl$$, all possibilities of controlling each state class. In case there is only one controllable transition in$$\alpha$$, its delay with a fictitious transition whose time variable is fixed at $$0$$ is considered.

Each element of $$Passed$$ is a triplet $$\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\Omega \mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{<mo\; stretchy="false">)</mo>,}LI\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{<mo\; stretchy="false">)</mo><mo\; stretchy="false">)</mo>}$$ where $$\alpha \mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}M\mathrm{,}F\mathrm{<mo\; stretchy="false">)</mo>}$$ is a state class s.t.$$M\notin bad$$, $$\Omega \mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{<mo\; stretchy="false">)</mo>}$$is the set of bad sequences of$$\alpha$$, which cannot be avoided, independently of$$\alpha$$, from its successors, and $$LI\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{<mo\; stretchy="false">)</mo>}$$ gives the intervals of controllable transitions in bad subclasses of $$\alpha$$ (bad intervals). The set $$LI\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{<mo\; stretchy="false">)</mo>}$$ allows to retrieve the safe intervals of controllable transitions, by computing the complements, in$$\alpha$$, of the forbidden intervals (i.e., all possibilities of controlling$$\alpha$$,$$Ctrl\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{<mo\; stretchy="false">)</mo>}$$).

The function $$explore$$ receives parameters $$\alpha$$ being the class under process, $$t$$the transition leading to $$\alpha$$ and $$\mathcal{C}$$ the set of traveled classes in the current path. It uses functions $$succ\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}t\mathrm{<mo\; stretchy="false">)</mo>}$$ and $$Fire\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\omega \mathrm{<mo\; stretchy="false">)</mo>}$$ already explained by equations (5) and (6) (in sections 2.3 and 2.4, respectively). It distinguishes $$3$$ cases:

1. $$\alpha$$$$\alpha$$$$Passed$$$$t$$$$\alpha$$$$\alpha$$$$\alpha$$$$\alpha$$$$\alpha$$$$\alpha$$$$t$$$$Dep\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}t\mathrm{,}LI\mathrm{<mo\; stretchy="false">)</mo>}$$$$\alpha$$$$t$$
2. $$\alpha$$$$\alpha$$$$t$$$$\alpha$$

3. In other cases, the function $$explore$$ is called for each successor of$$\alpha$$, not already encountered in the current path (see Figure 5), to collect, in$$\Omega$$, the bad sequences of its successors. Once all successors are processed, $$\Omega$$is checked:

3.1. If$$\Omega \mathrm{<mo>=</mo>}\varnothing$$, it means that $$\alpha$$ does not lead to any bad state class or its bad sequences can be avoided later by controlling its successors, then$$\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\varnothing \mathrm{,}\varnothing$$) is added to $$Passed$$ and the function returns with$$\varnothing$$.

3.2. If$$\Omega \ne \varnothing$$, the function $$explore$$ determines intervals of controllable transitions in bad subclasses, which do not cover their intervals in$$\alpha$$. It gets such intervals, identifying states to be avoided, in $$LI$$ (bad intervals). It adds $$\mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\Omega \mathrm{,}LI\mathrm{<mo\; stretchy="false">)</mo>}$$ to $$Passed$$ and then verifies whether or not $$\alpha$$ 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 $$\alpha$$ and then the empty set is returned by the function. Otherwise, it is needed to propagate the control to its predecessor by$$t$$. The set of sequences, obtained by prefixing with $$t$$ sequences of$$\Omega$$, 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 have$$T_c\mathrm{<mo>=</mo><mo>\{</mo>}{t}_1\mathrm{<mo>\}</mo>}$$, $$bad\mathrm{<mo>=</mo><mo>\{</mo>}{p}_2\mathrm{,}{p}_4\mathrm{<mo>\}</mo>}$$, $$Passed\mathrm{<mo>=</mo>}\varnothing$$and$${\alpha }_0\mathrm{<mo>=</mo><mo\; stretchy="false">(</mo>}{p}_1+p_2\mathrm{,0}\le {\underset{\_}{t}}_1\le 4\wedge 2\le {\underset{\_}{t}}_2\le \mathrm{3<mo\; stretchy="false">)</mo>}$$.

Figure 8.

Applying Algorithms 6 & 7 on the TPN at Figure 1 for $$AGnot{p}_1+p_3\mathrm{<mo>=</mo>0}$$

The process starts by calling $$explore\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}\epsilon \mathrm{,<mo>\{</mo>}{\alpha }_0\mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo>}$$ (see Figure 6). Since $${\alpha }_0$$ is not in $$Passed$$ and its marking is not forbidden, $$explore$$is successively called for the successors of$${\alpha }_0$$: $$explore\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_1\mathrm{,}{t}_1\mathrm{,<mo>\{</mo>}{\alpha }_0\mathrm{,}{\alpha }_1\mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo>}$$and$$explore\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_2\mathrm{,}{t}_2\mathrm{,<mo>\{</mo>}{\alpha }_0\mathrm{,}{\alpha }_2\mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo>}$$. In $$explore$$ of$${\alpha }_1$$, function $$explore$$ is successively called for $${\alpha }_3$$ and$${\alpha }_4$$. In $$explore$$ of$${\alpha }_3$$, function $$explore$$ is called for the successor $${\alpha }_6$$ of $${\alpha }_3$$ by$$t_3$$:$$explore\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_6\mathrm{,}{t}_3\mathrm{,<mo>\{</mo>}{\alpha }_0\mathrm{,}{\alpha }_1\mathrm{,}{\alpha }_3\mathrm{,}{\alpha }_6\mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo>}$$. For the successor of $${\alpha }_3$$ by $$t_4$$ (i.e.,$${\alpha }_0$$), there is no need to call $$explore$$ as it belongs to the current path. Since $${\alpha }_6$$ has a forbidden marking, $$explore$$of $${\alpha }_6$$ returns to $$explore$$ of $${\alpha }_3$$ with$$\mathrm{<mo>\{</mo>}{t}_3\mathrm{<mo>\}</mo>}$$, which, in turn, adds $$\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_3\mathrm{,<mo>\{</mo>}{t}_2{t}_3\mathrm{<mo>\}</mo>,}\varnothing \mathrm{<mo\; stretchy="false">)</mo>}$$ to $$Passed$$ and returns to $$explore$$ of $${\alpha }_1$$ with$$\mathrm{<mo>\{</mo>}{t}_2{t}_3\mathrm{<mo>\}</mo>}$$.

In $$explore$$ of$${\alpha }_1$$, function $$explore$$ is called for $${\alpha }_4$$ ($$explore\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_4\mathrm{,}{t}_3\mathrm{,<mo>\{</mo>}{\alpha }_0\mathrm{,}{\alpha }_1\mathrm{,}{\alpha }_4\mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo>}$$). This call returns, to $$explore$$ of$${\alpha }_1$$, with$$\mathrm{<mo>\{</mo>}{t}_3\mathrm{<mo>\}</mo>}$$, since $${\alpha }_4$$ has a forbidden marking. In $$explore$$ of$${\alpha }_1$$, the tuple $$\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_1\mathrm{,<mo>\{</mo>}{t}_2{t}_3\mathrm{,}{t}_3\mathrm{<mo>\}</mo>,}\varnothing \mathrm{<mo\; stretchy="false">)</mo>}$$ is added to $$Passed$$ and $$\mathrm{<mo>\{</mo>}{t}_1{t}_2{t}_3\mathrm{,}{t}_1{t}_3\mathrm{<mo>\}</mo>}$$ is returned to $$explore$$ of$${\alpha }_0$$. Then, $$explore$$of $${\alpha }_0$$ calls$$explore\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_2\mathrm{,}{t}_2\mathrm{,<mo>\{</mo>}{\alpha }_0\mathrm{,}{\alpha }_2\mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo>}$$, which in turn calls$$explore\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_5\mathrm{,}{t}_1\mathrm{,<mo>\{</mo>}{\alpha }_0\mathrm{,}{\alpha }_2\mathrm{,}{\alpha }_5\mathrm{<mo>\}</mo><mo\; stretchy="false">)</mo>}$$. Since $${\alpha }_5$$ has only one successor ($${\alpha }_0$$) and this successor belongs to the current path, the call of $$explore$$ for $${\alpha }_5$$ adds $$\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_5\mathrm{,}\varnothing \mathrm{,}\varnothing \mathrm{<mo\; stretchy="false">)</mo>}$$ to $$Passed$$ and returns to $$explore$$ of $${\alpha }_2$$ with$$\varnothing$$, which, in turn, returns to $$explore$$ of$${\alpha }_0$$.

After exploring both successors of$${\alpha }_0$$, in $$explore$$ of$${\alpha }_0$$, we get in $$\Omega \mathrm{<mo>=</mo><mo>\{</mo>}{t}_1{t}_2{t}_3\mathrm{,}{t}_1{t}_3\mathrm{<mo>\}</mo>}$$ the set of bad paths of$${\alpha }_0$$. As the state class $${\alpha }_0$$ has a controllable transition$$t_1$$, its bad subclasses are computed: $$Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1{t}_2{t}_3\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo><mo\; stretchy="false">(</mo>}{p}_1+p_2\mathrm{,0}\le {\underset{\_}{t}}_1\le 2\wedge 2\le {\underset{\_}{t}}_2\le 3\wedge 1\le {\underset{\_}{t}}_2-{\underset{\_}{t}}_1\le \mathrm{3<mo\; stretchy="false">)</mo>}$$and$$Fire\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,}{t}_1{t}_3\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo\; stretchy="false">(</mo>}{p}_1+p_2\mathrm{,0}\le {\underset{\_}{t}}_1\le 1\wedge 2\le {\underset{\_}{t}}_2\le 3\wedge 2\le {\underset{\_}{t}}_2-{\underset{\_}{t}}_1\le \mathrm{3<mo\; stretchy="false">)</mo><mo>\}</mo>}$$. The firing interval of $$t_1$$ in $${\alpha }_0$$ ($$\mathrm{<mo\; stretchy="false">[</mo>0,4<mo\; stretchy="false">]</mo>}$$) is not covered by the union of intervals of $$t_1$$ in bad subclasses of $${\alpha }_0$$ ($$\mathrm{<mo\; stretchy="false">[</mo>0,2<mo\; stretchy="false">]</mo>}\cup \mathrm{<mo\; stretchy="false">[</mo>0,1<mo\; stretchy="false">]</mo>}\ne \mathrm{<mo\; stretchy="false">[</mo>0,4<mo\; stretchy="false">]</mo>}$$). Then, $$\mathrm{<mo\; stretchy="false">(</mo>}{\alpha }_0\mathrm{,<mo>\{</mo>}{t}_1{t}_2{t}_3\mathrm{,}{t}_1{t}_3\mathrm{<mo>\}</mo>,<mo>\{</mo><mo\; stretchy="false">(</mo>}{t}_1\mathrm{,}{t}_0\mathrm{,<mo>\{</mo><mo\; stretchy="false">[</mo>0,2<mo\; stretchy="false">]</mo><mo>\}</mo><mo\; stretchy="false">)</mo><mo>\}</mo><mo\; stretchy="false">)</mo>}$$is added to$$Passed$$. As $$t_1$$ is newly enabled, the empty set is returned to the function$$main$$, which concludes that a controller exists. According with the list$$Passed$$, $${\alpha }_0$$needs to be controlled ($$Ctrl\mathrm{<mo\; stretchy="false">[</mo>}{\alpha }_0\mathrm{<mo\; stretchy="false">]</mo><mo>=</mo><mo>\{</mo><mo\; stretchy="false">(</mo>}{t}_1\mathrm{,}{t}_0\mathrm{,<mo>\{</mo><mo\; stretchy="false">[</mo>0,4<mo\; stretchy="false">]</mo>}-\mathrm{<mo\; stretchy="false">[</mo>0,2<mo\; stretchy="false">]</mo><mo>\}</mo><mo\; stretchy="false">)</mo><mo>\}</mo>}$$). 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 $$t_1$$ with$$\mathrm{<mo\; stretchy="false">]</mo>2,4<mo\; stretchy="false">]</mo>}$$. 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 duplicating$$t_1$$, 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 at Figure 1 for $$AGnot{p}_1+p_3\mathrm{<mo>=</mo>0}$$

Marking	Constraint to be applied on $$t_1$$
$$p_1+p_2$$	$$\mathrm{2<mo><</mo>}{\underset{\_}{t}}_1\le 4$$
Others	$$0\le {\underset{\_}{t}}_1\le 4$$

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 $$\alpha$$ can be partitioned in two subsets: the set of bad sequences that can be avoided from $$\alpha$$ and the set of bad sequences that cannot to be avoided from$$\alpha$$. The former set is avoided from $$\alpha$$ while the latter is let to be controlled by the predecessors of$$\alpha$$. The function $$explore$$ in this case should return the set of bad sequences that cannot be controlled from$$\alpha$$. 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 $$t_c$$ be a controllable transition whose interval needs to be restricted and$$SIr\mathrm{<mo\; stretchy="false">(</mo>}{t}_c\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}Ir\mathrm{<mo>|</mo>}\forall \mathrm{<mo\; stretchy="false">(</mo>}\alpha \mathrm{,}\Omega \mathrm{,}L\mathrm{<mo\; stretchy="false">)</mo>}\in Passed\mathrm{,}\exists \mathrm{<mo\; stretchy="false">(</mo>}{t}_c\mathrm{,}SI\mathrm{<mo\; stretchy="false">)</mo>}\in Ctrl\mathrm{<mo\; stretchy="false">[</mo>}\alpha \mathrm{<mo\; stretchy="false">]</mo>,}Ir\subseteq SI\wedge Ir\ne \varnothing \mathrm{<mo>\}</mo>}$$. The static firing interval of $$t_c$$ should be replaced with any interval of$$SIr\mathrm{<mo\; stretchy="false">(</mo>}{t}_c\mathrm{<mo\; stretchy="false">)</mo>}$$. Note that $$SIr\mathrm{<mo\; stretchy="false">(</mo>}{t}_c\mathrm{<mo\; stretchy="false">)</mo>}$$ 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 $$t_1$$ with$$\mathrm{<mo\; stretchy="false">[</mo>2,4<mo\; stretchy="false">]</mo>}$$.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 $$t_c$$ be a controllable transition whose interval needs to be restricted and$$SIm\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}{t}_c\mathrm{<mo\; stretchy="false">)</mo><mo>=</mo><mo>\{</mo>}Im\mathrm{<mo>|</mo>}\forall \mathrm{<mo\; stretchy="false">(</mo><mo\; stretchy="false">(</mo>}M\mathrm{,}I\mathrm{<mo\; stretchy="false">)</mo>,}\Omega \mathrm{,}L\mathrm{<mo\; stretchy="false">)</mo>}\in Passed\mathrm{,}\exists \mathrm{<mo\; stretchy="false">(</mo>}{t}_c\mathrm{,}SI\mathrm{<mo\; stretchy="false">)</mo>}\in Ctrl\mathrm{<mo\; stretchy="false">[</mo><mo\; stretchy="false">(</mo>}M\mathrm{,}I\mathrm{<mo\; stretchy="false">)</mo><mo\; stretchy="false">]</mo>,}Im\subseteq SI\wedge Im\ne \varnothing \mathrm{<mo>\}</mo>}$$. For each marking$$M$$, the firing interval of each controllable transition $$t_c$$ enabled in $$M$$ should be any interval of$$SIm\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}{t}_c\mathrm{<mo\; stretchy="false">)</mo>}$$. The set $$SIm\mathrm{<mo\; stretchy="false">(</mo>}M\mathrm{,}{t}_c\mathrm{<mo\; stretchy="false">)</mo>}$$ 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 $$AFgoal$$ meaning 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 $$goal$$ stands 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.