Informační systém Masarykovy univerzity 

LTL to Büchi Automata Translation: Fast and More Deterministic

česky | in English

BABIAK, Tomáš, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. LTL to Büchi Automata Translation: Fast and More Deterministic. In Cormac Flanagan, Barbara König. TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2012. s. 95-109, 15 s. ISBN 978-3-642-28755-8. doi:10.1007/978-3-642-28756-5_8.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název LTL to Büchi Automata Translation: Fast and More Deterministic
Název česky Překlad LTL na Büchiho automaty: rychle a determinističtěji
Autoři BABIAK, Tomáš (203 Česká republika, garant, domácí), Mojmír KŘETÍNSKÝ (203 Česká republika, domácí), Vojtěch ŘEHÁK (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, domácí).
Vydání Berlin, Heidelberg, TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, od s. 95-109, 15 s. 2012.
Nakladatel Springer-Verlag
Další údaje
Originální jazyk angličtina
Typ výsledku Článek ve sborníku
Obor Informatika
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Forma vydání paměťový nosič (CD, DVD, flash disk)
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/12:00057222
Organizační jednotka Fakulta informatiky
ISBN 978-3-642-28755-8
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-642-28756-5_8
Klíčová slova česky Lineární temporální logika; Büchiho automaty
Klíčová slova anglicky Linear Temporal Logic; Büchi Automata
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 9. 4. 2013 18:14.
Anotace
We introduce improvements in the algorithm by Gastin and Oddoux translating LTL formulae into Büchi automata via very weak alternating co-Büchi automata and generalized Büchi automata. Several improvements are based on specific properties of any formula where each branch of its syntax tree contains at least one eventually operator and at least one always operator. These changes usually result in faster translations and smaller automata. Other improvements reduce non-determinism in the produced automata. In fact, we modified all the steps of the original algorithm and its implementation known as LTL2BA. Experimental results show that our modifications are real improvements. Their implementations within an LTL2BA translation made LTL2BA very competitive with the current version of SPOT, sometimes outperforming it substantially.
Anotace česky
Představujeme vylepšení algoritmu Gastina a Oddouxe pro překlad LTL formulí na Büchiho automaty pomocí velmi slabých alternujících co-Büchiho automatů a zobecněných Büchiho automatů. Několik vylepšení je založeno na specifických vlastnostech formulí, kde každá cesta syntaktickým stromem obsahuje alespoň jeden operátor "eventually" a alespoň jeden operátor "always". Tato vylepšení vedou k rychlejšímu překladu a menším automatům. Další vylepšení redukují nedeterminismus produkovaných automatů. Ve skutečnosti modifikujeme všechno kroky původního algoritmu a jeho implementace známé pod názvem LTL2BA. Experimentální výsledky ukazují, že naše modifikace jsou vskutku vylepšeními. Díky nim se LTL2BA stává opět srovnatelným se současnou verzí překladače SPOT, někdy ho dokonce výrazně předčí.
Návaznosti
GAP202/10/1469, projekt VaVNázev: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Grantová agentura ČR, Standardní projekty
GA201/09/1389, projekt VaVNázev: Verifikace a analýza velmi velkých počítačových systémů
Investor: Grantová agentura ČR, Standardní projekty
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
GD102/09/H042, projekt VaVNázev: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
Investor: Grantová agentura ČR, Doktorské granty
GPP202/12/P612, projekt VaVNázev: Formální verifikace stochastických systémů s reálným časem (Akronym: Formální verifikace stochastických systémů s reáln)
Investor: Grantová agentura ČR, Postdoktorské projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
MUNI/A/0758/2011, 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/0914/2009, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 13. 12. 2017 18:04

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 13. 12. 2017 18:04, 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