A Tableau Method for the Realizability and Synthesis of Reactive Safety Specifications

TL;DR

This paper presents a novel tableau decision method for determining the realizability of safety specifications in reactive systems, enabling automatic synthesis of correct systems and extending to richer domains beyond automata-based approaches.

Contribution

Introduces a tableau-based approach for reactive safety specification realizability and synthesis, which can be extended to handle richer domains unlike automata methods.

Findings

Decides realizability of safety LTL specifications.

Allows extraction of correct reactive systems.

Extensible to richer domains like integers.

Abstract

We introduce a tableau decision method for deciding realizability of specifications expressed in a safety fragment of LTL that includes bounded future temporal operators. Tableau decision procedures for temporal and modal logics have been thoroughly studied for satisfiability and for translating temporal formulae into equivalent B\"uchi automata, and also for model checking, where a specification and system are provided. However, to the best of our knowledge no tableau method has been studied for the reactive synthesis problem. Reactive synthesis starts from a specification where propositional variables are split into those controlled by the environment and those controlled by the system, and consists on automatically producing a system that guarantees the specification for all environments. Realizability is the decision problem of whether there is one such system. In this paper we present a method to decide realizability of safety specifications, from which we can also extract (i.e. synthesize) a correct system (in case the specification is realizable). Our method can easily be extended to handle richer domains (integers, etc) and bounds in the temporal operators in ways that automata approaches for synthesis cannot.