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,
Among various models used to describe the behavior of, Timed Automata (in short) and Time Petri Nets (in short) are the well-known. The properties studied in the TPN and TA for control purposes are classified in two main categories:
Safety properties: Whatever path is traveled, for all situations, a given set of forbidden states (or bad states) are never reached.
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
In this chapter, we discuss an efficient approach to check whether a safety / reachability controller in time Petri nets exists or not . 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  is a Petri net augmented with time intervals associated with transitions. Among the different semantics proposed for time Petri nets , here we focus on the classical one, called intermediate semantics in , in the context of mono-server and strong-semantics .
Formally, a is a tuple where:
In a controllable time Petri net, transitions are partitioned into controllable and uncontrollable transitions, denoted and, respectively (with and). 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, is called bounded if for every reachable marking, there is a bound where holds. In this condition stands for the number of places in.Let be a marking and a transition. Transition is enabled for iff all required tokens for firing are present in, i.e.,. In this case, the firing of leads to the marking defined by: We denote the set of transitions enabled for:
There are two known characterizations for the TPN state. The first one, based on clocks, associates with each transition of the model a to measure the time elapsed since became enabled most recently. The TPN clock state is a couple, where M is a marking and is a clock valuation function,. For a clock state and, is the value of the clock associated with transition. The initial clock state is where, for all. The TPN clock state evolves either by time progression or by firing transitions. When a transition becomes enabled, its clock is initialized to zero. The value of this clock increases synchronously with time until is fired or disabled by the firing of another transition. can fire, if the value of its clock is inside its static firing interval. It must be fired immediately, without any additional delay, when the clock reaches. The firing of a transition takes no time, but may lead to another marking (required tokens disappear while produced ones appear).Let and be two clock states of the TPN model, and. We write, also denoted, iff state is reachable from state after a time progression of time units, i.e.:
We write iff state is immediately reachable from state by firing transition, i.e.:, , , and, , if, 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 .
The TPN state is defined as a pair, where is a marking and is a firing interval function. The initial state is where is the initial marking and, for.Let and be two states of the TPN model, and. The transition relation over states is defined as follows:
The TPN state space is the structure, where is the initial state of the TPN and being the reflexive and transitive closure of the relation defined above) is the set of reachable states of the model.A in the TPN state space, of a state, is a maximal sequence, such that. By convention, for any state, relation holds. The sequence is called the timed trace of. The sequence is called the firing sequence (untimed trace) of. A marking is reachable iff s.t. its marking is. Runs (resp. timed / untimed traces) of the TPN are all runs (resp. timed / untimed traces) of the initial state.
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 .
Several state space abstraction methods have been proposed, in the literature, for time Petri nets like the
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) , 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 combining a marking and a formula which characterizes the clock domains of all states agglomerated in the state zone. In, the clock of each enabled transition for is represented by a variable with the same name. The domain of is convex and has a unique canonical form represented by the pair, where is a DBM of order defined by:, , where represents the value 0. State zones of the ZBG are in relaxed form.
The initial state zone is the pair, where is the initial marking and.
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 , 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 For economy of notation, we use operator even if .
For economy of notation, we use operator even if .
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) . The canonical form of is encoded by the DBM (a square matrix) of order defined by: where () represents a fictitious transition whose delay is always equal to and is the largest value of in the domain of. Its computation is based on the shortest path
The initial state class is, where.Let be a state class and a transition and the set of states defined by:
The state class has a successor by (i.e., iff is enabled in 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.
A formula F is consistent iff there is, at least, one tuple of values that satisfies, at once, all constraints of F.
Replace in each, by ().
Eliminate by substitution and each of transition conflicting with in.
Add constraint, for each transition.
Formally, the SCG of a TPN model is a structure, where is the initial state class, iff and.
The SCG is finite for all bounded TPNs and preserves linear properties . 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.
2.4. A forward method for computing predecessors of state classesLet be a state class and a sequence of transitions firable from. We denote the state class reachable from by firing successively transitions of. We define inductively this set as follows: and.
During the firing of a sequence of transitions from, the same transition may be newly enabled several times. To distinguish between different enabling of the same transition, we denote for the transition (newly) enabled by the transition of the sequence; denotes the transition enabled in. Let with be a sequence of transitions firable from (i.e.,). We denote the largest subclass of (i.e.,) s.t. is firable from all its states, i.e.,
We suppose that the truth value of an empty set of constraints is always .
Initialize with the formula obtained from by renaming all variables in.
Add the following constraints:
Put the resulting formula in canonical form and eliminate all variables such that, rename all variables in.
Note that (i.e., is firable from) iff is feasible in the underlying untimed model and the formula obtained at step 2) above is consistent.
Proof. By step 1) all variables associated with transitions of are renamed (is renamed in). This step allows us to distinguish between delays of transitions enabled in 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). For each transition of the sequence, three blocks of constraints are added. The two first blocks mean that the delay of must be less or equal to the delays of all transitions enabled in (i.e., transitions of and those enabled by () that are maintained continuously enabled at least until firing ). Transitions of that are maintained continuously enabled at least until firing are transitions of which are not in conflict with in, and,..., and not in conflict with in. Similarly, transitions of (with) that are maintained continuously enabled at least until firing are transitions of which are not in conflict with in, and,..., and not in conflict with in. The third block of constraints specifies the firing delays of transitions that are newly enabled by.
Step 3) isolates the largest subclass of such that is firable from all its states.
Initialize with the formula obtained from by renaming all variables in:
Add the firing constraints of before, before and constraints on the firing intervals of transitions enabled by these firings (i.e., and):
Put the resulting formula in canonical form and eliminate all variables such that, rename all variables in:.
The subclass consists of all states of from which the sequence is firable. If is controllable, to avoid reaching the marking by the sequence, it suffices to choose the firing interval of in outside its firing interval in (i.e.,).
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. The sub-zone of, from which the sequence is firable, can be computed in a similar way as the previous procedure where delay constraints are replaced by clock constraints:. To avoid reaching by the sequence the marking, it suffices to delay the firing of until when its clocks overpasses, which means that its firing interval should be.
3. Related work
The theory of control was initially introduced by Ramadge and Wonham in . 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  and time Petri nets , 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 ) 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 , structural as in , semantic as in [10, 11, 20]), and finally the property to be controlled.
In , 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 which prevents to meet the deadline of a transition. A transition is allowed to fire only if its latency (the maximum delay between firing and the next firing of) is not greater than the current deadline of. 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, where is a set of states satisfying the desired property (safe/goal states). The set is defined by :
Intuitively, is the set of predecessors of which will not bring the system out of. Figure 3 clarifies this concept. If the environment can execute an uncontrollable transition after time units, leading the system out of (denoted by), then the controller should be able to execute a controllable action to keep the system in before 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.Let be a safety property and the set of states which satisfy the property (safe states). The fix point of 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 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 be a reachability property and the set of goal states. The least fix point of 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, is a set of abstract states. If is a finite set of abstract states, then the controllable predecessors of is also a finite set of abstract states. The computation of the fix point of 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  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 for a safety property. Consider the TPN given in  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: which means that the number of tokens in the TPN is always. The transition is the only controllable transition and the forbidden markings is determined by. As the state class graph shows, if happens before the right path happens which is safe and the controller has nothing to do. On the other hand, if happens before, two state classes having forbidden markings may be reached ().
To verify whether or not there is a controller for such a property, we compute the fix point of, where is the set of state zones which satisfy the property. Such a controller exists iff the initial state of the model is a winning state (i.e., belongs to the fix point of). The fix point is computed, in iterations, as follows:
Iteration:. In this iteration, all states of and, which are uncontrollable predecessors of bad state classes and are eliminated:
Iteration:. This iteration eliminates from all states, which are uncontrollable predecessors of bad states of:
Iteration:. The fix point is then the set of winning states. Since the initial state zone belongs to, there is a controller for forcing the property. To keep the model in safe states (in states of), the controller must delay, in, the firing of until its clock overpasses the value. Doing so, the successor of by will be.
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  for the case of reachability properties and timed game automata. This algorithm uses three lists containing all state zones explored so far, , containing the set of edges to be processed and indicating, for each state zone, the set of edges to be reevaluated in case the set of the winning states in () is updated. Using this on-the-fly method, in each step, a part of the state zone graph is constructed and an edge of the list is processed. If the state zone is not in and there is, in, some states which satisfy the desired reachability property, then these states are added to the winning states of (). The winning states of will be recomputed later (the edge is added to the list). If is in, the set of the winning states of () is recomputed and possibly those of its predecessors and so on. The set is the largest subset of which is included in the controllable predecessors of the winning states of all its successors.
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 and) by choosing appropriately the firing intervals for controllable transitions.
From the initial state class, there are two elementary paths and that lead to bad states. In both paths, there is only one state class () where the controllable transition is firable. To avoid these bad paths, we propose to compute all states of from which or is firable, i.e., , where:
To avoid these bad states, it suffices to replace in, the firing interval of with. This interval is the complement of in the firing interval of in ().
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 ’’ 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 of a state class is obtained by subtracting from its interval in (), intervals of in its bad subclasses.
Before describing the procedure formally, we define an auxiliary operation over intervals to be used in the algorithm. Let and be two nonempty (real) intervals. We denote intervals defined by:
As an example, for and,. And also
This method is presented in the algorithms 6 and 7. The symbol refers to the set of controllable transitions and all forbidden markings of the net are saved in a set called, bad. The list 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 consists of an initialization step and a calling to the recursive function. The call returns the set of bad sequences that cannot be avoided, from, by restricting firing domains of controllable transitions. If this set is nonempty, it means that such a controller does not exist. Otherwise, it exists and the algorithm guarantees that for each state class with some bad sequences, there is a possibility to choose appropriately the firing intervals of some controllable transitions so as to avoid all bad subclasses of. The control of consists of eliminating, from the firing intervals of such controllable transitions, all parts figuring in its bad subclasses. The restriction of domains is also applied on firing delays between two controllable transitions of. We get in, all possibilities of controlling each state class. In case there is only one controllable transition in, its delay with a fictitious transition whose time variable is fixed at is considered.
Each element of is a triplet where is a state class s.t., is the set of bad sequences of, which cannot be avoided, independently of, from its successors, and gives the intervals of controllable transitions in bad subclasses of (bad intervals). The set allows to retrieve the safe intervals of controllable transitions, by computing the complements, in, of the forbidden intervals (i.e., all possibilities of controlling,).
The function receives parameters being the class under process, the transition leading to and the set of traveled classes in the current path. It uses functions and already explained by equations (5) and (6) (in sections 2.3 and 2.4, respectively). It distinguishes cases:
In other cases, the function is called for each successor of, not already encountered in the current path (see Figure 5), to collect, in, the bad sequences of its successors. Once all successors are processed, is checked:
3.1. If, it means that does not lead to any bad state class or its bad sequences can be avoided later by controlling its successors, then) is added to and the function returns with.
3.2. If, the function determines intervals of controllable transitions in bad subclasses, which do not cover their intervals in. It gets such intervals, identifying states to be avoided, in (bad intervals). It adds to and then verifies whether or not is controllable independently of its predecessor state class in the current path. In such a case, there is no need to start the control before reaching and then the empty set is returned by the function. Otherwise, it is needed to propagate the control to its predecessor by. The set of sequences, obtained by prefixing with sequences of, is then returned by the function.
This algorithm tries to control the system behavior starting from the last to the first state classes of bad paths. If it fails to control a state class of a path, so as to avoid all bad state classes, the algorithm tries to control its previous state classes. If it succeeds to control a state class, there is no need to control its predecessors. The aim is to limit as little as possible the behavior of the system (more permissive controller).4.2. Example
The process starts by calling (see Figure 6). Since is not in and its marking is not forbidden, is successively called for the successors of: and. In of, function is successively called for and. In of, function is called for the successor of by:. For the successor of by (i.e.,), there is no need to call as it belongs to the current path. Since has a forbidden marking, of returns to of with, which, in turn, adds to and returns to of with.In of, function is called for (). This call returns, to of, with, since has a forbidden marking. In of, the tuple is added to and is returned to of. Then, of calls, which in turn calls. Since has only one successor () and this successor belongs to the current path, the call of for adds to and returns to of with, which, in turn, returns to of.
After exploring both successors of, in of, we get in the set of bad paths of. As the state class has a controllable transition, its bad subclasses are computed: and. The firing interval of in () is not covered by the union of intervals of in bad subclasses of (). Then, is added to. As is newly enabled, the empty set is returned to the function, which concludes that a controller exists. According with the list, needs to be controlled (). 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 with. 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, each of them being associated with an interval and conditioned to a marking (see Table 3 and Figure 7).
|Marking||Constraint to be applied on|
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  it is impossible to cancel a transition. Thus, if the entire domain of a controllable transition leads to bad states, as it cannot be canceled or delayed, the state class cannot be controlled so as to avoid bad states.
In the algorithms presented here, a state class is declared to be uncontrollable if it does not contain controllable transitions or it cannot be controlled so as to avoid all bad state classes. Note that if a state class cannot be controlled to avoid all bad classes, it can be however controlled to avoid some bad classes. To limit as little as possible the behavior of the system, the set of bad sequences of a state class can be partitioned in two subsets: the set of bad sequences that can be avoided from and the set of bad sequences that cannot to be avoided from. The former set is avoided from while the latter is let to be controlled by the predecessors of. The function in this case should return the set of bad sequences that cannot be controlled from. In this way, we increase the permissiveness of the controller.
The most significant advantage of this algorithm is the possibility of choosing the level of control. Three levels of control can be carried out:1) Static controller: The control is independent of markings and states of the system. For each controllable transition, the intersection of all safe intervals is considered. Let be a controllable transition whose interval needs to be restricted and. The static firing interval of should be replaced with any interval of. Note that 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 with.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 be a controllable transition whose interval needs to be restricted and. For each marking, the firing interval of each controllable transition enabled in should be any interval of. The set 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 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 stands for the set of markings of goal states.
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.
- For economy of notation, we use operator even if .
- A formula F is consistent iff there is, at least, one tuple of values that satisfies, at once, all constraints of F.
- We suppose that the truth value of an empty set of constraints is always .