From LTL to Deterministic Automata: A Safraless Compositional
Approach

D 2014

From LTL to Deterministic Automata: A Safraless Compositional Approach

ESPARZA, Javier a Jan KŘETÍNSKÝ

Základní údaje

Originální název

From LTL to Deterministic Automata: A Safraless Compositional Approach

Autoři

ESPARZA, Javier (724 Španělsko) a Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí)

Vydání

Heidelberg Dordrecht London New York, Computer Aided Verification - 26th International Conference, CAV 2014, od s. 192-208, 17 s. 2014

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/14:00073709

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-08866-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-08867-9_13

Klíčová slova anglicky

linear temporal logic; automata; determinism; synthesis; probabilistic model checking

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 27. 4. 2015 05:43, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GBP202/12/G061, projekt VaV

Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

MUNI/A/0765/2013, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/0855/2013, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

ESPARZA, Javier a Jan KŘETÍNSKÝ. From LTL to Deterministic Automata: A Safraless Compositional Approach. In Computer Aided Verification - 26th International Conference, CAV 2014. Heidelberg Dordrecht London New York: Springer, 2014, s. 192-208. ISBN 978-3-319-08866-2. Dostupné z: https://dx.doi.org/10.1007/978-3-319-08867-9_13.

@inproceedings{1187165,
   author = {Esparza, Javier and Křetínský, Jan},
   address = {Heidelberg Dordrecht London New York},
   booktitle = {Computer Aided Verification - 26th International Conference, CAV 2014},
   doi = {http://dx.doi.org/10.1007/978-3-319-08867-9_13},
   keywords = {linear temporal logic; automata; determinism; synthesis; probabilistic model checking},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Heidelberg Dordrecht London New York},
   isbn = {978-3-319-08866-2},
   pages = {192-208},
   publisher = {Springer},
   title = {From LTL to Deterministic Automata: A Safraless Compositional Approach},
   year = {2014}
}

TY  - JOUR
ID  - 1187165
AU  - Esparza, Javier - Křetínský, Jan
PY  - 2014
TI  - From LTL to Deterministic Automata: A Safraless Compositional Approach
PB  - Springer
CY  - Heidelberg Dordrecht London New York
SN  - 9783319088662
KW  - linear temporal logic
KW  - automata
KW  - determinism
KW  - synthesis
KW  - probabilistic model checking
N2  - 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.
ER  -

ESPARZA, Javier a Jan KŘETÍNSKÝ. From LTL to Deterministic Automata: A Safraless Compositional Approach. In \textit{Computer Aided Verification - 26th International Conference, CAV 2014}. Heidelberg Dordrecht London New York: Springer, 2014, s.~192-208. ISBN~978-3-319-08866-2. Dostupné z: https://dx.doi.org/10.1007/978-3-319-08867-9\_{}13.

Podrobný výpis o publikaci