A tableau method for the realizability and synthesis of reactive safety specifications

Abstract

Reactive systems are systems that continuously interact with the environment. In general, as they are critical systems, a failure or malfunction can result in serious consequences, such as loss of human lives or large economic investments. Therefore, correctly modeling the behavior and verification of the system is crucial and, for this, Linear-time Temporal Logic (LTL) and Realizabilty and Synthesis problem represent a promising approach for obtaining confidence in the correctness of a reactive system. The Realizability and Synthesis problem decides if there is a model that satisfies the given specification under all possible environmental behaviours. Moreover, it can be seen as a game between two players; the player who controls the inputs of the system to be synthesized (environment player) and the player who controls the outputs and tries to satisfy the specification for each environmental behaviour (system player).

In this Master thesis, we present both a tableau decision method for deciding the realizability of specifications expressed in a safety fragment of LTL and a prototype that builds a Realizability Tableau from a safety specification input. The prototype returns an open tableau (meaning the specification is realizable) or a closed tableau (when the specification is unrealizable). Finally, we present the future of the work and some of the improvements that will be implemented.