--- res: bibo_abstract: - We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of φ. The slave automaton for G ψ is in charge of recognizing whether FG ψ 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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Javier foaf_name: Esparza, Javier foaf_surname: Esparza - foaf_Person: foaf_givenName: Jan foaf_name: Kretinsky, Jan foaf_surname: Kretinsky foaf_workInfoHomepage: http://www.librecat.org/personId=44CEF464-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-8122-2881 bibo_doi: 10.1007/978-3-319-08867-9_13 bibo_volume: 8559 dct_date: 2014^xs_gYear dct_language: eng dct_publisher: Springer@ dct_title: 'From LTL to deterministic automata: A safraless compositional approach@' ...