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áš; KŘETÍNSKÝ Mojmír; ŘEHÁK Vojtěch; STREJČEK Jan
• Rok publikování: 2012
• Druh: Článek ve sborníku
• Konference: TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: http://www.springerlink.com/content/nq344x6v62v63336/
• Doi: http://dx.doi.org/10.1007/978-3-642-28756-5_8
• Obor: Informatika
• Klíčová slova: Linear Temporal Logic; Büchi Automata
• Popis: 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čí.

Související projekty

• Vysoce paralelní a distribuované výpočetní systémy
• Verifikace a analýza velmi velkých počítačových systémů
• 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ů
• Formální metody pro analýzu a verifikaci komplexních systémů
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace
• Formální verifikace stochastických systémů s reálným časem
• Centrum excelence - Institut teoretické informatiky
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity