Rabinizer 2: Small Deterministic Automata for LTL\GU

D 2013

Rabinizer 2: Small Deterministic Automata for LTL\GU

KŘETÍNSKÝ, Jan and Ruslan LEDESMA GARZA

Basic information

Original name

Rabinizer 2: Small Deterministic Automata for LTL\GU

Authors

KŘETÍNSKÝ, Jan (203 Czech Republic, guarantor, belonging to the institution) and Ruslan LEDESMA GARZA (484 Mexico)

Edition

Heidelberg Dordrecht London New York, Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, p. 446-450, 5 pp. 2013

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/13:00066204

Organization unit

Faculty of Informatics

ISBN

978-3-319-02443-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-02444-8_32

Keywords in English

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

Abstract

V originále

We present a tool that generates automata for LTL(X,F,G,U) where U does not occur in any G-formula (but F still can). The tool generates deterministic generalized Rabin automata (DGRA) significantly smaller than deterministic Rabin automata (DRA) generated by state-of-the-art tools. For complex properties such as fairness constraints, the difference is in orders of magnitude. DGRA have been recently shown to be as useful in probabilistic model checking as DRA, hence the difference in size directly translates to a speed up of the model checking procedures.

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/0739/2012, interní kód MU

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

Investor: Masaryk University, Category A

MUNI/A/0760/2012, interní kód MU

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

Investor: Masaryk University, Category A

Citovat

KŘETÍNSKÝ, Jan and Ruslan LEDESMA GARZA. Rabinizer 2: Small Deterministic Automata for LTL\GU. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013. Heidelberg Dordrecht London New York: Springer, 2013, p. 446-450. ISBN 978-3-319-02443-1. Available from: https://dx.doi.org/10.1007/978-3-319-02444-8_32.

@inproceedings{1112170,
   author = {Křetínský, Jan and Ledesma Garza, Ruslan},
   address = {Heidelberg Dordrecht London New York},
   booktitle = {Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013},
   doi = {http://dx.doi.org/10.1007/978-3-319-02444-8_32},
   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-02443-1},
   pages = {446-450},
   publisher = {Springer},
   title = {Rabinizer 2: Small Deterministic Automata for LTL\GU},
   year = {2013}
}

TY  - JOUR
ID  - 1112170
AU  - Křetínský, Jan - Ledesma Garza, Ruslan
PY  - 2013
TI  - Rabinizer 2: Small Deterministic Automata for LTL\GU
PB  - Springer
CY  - Heidelberg Dordrecht London New York
SN  - 9783319024431
KW  - linear temporal logic
KW  - automata
KW  - determinism
KW  - synthesis
KW  - probabilistic model checking
N2  - We present a tool that generates automata for LTL(X,F,G,U) where U does not occur in any G-formula (but F still can). The tool generates deterministic generalized Rabin automata (DGRA) significantly smaller than deterministic Rabin automata (DRA) generated by state-of-the-art tools. For complex properties such as fairness constraints, the difference is in orders of magnitude. DGRA have been recently shown to be as useful in probabilistic model checking as DRA, hence the difference in size directly translates to a speed up of the model checking procedures.
ER  -

KŘETÍNSKÝ, Jan and Ruslan LEDESMA GARZA. Rabinizer 2: Small Deterministic Automata for LTL$\backslash$GU. In \textit{Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013}. Heidelberg Dordrecht London New York: Springer, 2013, p.~446-450. ISBN~978-3-319-02443-1. Available from: https://dx.doi.org/10.1007/978-3-319-02444-8\_{}32.

Detailed Information on Publication Record