From LTL to deterministic automata: A safraless compositional approach

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

40 Scopus citations

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.

Original languageEnglish
Title of host publicationComputer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer Verlag
Pages192-208
Number of pages17
ISBN (Print)9783319088662
DOIs
StatePublished - 2014
Event26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: 18 Jul 201422 Jul 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8559 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
Country/TerritoryAustria
CityVienna
Period18/07/1422/07/14

Fingerprint

Dive into the research topics of 'From LTL to deterministic automata: A safraless compositional approach'. Together they form a unique fingerprint.

Cite this