Informační systém Masarykovy univerzity 

Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment

česky | in English

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, 15 s. ISBN 978-3-319-02443-1. doi: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 Článek ve sborníku
Obor Informatika
Stát vydavatele Spojené státy americké
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, formela-conference, inear time logic, LTL, translation to deterministic Rabin automata
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: doc. 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 VaVNázev: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Projekty na podporu excelence v základním výzkumu
MUNI/A/0739/2012, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0760/2012, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 15. 12. 2017 16:54

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 15. 12. 2017 16:54, 50. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému