Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
BLAHOUDEK, František, Tomáš BABIAK, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment. In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Berlin Heidelberg: Springer, 2013, s. 24-38. ISBN 978-3-319-02443-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-02444-8_4. |
Další formáty:
BibTeX
LaTeX
RIS
|
Základní údaje | |
---|---|
Originální název | Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment |
Název česky | Efektivní překlad LTL na deterministické Rabinovy automaty |
Autoři | BLAHOUDEK, František (203 Česká republika, domácí), Tomáš BABIAK (703 Slovensko, domácí), Mojmír KŘETÍNSKÝ (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí). |
Vydání | Berlin Heidelberg, 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, od s. 24-38, 15 s. 2013. |
Nakladatel | Springer |
Další údaje | |
---|---|
Originální jazyk | angličtina |
Typ výsledku | Stať ve sborníku |
Obor | 10201 Computer sciences, information science, bioinformatics |
Stát vydavatele | Spojené státy |
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:00066175 |
Organizační jednotka | Fakulta informatiky |
ISBN | 978-3-319-02443-1 |
ISSN | 0302-9743 |
Doi | http://dx.doi.org/10.1007/978-3-319-02444-8_4 |
Klíčová slova anglicky | linear temporal logic; deterministic omega-automata |
Štítky | best, core_A, firank_A, formela-conference, inear time logic, LTL, translation to deterministic Rabin automata |
Příznaky | Mezinárodní význam, Recenzováno |
Změnil | Změnil: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Změněno: 15. 11. 2013 23:58. |
Anotace |
---|
Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to the fragment LTL(F,G). We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae. |
Anotace česky |
---|
Některé aplikace Lineární temporální logiky (LTL) vyžadují překlad formulí této logiky na deterministické omega-automaty. V současnosti existují dva překladače produkující deterministické automaty: ltl2dstar zpracovávající celou logiku LTL a Rabinizer použitelný pouze na fragmentu LTL (F,G). Představujeme nový algoritmus pro překlad LTL formulí na deterministické Rabinovy automaty přes alternující automaty a deterministické zobecněné Rabinovy automaty s akceptující podmínkou na hranách. Náš překlad funguje pro fragment LTL, který je striktně větší než LTL(F,G). Experimentální výsledky ukazují, že náš algoritmus může produkovat podstatně menší automaty v porovnání s Rabinizerem s ltl2dstar, zejména pro složitější LTL formule. |
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 |
VytisknoutZobrazeno: 27. 8. 2024 01:56