From LTL to deterministic automata: A safraless compositional approach

Javier Esparza; Jan Křetínský; Salomon Sickert

doi:10.1007/s10703-016-0259-2

From LTL to deterministic automata: A safraless compositional approach

Javier Esparza
, Jan Křetínský
, Salomon Sickert

Technical University of Munich

Research output: Contribution to journal › Article › peer-review

25 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 co-Büchi automaton for φ and an array of Rabin automata, one for each G-subformula of φ. The Rabin automaton for Gψ is in charge of recognizing whether FGψ holds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.

Original language	English
Pages (from-to)	219-271
Number of pages	53
Journal	Formal Methods in System Design
Volume	49
Issue number	3
DOIs	https://doi.org/10.1007/s10703-016-0259-2
State	Published - 1 Dec 2016

Keywords

Automata theory
Temporal logic
Verification

Access to Document

10.1007/s10703-016-0259-2

Cite this

@article{a20365640885451fa7e05e5735f0fb65,

title = "From LTL to deterministic automata: A safraless compositional approach",

abstract = "We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a co-B{\"u}chi automaton for φ and an array of Rabin automata, one for each G-subformula of φ. The Rabin automaton for Gψ is in charge of recognizing whether FGψ holds. This information is passed to the co-B{\"u}chi automaton that decides on acceptance. As opposed to standard procedures based on Safra{\textquoteright}s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.",

keywords = "Automata theory, Temporal logic, Verification",

author = "Javier Esparza and Jan K{\v r}et{\'i}nsk{\'y} and Salomon Sickert",

note = "Publisher Copyright: {\textcopyright} 2016, Springer Science+Business Media New York.",

year = "2016",

month = dec,

day = "1",

doi = "10.1007/s10703-016-0259-2",

language = "English",

volume = "49",

pages = "219--271",

journal = "Formal Methods in System Design",

issn = "0925-9856",

publisher = "Springer Netherlands",

number = "3",

}

TY - JOUR

T1 - From LTL to deterministic automata

T2 - A safraless compositional approach

AU - Esparza, Javier

AU - Křetínský, Jan

AU - Sickert, Salomon

PY - 2016/12/1

Y1 - 2016/12/1

N2 - We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a co-Büchi automaton for φ and an array of Rabin automata, one for each G-subformula of φ. The Rabin automaton for Gψ is in charge of recognizing whether FGψ holds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.

AB - We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a co-Büchi automaton for φ and an array of Rabin automata, one for each G-subformula of φ. The Rabin automaton for Gψ is in charge of recognizing whether FGψ holds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.

KW - Automata theory

KW - Temporal logic

KW - Verification

UR - https://www.scopus.com/pages/publications/85000956454

U2 - 10.1007/s10703-016-0259-2

DO - 10.1007/s10703-016-0259-2

M3 - Article

AN - SCOPUS:85000956454

SN - 0925-9856

VL - 49

SP - 219

EP - 271

JO - Formal Methods in System Design

JF - Formal Methods in System Design

IS - 3

ER -

From LTL to deterministic automata: A safraless compositional approach

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this