Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis

Andreas Morgenstern
(University Kaiserslautern)
Klaus Schneider
(University Kaiserslautern)

The classic approaches to synthesize a reactive system from a linear temporal logic (LTL) specification first translate the given LTL formula to an equivalent omega-automaton and then compute a winning strategy for the corresponding omega-regular game. To this end, the obtained omega-automata have to be (pseudo)-determinized where typically a variant of Safra's determinization procedure is used. In this paper, we show that this determinization step can be significantly improved for tool implementations by replacing Safra's determinization by simpler determinization procedures. In particular, we exploit (1) the temporal logic hierarchy that corresponds to the well-known automata hierarchy consisting of safety, liveness, Buechi, and co-Buechi automata as well as their boolean closures, (2) the non-confluence property of omega-automata that result from certain translations of LTL formulas, and (3) symbolic implementations of determinization procedures for the Rabin-Scott and the Miyano-Hayashi breakpoint construction. In particular, we present convincing experimental results that demonstrate the practical applicability of our new synthesis procedure.

In Angelo Montanari, Margherita Napoli and Mimmo Parente: Proceedings First Symposium on Games, Automata, Logic, and Formal Verification (GANDALF 2010), Minori (Amalfi Coast), Italy, 17-18th June 2010, Electronic Proceedings in Theoretical Computer Science 25, pp. 89–102.
Published: 9th June 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.25.11 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org