Efficient Synthesis for Monotone Transition Systems and Directed Safety Specifications

Adnane Saoud (1, 2) , Elena Ivanova (2) , Antoine Girard (2)

1 LSV - Laboratoire Spécification et Vérification [Cachan]
2 L2S - Laboratoire des signaux et systèmes

In this paper, we introduce an efficient algorithm for control policy synthesis for monotone transition systems and lower (upper) safety specifications. For a monotone transition system the sets of states and inputs are equipped with partial orders, moreover, the transitions preserve the ordering on the states. We propose a lazy algorithm that exploits priorities on the states and inputs. To compute the maximal controlled invariant set, only inputs with the lowest priorities are used. Then, starting from the states with the highest priorities, transitions are computed on-the-fly and only when a particular region of the state space needs to be explored. Once this set is computed, controller synthesis is straightforward by exploring different inputs and using their priorities. We prove the completeness of our algorithm w.r.t the classical safety algorithm. Finally, we illustrate the advantages of the proposed approach on a vehicle platooning problem.

Domains: Automatic

Adnane Saoud, Elena Ivanova, Antoine Girard. Efficient Synthesis for Monotone Transition Systems and Directed Safety Specifications. IEEE Conference on Decision and Control, Dec 2019, Nice, France. ⟨10.1109/CDC40024.2019.9029784⟩. ⟨hal-02281945v1⟩