From LTL to deterministic automata: A safraless compositional approach Conference Paper

Author(s): Esparza, Javier; Křetínský, Jan
Title: From LTL to deterministic automata: A safraless compositional approach
Title Series: LNCS
Affiliation IST Austria
Abstract: We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula \phi. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of \phi. The slave automaton for G\psi is in charge of recognizing whether FG\psi holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.
Keywords: Deterministic automata; Determinization; Logical structure; LTL formulae; Rabin automaton
Conference Title: CAV: Computer Aided Verification
Volume: 8559
Conference Dates: July 18-22, 2014
Conference Location: Vienna, Austria
Publisher: Springer  
Date Published: 2014-01-01
Start Page: 192
End Page: 208
DOI: 10.1007/978-3-319-08867-9_13
Notes: This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM) and by the Austrian Science Fund (FWF) project S11402-N23 (RiSE). The author is on leave from Faculty of Informatics, Masaryk University, Czech Republic, and partially supported by the Czech Science Foundation, grant No. P202/12/G061.
Open access: yes (repository)
IST Austria Authors
Related IST Austria Work