D 2013

Rabinizer 2: Small Deterministic Automata for LTL\GU

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

Základní údaje

Originální název

Rabinizer 2: Small Deterministic Automata for LTL\GU

Autoři

KŘETÍNSKÝ, Jan (203 Česká republika, garant, domácí) a Ruslan LEDESMA GARZA (484 Mexiko)

Vydání

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

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

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-02443-1

ISSN

DOI

Klíčová slova anglicky

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

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 28. 4. 2014 00:07, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

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/0739/2012, 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/0760/2012, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty