Deterministic Automata for the (F,G)-fragment of LTL

D 2012

Deterministic Automata for the (F,G)-fragment of LTL

KŘETÍNSKÝ, Jan and Javier ESPARZA

Basic information

Original name

Deterministic Automata for the (F,G)-fragment of LTL

Authors

KŘETÍNSKÝ, Jan (203 Czech Republic, guarantor, belonging to the institution) and Javier ESPARZA (724 Spain)

Edition

Heidelberg Dordrecht London New York, Computer Aided Verification - 24th International Conference, p. 7-22, 16 pp. 2012

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/12:00057483

Organization unit

Faculty of Informatics

ISBN

978-3-642-31423-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-31424-7_7

Keywords in English

linear temporal logic; automata; determinism

Abstract

V originále

When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the formula to a non-deterministic Buchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic omega-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic omega-automata with no determinization procedure involved. Since our approach is tailored to LTL, we often avoid the typically unnecessarily large blowup caused by general determinization algorithms. We investigate the complexity of this translation and provide experimental results and compare them to the traditional method.

Links

GBP202/12/G061, research and development project

Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)

Investor: Czech Science Foundation

MUNI/A/0758/2011, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

MUNI/A/0914/2009, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)

Investor: Masaryk University, Category A

Citovat

KŘETÍNSKÝ, Jan and Javier ESPARZA. Deterministic Automata for the (F,G)-fragment of LTL. In Computer Aided Verification - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2012, p. 7-22. ISBN 978-3-642-31423-0. Available from: https://dx.doi.org/10.1007/978-3-642-31424-7_7.

@inproceedings{987377,
   author = {Křetínský, Jan and Esparza, Javier},
   address = {Heidelberg Dordrecht London New York},
   booktitle = {Computer Aided Verification - 24th International Conference},
   doi = {http://dx.doi.org/10.1007/978-3-642-31424-7_7},
   keywords = {linear temporal logic; automata; determinism},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Heidelberg Dordrecht London New York},
   isbn = {978-3-642-31423-0},
   pages = {7-22},
   publisher = {Springer},
   title = {Deterministic Automata for the (F,G)-fragment of LTL},
   year = {2012}
}

TY  - JOUR
ID  - 987377
AU  - Křetínský, Jan - Esparza, Javier
PY  - 2012
TI  - Deterministic Automata for the (F,G)-fragment of LTL
PB  - Springer
CY  - Heidelberg Dordrecht London New York
SN  - 9783642314230
KW  - linear temporal logic
KW  - automata
KW  - determinism
N2  - When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the formula to a non-deterministic Buchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic omega-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic omega-automata with no determinization procedure involved. Since our approach is tailored to LTL, we often avoid the typically unnecessarily large blowup caused by general determinization algorithms. We investigate the complexity of this translation and provide experimental results and compare them to the traditional method.
ER  -

KŘETÍNSKÝ, Jan and Javier ESPARZA. Deterministic Automata for the (F,G)-fragment of LTL. In \textit{Computer Aided Verification - 24th International Conference}. Heidelberg Dordrecht London New York: Springer, 2012, p.~7-22. ISBN~978-3-642-31423-0. Available from: https://dx.doi.org/10.1007/978-3-642-31424-7\_{}7.

Detailed Information on Publication Record