# Controller Synthesis of Time Petri Nets Using Stopwatch

Authors: Parisa Heidari; Hanifa Boucheneb
Journal: Journal of Engineering
 (2013)

---

## Abstract

Scheduling is often a difficult task specially in complex systems. Few tools are targeted at both modeling and scheduling of the systems. In controller synthesis, a scheduler is seen as a controller to
manage shared resources and timing requirements of a system. This paper proposes a time Petri net-based approach for controller synthesis and finding a scheduler using stopwatch. The solution suggested
here is particularly interesting for preemptive scheduling purposes. This paper deals with time Petri nets with controllable and uncontrollable transitions and assumes that a controllable transition can be suspended and retrieved when necessary. In fact, the paper supposes that every controllable transition can be associated with stopwatch. With this hypothesis, the objective is to model a system by time Petri nets and calculate subintervals where the system violates the given property. Then, the controller associates the corresponding controllable transitions with stopwatch to suspend them in their bad subintervals. The interesting advantage of this solution is that this approach synthesizes an ordinary time Petri net model before adding stopwatch. Therefore, complicated computations and overapproximations required during controller synthesis of time Petri nets associated
with stopwatch are avoided.


---

## Body

## 1. Introduction

A scheduler is a kind of controller that manages shared resources and timing specifications of the system. In the concept of controller synthesis, actions are partitioned into two disjoint sets,controllable and uncontrollable. Controllable actions are those that can be managed by the controller (forced to happen or prevented from happening). Uncontrollable actions are those that the controller has no control on. As an example, an internal counter in a digital system progresses with each clock cycle until it captures a predefined value and is reset after then. In a multitasking system, a newly arrived task waits for accessing resources. After accessing the required resources, each task spends its execution time and then releases the resources. If the task is periodic, it stays in a passive state before its next arrival. Process arrival depends on its period and its termination depends on the execution time. Then, both process arrival and termination of execution are uncontrollable, whereas access to the shared resources and starting the execution are controllable [1].In order to manage shared resources among different periodic tasks with different levels of priority, the solution is to suspend a task with the lower priority and let the others with the higher priorities execute and use the resources. Then, the suspended task is retrieved until it finishes its execution. When a task is suspended, the execution time is not progressing. This behavior is modeled by stopwatch.Stopwatch is an extension of timed models to facilitate modeling of interruption and resumption of a job. Once an interrupt happens, a task is suspended. Later, it is retrieved and continued from where it was interrupted. During the interruption, the clock of interrupted task is stopped while other clocks progress normally. The idea of stopwatch has been discussed and extended to timed automata (TA) as well as time petri nets (TPN) and some types of TA and TPN associated with stopwatch are already introduced [2–5]. In stopwatch, we may have some states whose clocks keep progressing, while in some other states the clock is stopped and keeps the value it had before being interrupted as if the clock has a memory and after being retrieved it continues with its previous value.In a multitasking real-time system with interruptible tasks and shared resources, a suitable scheduler is necessary to manage the resources and to prevent blocking and deadlock. The scheduler guarantees the well functionality of the system in terms of respecting deadline, priority, and similar constraints. Each task cannot start execution until the required resources are available. A task releases the occupied resources after finishing its execution.In multitasking systems, tasks are categorized to periodic, aperiodic, and sporadic [6].(i)Periodic Task. Periodic tasks arrive in regular intervals. Worst-case and best-case execution time is of the specifications defined for periodic tasks. Deadline is the other characteristic defined for these tasks with respect to their worst-case execution time. Deadline in periodic tasks can be either soft or hard. A critical deadline is called hard deadline whereas meeting a soft deadline is not critical.(ii)Aperiodic Task. Tasks with irregular interarrivals are called aperiodic. Aperiodic tasks are usually associated with soft deadlines.(iii)Sporadic Task. Aperiodic tasks with a minimum interarrival are called sporadic. Sporadic tasks are associated with hard deadlines.A periodic task may have the following three states [7].(i)Waiting. Once a periodic task arrives, it should wait for required resources.(ii)Execution. When all required resources are available, the task starts its execution and spends its execution time in this state.(iii)Passive. After being executed, the task releases the required resources and waits until its next arrival. The time between two consecutive task arrivals is equal with the given period.In a multitasking system with periodic tasks, the scheduler should manage the shared resources in a way that the predefined period for the tasks is respected. On the other hand, some of the tasks may be associated with a deadline or priority. In that case, the scheduler should suspend the execution of a task with lower priority and let the higher priority tasks to use the resources. Once the tasks with higher priority are executed, the other tasks with lower priorities are retrieved and continue their execution. This behavior is called preemptive scheduling.In the field of controller synthesis, a scheduler is seen as a controller [7, 8]. The scheduler should manage the shared resources and starts execution of each task in a way that the timing constraints, deadlines, and priorities are respected. Arrival of each task is due to its period and then is uncontrollable. Execution time is also predefined and then is uncontrollable. The only controllable action is the starting of an execution. In preemptive scheduling, a task can be suspended during its execution and leave the resources to some other task with a higher priority.One solution is to model the system with time Petri nets associated with stopwatch. In this context, each task execution is modeled by a transition equipped with stopwatch and then the corresponding controller is synthesized to manage suspension and resumption of each task such that the corresponding timing constraints are respected. As we will see in this paper, one problem with this solution is that the state space of time Petri nets associated with stopwatch is not exact and requires some overapproximation.The other problem is that time Petri nets associated with stopwatch does not preserve the boundedness property. Let𝒩1 be a time Petri net, 𝒩2 be a time Petri net associated with stopwatch, and SCG shows the corresponding state class graph, the following relation holds:
(1)𝒩1isbounded⟺SCGof𝒩1isfinite.This condition is not always true for a time Petri net associated with stopwatch. In other terms,(2)𝒩2isbounded⇏SCGof𝒩2isfinite.Indeed, if the number of reachable markings in a time Petri net associated with stopwatch is finite, the number of state classes is not necessarily finite [3]. These limitations hinder the controller synthesis of time Petri nets with stopwatch.In this paper, we suggest an alternative solution. We propose to synthesize a time Petri net without stopwatch where the transitions corresponding to the task executions are considered controllable. We extract the controller (i.e., scheduling strategy) and then add the stopwatch to model the controlled system (the system and its scheduler). In fact, we suggest to implement the synthesized controller by means of stopwatch.In the following, we discuss how the algorithm suggested in [9] for controller synthesis of time Petri nets is used for scheduling purposes to synthesize a controller for interruptible tasks. The algorithm of [9] is permissive and the computed controller is restricting time intervals making the system to satisfy the given properties. In this paper, we suggest to suspend a task during its bad subinterval. This approach is useful for preemptive scheduling purposes where safety properties correspond to meeting deadlines, priorities, preventing deadlock for shared resources, and so forth.In this paper, we use a synthesized controller (output of the algorithm of [9] in particular), and we show how to control the system using stopwatch. In order to implement the controller by means of stopwatch, we assume that it is possible to associate each controllable transition with a stopwatch so as to suspend or resume it whenever needed.The rest of this paper is organized as follows. Section2 is dedicated to time Petri nets, their definition, and semantics. Section 3 presents a literature review on different stopwatch Petri nets. Section 4 has a brief survey on the solution proposed in [9]. Section 5 synthesizes a controller using stopwatch. Section 6 presents an example of a multitasking system. Finally, Section 7 gives the conclusion and future work.


## 2. Time Petri Nets

A time Petri net (TPN) is a Petri net augmented with time intervals associated with transitions. This paper focuses on the classical semantics, called intermediate semantics in [10], in the context of monoserver and strong semantics [11]. Formally, a TPN is a tuple (P,T,Pre,Post,M0,Is) where  (i)
P and T are finite sets of places and transitions such that (P∩T=∅).(ii)
Pre and Post are the backward and the forward incidence functions (Pre,Post:P×T→ℕ, where ℕ is the set of nonnegative integers).(iii)
M0 is the initial marking (M0:P→ℕ).(iv)
Is is the static interval function (Is:T→ℚ+×(ℚ+∪{∞})),ℚ+ is the set of nonnegative rational numbers. Is associates with each transition t an interval called the static firing interval of t. Bounds ↓Is(t) and ↑Is(t) of the interval Is(t) are the minimum and maximum firing delays of t, respectively.In a controllable time Petri net, transitions are partitioned into controllable and uncontrollable transitions, denoted byTc and Tu, respectively (with Tc∩Tu=∅ and T=Tc∪Tu). For the sake of simplicity and clarification, in this paper the controllable transitions are depicted as white bars, while the uncontrollable ones as black bars.A TPN, is called bounded if for every reachable markingM, there is a bound b∈ℕp where M≤b holds. In this condition, p stands for the number of places in P.LetM be a marking and t a transition. Transition t is enabled for M if and only if all required tokens for firing t are present in M, that is, ∀p∈P,M(p)≥Pre(p,t). Firing of t leads to the marking M′ defined by: ∀p∈P,M′(p)=M(p)-Pre(p,t)+Post(p,t). We denote En(M) the set of transitions enabled for M, that is, En(M)={t∈T∣∀p∈P,Pre(p,t)≤M(p)}. For t∈En(M), we denote CF(M,t) the set of transitions enabled in M but in conflict with t, that is, CF(M,t)={t′∈En(M)∣t′=t∨∃p∈P,M(p)<Pre(p,t′)+Pre(p,t)}. Let t∈En(M) and M′ the successor marking of M by t; a transition t′ is said to be newly enabled in M′ if and only if t′ is not enabled in the intermediate marking (i.e., M-Pre(·,t)) or t′=t. We denote New(M′,t) the set of transitions newly enabled M′, by firing t from M; that is, New(M′,t)={t′∈En(M′)∣t=t′∨∃p∈P,M′(p)-Post(p,t)<Pre(p,t′)}.The TPN state is defined as a pair(M,Id), where M is a marking and Id is a firing interval function (Id:En(M)→ℚ+×(ℚ+∪{∞})). The initial state is (M0,Id0) where M0 is the initial marking and Id0(t)=Is(t), for t∈En(M0). Let (M,Id) and (M′,Id′) be two states of the TPN model, θ∈ℝ+ and t∈T. The transition relation → over states is defined as follows.  (i)
(M,Id)→θ(M′,Id′), also denoted by (M,Id)+θ, if and only if the state (M′,Id′) is reachable from state (M,Id), after θ time units, that is, ⋀t′∈En(M)θ≤↑Id(t′),M′=M, and ∀t′′∈En(M′),Id′(t′′)=[Max(↓Id(t′′)-θ,0),↑Id(t′′)-θ].(ii)
(M,Id)→t(M′,Id′) if and only if the state (M′,Id′) is reachable from the state (M,Id) by immediately firing transition t, that is, t∈En(M),↓Id(t)=0, ∀p∈P,M′(p)=M(p)-Pre(p,t)+Post(p,t), and ∀t′∈En(M′),Id′(t′)=Is(t′), if t′∈New(M′,t), and Id′(t′)=Id(t′), otherwise.The TPN state space is the structure(𝒬,→,q0), where q0=(M0,Id0) is the initial state of the TPN and 𝒬={q∣q0→*q}(→* being the reflexive and transitive closure of the relation → defined above) is the set of reachable states of the model. A run in the TPN state space (𝒬,→,q0), of a state q∈𝒬, is a maximal sequence ρ=q1→θ1q1+θ1→t1q2→θ2q2+θ2→t2q3,…, such that q1=q. By convention, for any state qi, the relation qi→0qi holds. The sequence θ1t1θ2t2… is called the timed trace of ρ. The sequence t1t2,…, is called the firing sequence (untimed trace) of ρ. A marking M is reachable if and only if ∃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 q0.To use enumerative analysis techniques with time Petri nets, their generally infinite state spaces are abstracted. Abstraction techniques 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 the minimal resources in terms of time and space. The preserved properties are usually verified using standard analysis techniques on the abstractions [12]. Several state space abstraction methods have been proposed in the literature for time Petri nets (the state class graph(SCG) [13], the zone based graph(ZBG) [14], etc.). They may differ in the characterization of states (interval or clock states), the state agglomeration criteria, the abstract states representation, the preserved properties (markings, linear or branching properties), and their size.These abstractions are finite for all bounded time Petri nets. However, abstractions based on clocks are less interesting than the interval-based abstractions when only linear properties are of interest. Indeed, abstractions based on clocks do not enjoy naturally the finiteness property for bounded TPN with unbounded intervals as it is the case for abstractions based on intervals. The finiteness is enforced using an approximation operation, which may involve some overhead computation. The algorithm of [9] is based on the state class graph method.


### 2.1. The State Class Graph Method

In the state class graph method [13], 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 if and only if 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 α=(M,F), where M is a marking and F is a formula which characterizes the firing domain of α. For each transition ti enabled in M, there is a variable t_i, in F, representing its firing delay. F can be rewritten as a set of atomic constraints of the form  t_i-t_j≤c,   t_i≤c or -t_j≤c, where ti, tj are transitions, c∈ℚ∪{∞}, and ℚ is the set of rational numbers. (for economy of notation, we use operator ≤ even if c=∞):Each domain is expressed by the canonical form that is usually encoded by a difference bound matrix (DBM) [15]. The canonical form of F is encoded by the DBM D (a square matrix) of order |En(M)|+1 defined by: ∀ti,tj∈En(M)∪{t0},dij=(≤,SupF(t_i-t_j)), where t0 (t0∉T) represents a fictitious transition whose delay is always equal to 0 and SupF(t_i-t_j) is the largest value of t_i-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 some operations over formulas like the test of equivalence easier. Two formulas are equivalent if and only if the canonical forms of their DBMs are identical.The initial state class isα0=(M0,F0), where F0=⋀ti∈En(M0)↓Is(ti)≤t_i≤↑Is(ti). Let α=(M,F) be a state class and tf a transition and succ(α,tf) the set of states defined by: succ(α,tf)={q′∈𝒬∣∃q∈α,∃θ∈ℝ+s.t.q→θq+θ→tfq′}. The state class α has a successor by tf (i.e., succ(α,tf)≠∅), if and only if tf is enabled in M and can be fired before any other enabled transition; that is, the following formula is consistent: F∧(⋀ti∈En(M)t_f≤ti_). A formula F is consistent if and only if there is, at least, one tuple of values that satisfies, at once, all constraints of F. In this case, the firing of tf leads to the state class α′=(M′,F′)=succ(α,tf) computed as follows [13]. (1)
∀p∈P,M′(p)=M(p)-Pre(p,tf)+Post(p,tf).(2)
F′=F∧(⋀ti∈En(M)t_f-t_i≤0).(3)
Replace inF′ each t_i≠t_f, by (t_i+t_f).(4)
Eliminate by substitutiont_f and each t_i of transition conflicting with tf in M.(5)
Add constraint↓Is(tn)≤t_n≤↑Is(tn), for each transition tn∈New(M′,tf).Formally, the SCG of a TPN model is a structure(𝒞𝒞,→,α0), where α0=(M0,F0) is the initial state class, ∀ti∈T,α→tiα′ iff α′=succ(α,ti)≠∅ and 𝒞𝒞={α∣α0→*α}. The SCG is finite for all bounded TPNs and preserves linear properties [16]. 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ω=ϵ  and succ(α,ω)=succ(succ(α,ω′),ti), if  ω=ω′·ti.As an example, Figure2 shows the state class graph of the TPN presented at Figure 1. Its state classes are reported in Table 1.Table 1
The state classes of the TPN presented at Figure2.
α
0
:
p
1
+
p
2
0
≤
t
_
1
≤
4
∧
2
≤
t
_
2
≤
3
α
1
:
p
2
+
p
3
0
≤
t
_
2
≤
3
∧
2
≤
t
_
3
α
6
:
p
4
α
2
:
p
1
+
p
4
0
≤
t
_
1
≤
2
α
3
:
p
3
+
p
4
0
≤
t
_
3
∧
0
≤
t
_
4
≤
1
α
4
:
p
2
0
≤
t
_
2
≤
1
α
5
:
p
3
+
p
4
2
≤
t
_
3
<
∞
∧
0
≤
t
_
4
≤
1Figure 1
A simple Petri net withTc={t1}.Figure 2
The state graph of the TPN presented at Figure1.Letω be a sequence of transitions firable from α, the same transition may be newly enabled several times. To distinguish among different enablings of the same transition ti, we denote tik for k>0 the transition ti (newly) enabled by the kth transition of the sequence; ti0 denotes the transition ti enabled in M. Let ω=t1k1,…,tmkm∈T+ with m>0 be a sequence of transitions firable from α s.t. succ(α,ω)≠∅. We define Fire(α,ω) the largest subclass α′ of α (i.e., α′⊆α) s.t. ω is firable from all its states, that is, Fire(α,ω)={q1∈α|∃θ1,…,θm,q1→θ1q1+θ1→t1k1q2,…,qm+θm→tmkmqm+1}.


## 2.1. The State Class Graph Method

In the state class graph method [13], 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 if and only if 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 α=(M,F), where M is a marking and F is a formula which characterizes the firing domain of α. For each transition ti enabled in M, there is a variable t_i, in F, representing its firing delay. F can be rewritten as a set of atomic constraints of the form  t_i-t_j≤c,   t_i≤c or -t_j≤c, where ti, tj are transitions, c∈ℚ∪{∞}, and ℚ is the set of rational numbers. (for economy of notation, we use operator ≤ even if c=∞):Each domain is expressed by the canonical form that is usually encoded by a difference bound matrix (DBM) [15]. The canonical form of F is encoded by the DBM D (a square matrix) of order |En(M)|+1 defined by: ∀ti,tj∈En(M)∪{t0},dij=(≤,SupF(t_i-t_j)), where t0 (t0∉T) represents a fictitious transition whose delay is always equal to 0 and SupF(t_i-t_j) is the largest value of t_i-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 some operations over formulas like the test of equivalence easier. Two formulas are equivalent if and only if the canonical forms of their DBMs are identical.The initial state class isα0=(M0,F0), where F0=⋀ti∈En(M0)↓Is(ti)≤t_i≤↑Is(ti). Let α=(M,F) be a state class and tf a transition and succ(α,tf) the set of states defined by: succ(α,tf)={q′∈𝒬∣∃q∈α,∃θ∈ℝ+s.t.q→θq+θ→tfq′}. The state class α has a successor by tf (i.e., succ(α,tf)≠∅), if and only if tf is enabled in M and can be fired before any other enabled transition; that is, the following formula is consistent: F∧(⋀ti∈En(M)t_f≤ti_). A formula F is consistent if and only if there is, at least, one tuple of values that satisfies, at once, all constraints of F. In this case, the firing of tf leads to the state class α′=(M′,F′)=succ(α,tf) computed as follows [13]. (1)
∀p∈P,M′(p)=M(p)-Pre(p,tf)+Post(p,tf).(2)
F′=F∧(⋀ti∈En(M)t_f-t_i≤0).(3)
Replace inF′ each t_i≠t_f, by (t_i+t_f).(4)
Eliminate by substitutiont_f and each t_i of transition conflicting with tf in M.(5)
Add constraint↓Is(tn)≤t_n≤↑Is(tn), for each transition tn∈New(M′,tf).Formally, the SCG of a TPN model is a structure(𝒞𝒞,→,α0), where α0=(M0,F0) is the initial state class, ∀ti∈T,α→tiα′ iff α′=succ(α,ti)≠∅ and 𝒞𝒞={α∣α0→*α}. The SCG is finite for all bounded TPNs and preserves linear properties [16]. 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ω=ϵ  and succ(α,ω)=succ(succ(α,ω′),ti), if  ω=ω′·ti.As an example, Figure2 shows the state class graph of the TPN presented at Figure 1. Its state classes are reported in Table 1.Table 1
The state classes of the TPN presented at Figure2.
α
0
:
p
1
+
p
2
0
≤
t
_
1
≤
4
∧
2
≤
t
_
2
≤
3
α
1
:
p
2
+
p
3
0
≤
t
_
2
≤
3
∧
2
≤
t
_
3
α
6
:
p
4
α
2
:
p
1
+
p
4
0
≤
t
_
1
≤
2
α
3
:
p
3
+
p
4
0
≤
t
_
3
∧
0
≤
t
_
4
≤
1
α
4
:
p
2
0
≤
t
_
2
≤
1
α
5
:
p
3
+
p
4
2
≤
t
_
3
<
∞
∧
0
≤
t
_
4
≤
1Figure 1
A simple Petri net withTc={t1}.Figure 2
The state graph of the TPN presented at Figure1.Letω be a sequence of transitions firable from α, the same transition may be newly enabled several times. To distinguish among different enablings of the same transition ti, we denote tik for k>0 the transition ti (newly) enabled by the kth transition of the sequence; ti0 denotes the transition ti enabled in M. Let ω=t1k1,…,tmkm∈T+ with m>0 be a sequence of transitions firable from α s.t. succ(α,ω)≠∅. We define Fire(α,ω) the largest subclass α′ of α (i.e., α′⊆α) s.t. ω is firable from all its states, that is, Fire(α,ω)={q1∈α|∃θ1,…,θm,q1→θ1q1+θ1→t1k1q2,…,qm+θm→tmkmqm+1}.


## 3. Literature Review

The idea of suspension and resumption of a task in a system is modeled in different ways in timed automata and time Petri nets [2–4, 17, 18]. In [2], the authors have introduced stopwatch automata (SWA) as a subclass of timed linear hybrid automata. In stopwatch automata, an additional binary variable is defined to show the rate of time progression. The clocks may have two velocities (time derivation): zero or one. Zero signifies stopped while one signifies normal progress. If clocks are running, they progress with a global rate, identical to all nonstopped clocks of the model. The authors have shown that stopwatch automata is as expressive as timed languages.In [3], the authors have introduced inhibitor hyperarcs to interrupt an enabled transition. Once a place p connected to a transition t via an inhibitor arc is marked, the transition t is suspended and stops firing. In other words, once an inhibitor arc is enabled, the corresponding transition is interrupted. They have called these nets IHTPN (time Petri nets with inhibitor hyperarcs). In Figure 3, t1 is enabled. As soon as P2 is marked, firing t1 is suspended. Note that an inhibitor hyperarc is not graphically presented by a classical arrow; instead, it is depicted with an empty circle at the extreme of the edge.Figure 3
A simple example of time Petri nets with inhibitor hyperarc.t1 is active if p2 is not marked, otherwise it is suspended.In [17], the authors have discussed an extension of time Petri nets adapted for scheduling. This extension is called scheduling extended time Petri nets (SETPN). SETPN is suitable to model concurrent tasks and shared resources with fixed priority. The behavior of scheduler is implicitly included in the model and the scheduler is not modeled as a separate agent.In [17], time Petri nets are associated with two more properties γ and ω standing for resource allocation and priority, respectively. As an example, suppose two different concurrent tasks sharing the same resource (γ is identical for both). Although both transitions are enabled, the one with a higher priority is active while the other is suspended. For each marking M, a function Act determines whether M is active or not.The time Petri nets presented in [17] assign both priority and resources to places. It is particularly suitable for scheduling approaches. State space analysis is done mapping scheduling Petri nets to hybrid automata (state class stopwatch automata). The advantage of this solution is using an automated tool like HYTECH [19] already existing for manipulation of hybird automata.Another extension of time Petri nets called preemptive time Petri nets is discussed in [18]. Preemptive time Petri nets are suitable for scheduling and preemptive approaches. In Preemptive time Petri nets, resource and priority are characteristics of transitions while in SETPN they were assigned to places. The preemptive time Petri nets as well as scheduling extended time Petri nets are adapted specifically for scheduling purposes with fixed priority rather than general cases of interruption and resumption of some tasks. A more generalized model comes in [4, 5].Another stopwatch model comes in [4, 5]. Post- and Pre-initialized stopwatch Petri nets (SWPN) [4, 5] also model interruption and retrieving of tasks. In such stopwatch Petri nets, transitions are partitioned into two disjoint subclasses T=Tint∪Tno-int where Tint is the set of interruptible transitions and Tno-int is the set of noninterruptible transitions. Stopwatches can suspend enabled interruptible transitions. For each transition ti, there is a function v(ti) representing the value of its associated stopwatch. If ti∈Tint, v(ti) signifies the time elapsed since ti was first enabled, whereas if ti∈Tno-int, v(ti) represents the time elapsed since ti was last enabled. A transition is called firable if it is enabled (M>Pre(ti)) and ↓Is(ti)≤v(ti)≤↑Is(ti).In contrary with IHTPN where a marked place suspended an enabled transition, in this model stopwatch consumes some tokens to disable an enabled transition. It is implemented by means of some extra places/transitions. A stopwatch transition is in conflict with an interruptible transition. Thus, consuming a token can suspend an interruptible enabled transition. With this model, an interrupt is unpredictable and we do not know when it happens. In fact at any time, the interruptible task and the interrupt both have equal chance to happen. The simple Petri nets of Figure4 reported from [4] are a simple example of SWPN of an interruptible task.Figure 4
An interruptible task modeled by SWPN, reported from [4].Letti be a transition and M a marking, ti is called:  (i)
enabled. If M≥Pre(ti) denoted by ti∈En(M);(ii)
firable. If ti∈En(M)∧↓Is(ti)≤v(ti)≤↑Is(ti), denoted by ti∈Firable(M);(iii)
suspended. If Pre(ti)>M∧v(ti)>0, denoted by ti∈susp(M).The notion↑enabled(ti,M,tk) indicates that ti is newly enabled by firing of tk at marking M.The new concept Preinitialization defined in this model refers to noninterruptible transitions. For everyti∈Tno-int, ti is firable if v(ti) has already been initialized when ti becomes enabled. In other words, v(ti)=0 when ti∈↑enabled(ti,M,tk).The concept,postinitialization is defined for interruptible transitions. When an interruptible transition is fired the associated v(ti) is initialized (v(ti)=0). Figures 5 and 6 reported from [4] show the difference between time evolution in an interruptible transition and a noninterruptible transition. In these figures, the notions E,D, and F stand for enabling, disabling, and firing of a transition, respectively.Figure 5
Time elapses,ti is an interruptible transition.Figure 6
Time elapses,ti is a noninterruptible transition.In brief, according to the types of transitions, two types of clock initialization are defined.(i)
Preinitialization. Given a transition ti∈Tno-int where Tno-int is the set of noninterruptible transitions, clock initialization is called preinitialization happening when ti is recently enabled. As soon as a transition becomes enabled, its associated clock is initialized.(ii)
Postinitialization. Given a transition ti∈Tint where Tint is the set of interruptible transitions, clock initialization is called post-initialization happening after firing ti; it means that the transition initializes the clock after being fired. Post-initialization is dependent on transition firing.In [4], continuous and discrete transitions are defined as follows.Letd∈ℝ+, a continuous transition is denoted by (M,v)→d(M,v′) iff ∀ti∈T:  (i)
v′(ti)=v(ti), if the transition ti is not enabled;(ii)
v′(ti)=v(ti)+d if ti is enabled;(iii)
M≥Pre(ti)⇒v′≤↑Is(ti).And a discrete transition is denoted by(M,v)→ti(M′,v′) iff ∀ti∈T:  (i)
ti∈Firable(M),(ii)
M′=M-Pre(ti)+Post(ti),(iii)
v′(ti)=0 if ti∈Tint (postinitialization),(iv)
∀tk∈T,v′(tk)=
(a)
0 iftk∈↑enabled(tk,M,ti); (preinitialization)(b)
v(ti) Otherwise.In order to perform further timing analysis, the same as scheduling extended time Petri nets of [17], the SWPN is transformed to hybrid automaton. In addition, a forward algorithm is suggested to compute reachable states.If the number of stopwatches increases, for example if all of the transitions are interruptible, the complexity of calculation will highly increase. Scheduling time Petri nets and preemptive time Petri nets are both subclasses of stopwatch Petri nets. An ordinary TPN is also a SWPN whereTint=∅.After having a survey on different stopwatch Petri nets available in the literature, in the following, we will have a brief review on the algorithm of [9] and then investigate how to integrate stopwatch in the controller synthesis approach of [9].


## 4. Safety Controller Synthesis Approach Proposed in [9]

Let𝒩 be a TPN with controllable and uncontrollable transitions (T=Tc∪Tu) and a set of markings to be avoided (bad). For a safety property, the approach proposed in [9] (see Algorithms 1 and 2) consists of exploring, on-the-fly and path by path, the state class graph of the TPN 𝒩 while collecting the bad sequences and the losing states (sequences or states that lead to bad markings). The list Passed is used to retrieve the set of state classes processed so far, their bad sequences, and their losing subclasses. For a given state class α and a bad sequence ω feasible from α, the function Fire is used to compute forwardly all states of α which lead by a sequence of transitions to an undesirable marking (i.e., a losing subclass of α). The function explore receives parameters α being the class under process, t the transition leading to α, and 𝒞 the set of traveled classes in the current path. Succinctly, it recursively computes the bad sequences of α (from bad sequences of its successors) and verifies whether or not α can be controlled so as to avoid its bad sequences. It returns the set of bad sequences if they cannot be avoided from α. Otherwise, it returns an empty set, which means that α can be controlled (i.e., α has no bad sequences or there is at least one controllable transition tc such that its firing interval in α can be restricted so as to avoid reaching bad states). The restriction of the interval of tc in α is obtained by subtracting from its interval in α, intervals of tc in its bad subclasses.Algorithm 1:On-the-fly algorithm for the safety control of TPN-Part I.
Functionmain (TPN  𝒩,  Markings bad)
Where
𝒩
is a TPN
badis a set of bad markings.
Let  Tc  be the set of controllable transitions of  𝒩  and
α
0  the initial state class of  𝒩.
Passed
=
∅
If  (explore(α0,ϵ,{α0})≠∅)  then
{Controller does not exist}
return
end if
for all
(
(
α
,
Ω
,
LI
)
∈
Passed
)
do
Ctrl[α]=⋃(tc,ts,BI)∈LI‍{(tc,ts,INT(α,t_c-t_s)-BI)}
end for
(
*
Remarks:
)
α
=
(
M
,
F
);
E
n
c
(
M
)
=
En
(
M
)
∩
T
c;
E
n
c
0
(
M
)
=
E
n
c
(
M
)
∪
{
t
0
};
Ne
w
c
(
M
,
t
)
=
New
(
M
,
t
)
∩
T
c;
New
(
M
0
,
ϵ
)
=
En
(
M
0
);
t
0 is a fictitious transition whose time variable is fixed at 0.
Dep
(
α
,
t
,
LI
)
≡
∃
(
t
c
,
t
s
,
BI
)
∈
LI
,
t
c
∉
New
(
M
,
t
)
∧
(
t
s
∉
New
(
M
,
t
)
∨
INT
(
α
,
t
_
c
-
t
_
0
)
⊈
⋂
I
∈
BI
‍
(
I
⊕
INT
(
α
,
t
_
s
-
t
_
0
)
)
)Algorithm 2:On-the-fly algorithm for the safety control of TPN-Part II.
FunctionTraces explore (Class  α, Trans t,  Classes  𝒞)
if
(
∃
Ω
,
LI
s
.
t
.
(
α
,
Ω
,
LI
)
∈
Passed
) then
if(Ω≠∅∧Dep(α,t,LI))then
return{t·ω∣ω∈Ω}
end if
return  ∅
end if
if(M∈bad)then
return{t}
end if
TracesΩ=∅;
for all
t
′
∈
En
(
M
)  s.t  succ(α,t′)≠∅∧succ(α,t′)∉𝒞
do
Ω = Ω∪explore(succ(α,t′),t′,𝒞∪{succ(α,t′)})
end for  {Ω  contains all bad sequences of  α.}
if  (Ω=∅)then
Passed=Passed∪{(α,∅,∅)}
return  ∅
end if
LI
=
{
(
t
c
,
t
s
,
BI
)
∣
(
t
c
,
t
s
)
∈
E
n
c
(
M
)
×
E
n
c
0
(
M
)
∧
BI
=
⋃
ω
∈
Ω
INT
(
Fire
(
α
,
ω
)
,
t
_
c
-
t
_
s
)
⊂
INT
(
α
,
t
_
c
-
t
_
s
)
}
Passed
=
Passed
∪
{
(
α
,
Ω
,
LI
)
}
if  (Dep(α,t,LI))then
return{t·ω∣ω∈Ω}
end if
return
∅This approach tries to control the system behavior starting from the last to the first state class 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).In [20], we have proven that this approach gives the maximally permissive controller and if it fails to compute the controller then the controller does not exist. We have also investigated the hardness complexity of the approach step by step.(i)
The complexity of computing BI of a state class (in worst case) isO(K×L×nt2) where K is the number of paths starting from the state class and leading to bad markings, L is the maximal length of such paths, and nt is the number of transitions in the model.(ii)
The complexity for computing Dep relation used in Algorithms1 and 2 is O(|LI|×m×|BI|), where m is the number of places in the model (complexity of testing New(M,t)).In [14], the authors have discussed the completeness complexity for bounded TPNs. They have proven that model checking of TPN-TCTL formula on a bounded TPN is PSPACE-complete.Let us explain this approach, by means of an example. Consider the TPN shown at Figure1, its state class graph presented at Figure 2 and its state classes reported in Table 1. Suppose that only t1 is controllable (i.e., Tc={t1}) and we want to avoid reaching markings where places p1 and p3 are both not marked (i.e., state classes α4 and α6) by choosing appropriately the firing intervals of t1. For this example, we have Tc={t1}, bad={p2,p4}, Passed=∅, and α0=(p1+p2,0≤t_1≤4∧2≤t_2≤3).The process starts by callingexplore(α0,ϵ,{α0}) (see Figure 7). Since α0 is not in Passed and its marking is not forbidden, explore is successively called for the successors of α0: explore(α1,t1,{α0,α1}) and explore(α2,t2,{α0,α2}). In explore of α1, function explore is successively called for α3 and α4. In explore of α3, function explore is called for the successor α6 of α3 by t3: explore(α6,t3,{α0,α1,α3,α6}. For the successor of α3 by t4 (i.e., α0), there is no need to call explore as it belongs to the current path. Since α6 has a forbidden marking, explore of α6 returns to explore of α3 with {t3}, which, in turn, adds (α3,{t2t3},∅) to Passed and returns to explore of α1 with {t2t3}.Figure 7
Applying Algorithms1 and 2 on the TPN at Figure 1 for AG not p1+p3=0.In explore ofα1, function explore is called for α4 (explore(α4,t3,{α0,α1,α4})). This call returns, to explore of α1, with {t3}, since α4 has a forbidden marking. In explore of α1, the tuple (α1,{t2t3,t3},∅) is added to Passed and {t1t2t3,t1t3} is returned to explore of α0. Then, explore of α0 calls explore(α2,t2,{α0,α2}), which in turn calls explore(α5,t1,{α0,α2,α5}). Since α5 has only one successor (α0) and this successor belongs to the current path, the call of explore for α5 adds (α5,∅,∅) to Passed and returns to explore of α2 with ∅, which, in turn, returns to explore of α0.After exploring both successors ofα0, in explore of α0, we get in Ω={t1t2t3,t1t3} the set of bad paths of α0. As the state class α0 has a controllable transition t1, its bad subclasses are computed: Fire(α0,t1t2t3)={(p1+p2,0≤t_1≤2∧2≤t_2≤3∧1≤t_2-t_1≤3) and Fire(α0,t1t3)=(p1+p2,0≤t_1≤1∧2≤t_2≤3∧2≤t_2-t_1≤3)}. The firing interval of t1 in α0 ([0,4]) is not covered by the union of intervals of t1 in bad subclasses of α0 ([0,2]∪[0,1]≠[0,4]). Then, (α0,{t1t2t3,t1t3},{(t1,t0,{[0,2]})}) is added to Passed. As t1 is newly enabled, the empty set is returned to the function main, which concludes that a controller exists. According to the list Passed, α0 needs to be controlled (Ctrl[α0]={(t1,t0,{[0,4]-[0,2]})}). For all others, there is nothing to do.


## 5. Controller Synthesis and Stopwatch

In this section, we consider time Petri nets with controllable/uncontrollable transitions and show how such a system is controlled by associating some of the controllable transitions with stopwatch. First, we apply the on-the-fly algorithm of [9] and calculate the appropriate controller. Then, instead of restricting time intervals of corresponding controllable transitions, we associate them with stopwatch. In fact, we suspend some transition during its bad subinterval to control a system so as to satisfy a given property.We consider the inhibitor hyperarcs of [3]. The controller shall suspend a controllable transition in its bad subinterval and retrieve it otherwise. Let us remember the example of Figure 1 with the state class graph of Figure 2 and Table 1. We have seen that in order to prevent the system entering the forbidden state classes α4 and α6, the controller should prevent t1 from firing before ]2,4]. Thus, an inhibitor hyperarc is added to the transition t1. This inhibitor hyperarc connects t1 to a place called psusp. At the beginning, this place is marked and then t1 is suspended. At [2,2] the token of psusp is consumed and the corresponding hyperarc becomes disabled. The controllable transition t1 is now firable again. The token is returned to place psusp after t1 is fired. Thus, the controller suspends t1 during its bad subinterval and resumes it after then. At the beginning, all clocks are initialized to zero. Then, time elapses but in [0,2], this transition is suspended and hence its clock does not elapse anymore. Later at time [2,2], this transition is retrieved and becomes active. We do not need to delay it anymore, that is why the lower bound of the interval associated with t1 is modified to 0. Now the clock starts elapsing. Within 2 time units t1 should be fired (i.e., when the actual time of the general clock of the system reaches to 4). Then, the interval associated with t1 in a controlled TPN associated with stopwatch is [0,2]. Figure 8 represents the clock evaluation of the transition t1. The controlled Petri nets of this example are presented in Figure 9.Figure 8
Clock evaluation oft1 in the controlled TPN of Figure 9.Figure 9
Time Petri net of Figure1, controlled by inhibitor hyperarcs (Tc={t1}).In summary, our goal is to synthesize the state class graph of the system through Algorithms1 and 2 (see [9]) and calculate bad subintervals of the corresponding controllable transitions. Then, suspend the appropriate controllable transitions during their bad subintervals. Note that in [9], we were restricting and limiting time intervals while in this approach the idea is to delay and suspend them. In this research, we suppose every controllable transition can be associated with a stopwatch if needed. As explained earlier in Section 1, in a multitasking system with periodic tasks only execution of a task is controllable. Then, those transitions modeling the task executions are considered controllable and consequently could be suspended and retrieved.Above, we have shown how to control a system when the bad subinterval is at the beginning of the firing interval. What if the acceptable subinterval is at the beginning and bad subintervals are after? Consider the example of Figure10. A controllable transition t1 is associated with firing interval [a,b]. Suppose that, based on Algorithms 1 and 2, the subinterval [a,α1] is acceptable while ]α1,b] is a bad subinterval, where a≤α1<b. The controlled time Petri nets are presented in Figure 11. Figure 12 represents the clock evaluation of t1 and shows how the new interval associated with t1 is calculated. In [0,a[, psusp is marked and t1 is neither active nor enabled. Meanwhile, at the time a, tr1 becomes enabled and is fired consuming the token in psusp. Thus, right at a, the transition t1 becomes active and its associated clock starts elapsing. Note that associated stopwatch delays t1 for a time units and we do not want to delay it anymore; then, the lower bound of the new associated interval in controlled TPN is 0. After α1 time units, tr2 is fired, and psusp becomes marked again. Consequently, t1 is suspended.Figure 10
A simple time Petri net(Tc={t1}).Figure 11
The controlled TPN of Figure10 using inhibitor hyperarcs (Tc={t1}). Forbidden interval is ]α1,b] where a≤α1<b.Figure 12
Clock evaluation oft1 in the controlled TPN of Figure 10. Forbidden interval is ]α1,b] where a≤α1<b.Consider the same example of Figure10 and this time suppose that Algorithms 1 and 2 give the following output.[
a
,
α
1
[ is acceptable, [α1,α2[ is a bad subinterval, [α2,b] is acceptable where the condition a<α1<α2≤b holds. With the same idea, the controlled Petri nets are presented in Figure 13 and the clock evaluation of t1 is shown in Figure 14.Figure 13
A simple time Petri net controlled by inhibitor hyperarcs(Tc={t1}); the bad subinterval is [α1,α2[ where a<α1<α2≤b.Figure 14
Clock evaluation oft1 in a controlled TPN of Figure 10. The forbidden interval is ]α1,α2] where a<α1<α2≤b.


### 5.1. Why Inhibitor Hyperarcs?

We have shown, how to achieve a controlled model from an uncontrolled time Petri nets by adding inhibitor hyperarcs. One question is why among different types of stopwatch inhibitor hyperarcs are chosen? Is it possible to use another stopwatch model? The answer is yes; but, inhibitor hyperarcs provide more flexibility and less complication. Let us see if this idea is feasible using other types of Petri nets with stopwatch.We consider the post- and preinitialized Petri nets proposed in [4, 5] for stopwatch and try to control a model where a controllable transition associated with time interval [a,b] has a bad subinterval [a,α]. Based on our hypothesis, the controller should suspend the controllable transition at [a,a] and resume it at [α,α]. The characteristic of post and pre-initialized Petri nets is that they consume the same token of the original model and in addition, the exact time when the model becomes suspended is unknown as stopwatch transition and original transition have the same chance for firing. At the first glance, the idea is feasible by adding one place and two transitions. However, there are some issues. We explain the problem through an example.We consider the same example of Figure1. The suggested controlled model using post and pre-initialized Petri nets comes in Figure 15. The controllable transition t1 is associated with stopwatch. The stopwatch interrupts the task at [0,0] and resume it at [2,2]. The problem is at [0,0], both transitions t1 and tsus are enabled with equal chance of firing whereas, in order to have a controlled model, tsus should fire at [0,0] before t1. Thus, the controller fails unless if we modify the interval associated to t1 to ]0,2] which is not of interest in this approach.Figure 15
Controlling the example of Figure1 using stopwatch of [4]. The controller fails.The other alternative is presented at Figure16. An auxiliary place ps solves the problem. Hence, using the stopwatch Petri nets suggested in [4, 5], it is not easy to give a general solution to control a model considering the output of Algorithms 1 and 2. In addition, the resulting controlled nets are more complicated. For example, in case the controllable transition is associated with the interval [a,b] where its bad subinterval is [α,b] and a≤α then, the controlled model becomes complicated.Figure 16
Controlled model of Figure1 using stopwatch of [4].


## 5.1. Why Inhibitor Hyperarcs?

We have shown, how to achieve a controlled model from an uncontrolled time Petri nets by adding inhibitor hyperarcs. One question is why among different types of stopwatch inhibitor hyperarcs are chosen? Is it possible to use another stopwatch model? The answer is yes; but, inhibitor hyperarcs provide more flexibility and less complication. Let us see if this idea is feasible using other types of Petri nets with stopwatch.We consider the post- and preinitialized Petri nets proposed in [4, 5] for stopwatch and try to control a model where a controllable transition associated with time interval [a,b] has a bad subinterval [a,α]. Based on our hypothesis, the controller should suspend the controllable transition at [a,a] and resume it at [α,α]. The characteristic of post and pre-initialized Petri nets is that they consume the same token of the original model and in addition, the exact time when the model becomes suspended is unknown as stopwatch transition and original transition have the same chance for firing. At the first glance, the idea is feasible by adding one place and two transitions. However, there are some issues. We explain the problem through an example.We consider the same example of Figure1. The suggested controlled model using post and pre-initialized Petri nets comes in Figure 15. The controllable transition t1 is associated with stopwatch. The stopwatch interrupts the task at [0,0] and resume it at [2,2]. The problem is at [0,0], both transitions t1 and tsus are enabled with equal chance of firing whereas, in order to have a controlled model, tsus should fire at [0,0] before t1. Thus, the controller fails unless if we modify the interval associated to t1 to ]0,2] which is not of interest in this approach.Figure 15
Controlling the example of Figure1 using stopwatch of [4]. The controller fails.The other alternative is presented at Figure16. An auxiliary place ps solves the problem. Hence, using the stopwatch Petri nets suggested in [4, 5], it is not easy to give a general solution to control a model considering the output of Algorithms 1 and 2. In addition, the resulting controlled nets are more complicated. For example, in case the controllable transition is associated with the interval [a,b] where its bad subinterval is [α,b] and a≤α then, the controlled model becomes complicated.Figure 16
Controlled model of Figure1 using stopwatch of [4].


## 6. Illustrative Example

Suppose the multitasking system depicted in Figure17 with the following specifications: four tasks T1,T2,T3, and T4 are being executed. Two tasks T3 and T4 are uncontrollable. The task T1 is periodic with a period of [6,6] and then, its start execution is controllable. Suppose that starting execution of T2 is also controllable. T4 is depended to T2 and T3 meaning that it can be executed only when T2 and T3 are executed. Two tasks T1 and T2 share a common resource. On the other hand, T1 enters through a single capacity buffer. It means that if T1 is not executed by the end of its period, the system will block. In Figure 7, tasks are modeled by tokens and the execution of each task Ti is shown by the transition ti. If T1 is not executed by the end of its period the system enters the state Block, and, t5 is the transition to be avoided. Delay is a place modeling the behavior of the buffer considering the period of the task T1. And finally, T1 executes within [2,2] time units, T2 in [2,3], T3 within [5,6] and T4 in [0,1].Figure 17
A periodic system withTc={t1,t2}.The state class graph of the model is given in Figure18 and Table 2 shows the state class informations. Based on the state class graph of the system, the state classes α4,α8,α13,α14,α18,α20, and α23 are forbidden. Let us briefly trace the algorithm on the state class graph. First, we follow the algorithm on the left branch where the state classes α4,α8, and α13 are located. The algorithm starts from α0 and is executed recursively to α1, then α3, α7 and finally reaches to α13 with a forbidden marking. Then, it comes back to α7 with {t5} and to α3 with {t4t5}. The other successor available from α3 is α8 which is also forbidden. Till now there is no enabled controllable transition to avoid these classes and the algorithm continues returning back to α1 with {t3t4t5,t3t5}. The other successor available from α1 is α4 which is also forbidden. Thus, it returns back to α0 with {t2t3t4t5,t2t3t5,t2t5}. The other successor available from α0 is α2 which is safe and the algorithm continues to α5,α9,α15,α19, and finally α18 which is a forbidden state. Then, it goes back to α19 with {t5} and consequently to α15 with {t2t5}. The other successors available from α15 are the forbidden state α20 and α2 which is already under processing. Note that two enabled controllable transitions are available at α15, but the controller cannot act at this level because t5 may fire before t1 or t2 and lead to a forbidden state. Then, the algorithm continues and returns back to α9 with {t4t2t5,t2t5} where no controllable transition is available. Consequently, the algorithm continues and returns back to α5 and finally reaches to α2 where newly enabled controllable transitions are available. Till now the path to be avoided at α2 includes {t2t3t4t2t5,t2t3t4t5}.Table 2
State classes of the TPN presented at Figure17.
α
0
:
Delay
+
P
1
+
Resource
2
≤
t
2
≤
3,5
≤
t
3
≤
6,2
≤
t
1
≤
2,6
≤
t
5
≤
6
α
1
:
Delay
+
P
1
+
Wait
3
≤
t
3
≤
4,4
≤
t
5
≤
4
α
2
:
Delay
+
P
1
+
Resource
2
≤
t
2
≤
3,3
≤
t
3
≤
4,2
≤
t
1
≤
2,6
≤
t
5
≤
6
α
3
:
Delay
+
P
3
+
Wait
0
≤
t
4
≤
1,0
≤
t
5
≤
1
α
4
:
P
1
+
Wait
+
Block
0
≤
t
3
≤
0
α
5
:
Delay
+
P
1
+
Wait
1
≤
t
3
≤
2,4
≤
t
5
≤
4
α
6
:
Delay
+
P
1
+
Resource
2
≤
t
2
≤
3,1
≤
t
3
≤
2,2
≤
t
1
≤
2,6
≤
t
5
≤
6
α
7
:
Delay
+
Resource
+
P
1
2
≤
t
2
≤
3,5
≤
t
3
≤
6,2
≤
t
1
≤
2,0
≤
t
5
≤
1
α
8
:
P
3
+
Wait
+
Block
0
≤
t
4
≤
1
α
9
:
Delay
+
P
3
+
Wait
0
≤
t
4
≤
1,2
≤
t
5
≤
3
α
10
:
Delay
+
P
1
+
Wait
0
≤
t
3
≤
0,4
≤
t
5
≤
4
α
11
:
Delay
+
Resource
+
P
3
0
≤
t
2
≤
2,0
≤
t
1
≤
1,4
≤
t
5
≤
5,
0
≤
t
2
-
t
1
≤
1
,
-
4
≤
t
2
-
t
5
≤
-
3
,
-
4
≤
t
1
-
t
5
≤
-
4
α
12
:
Delay
+
Resource
+
P
1
2
≤
t
2
≤
3,0
≤
t
3
≤
0,2
≤
t
1
≤
2,6
≤
t
5
≤
6
α
13
:
Resource
+
P
1
+
Block
1
≤
t
2
≤
3,4
≤
t
3
≤
6
,
-
4
≤
t
2
-
t
3
≤
-
2
α
14
:
Resource
+
P
1
+
Block
2
≤
t
2
≤
3,5
≤
t
3
≤
6
α
15
:
Delay
+
Resource
+
P
1
2
≤
t
2
≤
3,5
≤
t
3
≤
6,2
≤
t
1
≤
2,1
≤
t
5
≤
3
α
16
:
Delay
+
P
3
+
Wait
0
≤
t
4
≤
1,4
≤
t
5
≤
4
α
17
:
Delay
+
Resource
+
P
3
2
≤
t
2
≤
3,2
≤
t
1
≤
2,6
≤
t
5
≤
6
α
18
:
P
1
+
Wait
+
Block
2
≤
t
3
≤
4
α
19
:
Delay
+
P
1
+
Wait
3
≤
t
3
≤
4,0
≤
t
5
≤
1
α
20
:
Resource
+
P
1
+
Block
0
≤
t
2
≤
2,3
≤
t
3
≤
5
,
-
4
≤
t
2
-
t
3
≤
-
2
α
21
:
Delay
+
Resource
+
P
1
2
≤
t
2
≤
3,5
≤
t
3
≤
6,2
≤
t
1
≤
2,3
≤
t
5
≤
4
α
22
:
Delay
+
P
1
+
Wait
3
≤
t
3
≤
4,1
≤
t
5
≤
2
α
23
:
P
1
+
Wait
+
Block
1
≤
t
3
≤
3Figure 18
The state class graph of the TPN presented at Figure17.The procedure is similar for the other path available fromα2 including α6 and its successors. The forbidden state reachable through this path is α23 and in order to avoid this forbidden state, the controller can act at α21 with two enabled controllable transitions. So, nothing is returned to α2 from this path. Having a closer look to the state class graph and the output of the algorithm, we conclude that at each state where t1 and t2 are newly enabled and the controller should act (i.e., α0,α2, and α21), the controller should force t1 to fire before t2 (i.e., t2-t1>0). In other words, t2 should not be active at [2,2]. It is sufficient to add an inhibitor hyperarc to deactivate t2 at [2,2]. The controller cannot act at the state class α15 as discussed earlier and has nothing to do at the state class α6 (the permissive controller will act later at the state class α21). Note that a state class like α14 which is reachable through a forbidden state (α8) is not processed by the algorithm as it is supposed to be avoided in the controlled system. The controlled model using inhibitor hyperarcs is given at Figure 19.Figure 19
Controlled model of Figure17 using inhibitor hyperarcs.Our model is now safe. Yet some challenges exist. Look at the state class graph of the model presented at Figure18. In some paths one task is executed frequently while others are still waiting. For example, see the paths leading to α17. Although the system is not blocked, some of the tasks cannot be executed. A good scheduler had better to perform different tasks alternatively. We may want to consider alternation, particular sequences, add a deadline for each task or other possible policies. And finally, we may ask if it is possible to restrict the execution time of a task even if it is in its safe subinterval? Then, while synthesizing a scheduler, we can add more constraints and scheduling policies beyond “safe states.” Further researches are required to answer these questions.


## 7. Conclusion

In this paper, we have extended the approach discussed in [9] to time Petri nets with stopwatch and have suggested to associate the controllable transitions with stopwatch in order to prevent their bad subintervals. We have proposed that in case a controller (like a scheduler) cannot restrict time intervals associated with controllable transitions, the controllable transitions can be suspended in their bad subintervals. Synthesizing a time Petri net associated with stopwatch is complicated and needs some overapproximations. Besides, time Petri nets associated with stopwatch do not preserve the boundedness property. In this paper, we have suggested a more effective alternative. We synthesize a time Petri net without stopwatch and then, equip the controllable transitions with stopwatch where necessary. With this assumption, every controllable transition can be suspended in its bad subinterval and resumed otherwise. Amongst different types of stopwatch, our solution is based on inhibitor hyperarcs.The approach suggested in this paper is particularly useful at design level for preemptive scheduling purposes, managing shared resources and critical sections. This is a good starting point for further researches on scheduling and to calculate automatically a scheduler in a multitasking system. It is interesting to see how the approach can be applied in a more general case with a variable number of tasks and dependencies. Consider different scheduling policies are challenging and are worth to be considered in further studies.



---

*Source: 970487-2013-04-04.xml*