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

Logo poskytovatele
Logo poskytovatele
Logo poskytovatele
Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
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

Citace
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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.