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