Rabinizer 3: Safraless Translation of LTL to Small
Deterministic Automata

D 2014

Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata

KOMÁRKOVÁ, Zuzana a Jan KŘETÍNSKÝ

Základní údaje

Originální název

Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata

Autoři

KOMÁRKOVÁ, Zuzana a Jan KŘETÍNSKÝ

Vydání

Heidelberg Dordrecht London New York, Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, od s. 235-241, 7 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

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/14:00073720

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-11935-9

ISSN

DOI

https://doi.org/10.1007/978-3-319-11936-6_17

EID Scopus

2-s2.0-84908673858

Klíčová slova anglicky

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

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

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

Anotace

V originále

We present a tool for translating LTL formulae into deterministic automata. It is the first tool that covers the whole LTL, while not using Safra's determinization or any of its variants, which leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.

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

KOMÁRKOVÁ, Zuzana a Jan KŘETÍNSKÝ. Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Heidelberg Dordrecht London New York: Springer, 2014, s. 235-241. ISBN 978-3-319-11935-9. Dostupné z: https://doi.org/10.1007/978-3-319-11936-6_17.

@inproceedings{1187948,
   author = {Komárková, Zuzana and Křetínský, Jan},
   address = {Heidelberg Dordrecht London New York},
   booktitle = {Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014},
   doi = {https://doi.org/10.1007/978-3-319-11936-6_17},
   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-11935-9},
   pages = {235-241},
   publisher = {Springer},
   title = {Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata},
   year = {2014}
}

TY  - CONF
ID  - 1187948
AU  - Komárková, Zuzana - Křetínský, Jan
PY  - 2014
TI  - Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
PB  - Springer
CY  - Heidelberg Dordrecht London New York
SN  - 9783319119359
KW  - linear temporal logic
KW  - automata
KW  - determinism
KW  - synthesis
KW  - probabilistic model checking
N2  - We present a tool for translating LTL formulae into deterministic automata. It is the first tool that covers the whole LTL, while not using Safra's determinization or any of its variants, which leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.
ER  -

KOMÁRKOVÁ, Zuzana a Jan KŘETÍNSKÝ. Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. In \textit{Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014}. Heidelberg Dordrecht London New York: Springer, 2014, s.~235-241. ISBN~978-3-319-11935-9. Dostupné z: https://doi.org/10.1007/978-3-319-11936-6\_{}17.

Přehled o publikaci