Maximally permissive controller synthesis for time Petri nets

Abstract

This article proposes a fully forward on-the-fly algorithm to synthesise safety/reachability controllers for real time systems. Given a time Petri net (TPN) with controllable and uncontrollable transitions and a safety/reachability property, the control consists of limiting the firing intervals of controllable transitions to satisfy the property of interest. This algorithm, based on the state class graph method, computes on-the-fly the reachable state classes of the TPN while collecting progressively firing subintervals to be avoided so that to satisfy the property. It does not need to compute controllable predecessors and then split state classes as it is the case for other approaches based on exploration of state space of the system (backward and forward approaches). Moreover, in the category of state-dependent controllers based on the restriction of firing intervals, the algorithm, proposed here, synthesises maximally permissive controllers.

Keywords:

• controller synthesis
• maximally permissive controllers
• time Petri nets
• on-the-fly algorithm
• safety properties
• reachability properties

Notes

Notes

1. The firing domain of a set of states is the union of the firing domains of its states.

2. For economy of notation, we use operator ≤ even if c = ∞.

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

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

5. A state space abstraction of a given model is sound iff it captures all firing sequences of the model. It is complete iff each firing sequence in the state space abstraction reflects a firing sequence of the model.

6. A timed game automata is a timed automata with two kinds of transitions: controllable and uncontrollable transitions.