Towards an efficient implementation of a tableau method for reactive safety specifications (Q6643466)

The paper is interested in model checking a fragment of linear-time temporal logic. To this end the authors develop a tableau system based on a new normal form for logical formulas. They consider synthesis and realizability properties. In a tableau we must develop both Boolean connectives and modalities. Usually, tableaux address the satisfiability problem for a formula. The tableau is seen as a game between the system and the environment. The terse normal form is designed to work well in this game. Realizability of a formula means that the system has a winning strategy in the game. Realizability is more complex than usual satisfiability for linear-time temporal logic: we have 2-EXPTIME completeness versus PSPACE completeness. However, the emphasis is on safety formulas, since safety is a behavior useful in practice (nothing bad can happen). The work is relevant for robotics specifications.