Automata for Formal Methods: Little Steps Towards Perfection /
Jako vhodná reprezentace jazyků nekonečných slov jsou ω-automaty hojně využívány ve formálních metodách. Obzvlášťe algoritmy, které analyzují systémy vykazující nekonečné chování, často spoléhají na ω-automaty. Díky efektivním algoritmům pro průnik, sjednocení a test prázdnosti reprezentovaných jazy...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2018
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/gwriw/ |
| Shrnutí: | Jako vhodná reprezentace jazyků nekonečných slov jsou ω-automaty hojně využívány ve formálních metodách. Obzvlášťe algoritmy, které analyzují systémy vykazující nekonečné chování, často spoléhají na ω-automaty. Díky efektivním algoritmům pro průnik, sjednocení a test prázdnosti reprezentovaných jazyků pro různé třídy ω-automatů jsou tyto automaty vhodné pro metody ověřování modelu se specifikací zadanou pomocí automatu či formule (nejen) logiky LTL. Determinizace a komplementace ω-automatů jsou problémy známé svou komplikovaností. Proto je nasazení metod, které pro své správné fungování vyžadují deterministické automaty (například syntéza reaktivních systémů či ověřování modelu pro systémy s pravděpodobností) nebo komplementují ω-automaty (například analýza terminace v nástroji Ultimate Büchi Automizer), často považované za problematické. Předkládaná dizertace přistupuje k ω-automatům a jejich využití ve formálních metodách z různých směrů a prezentuje hned několik výsledků, které př As ω-automata are a convenient representation of languages of infinite words, they are widespread in the area of formal methods; many algorithms that analyze systems with infinite behaviours rely on ω-automata. The efficient algorithms for the intersection, union, and emptiness checking for various classes of ω-automata made them appealing for model checking of properties expressed as ω-regular languages or as formulae in (not only) Linear Temporal Logic (LTL). On the contrary, determinization and complementation of ω-automata are notoriously difficult problems. This fact complicates usage of the automata-based methods that need deterministic automata (like model checking of probabilistic systems or synthesis of reactive systems) or inherently employ language difference or complementation of ω-automata (like termination analysis in the tool Ultimate Automizer). This dissertation approaches ω-automata and formal methods from various directions and presents several contributions toward |
|---|---|
| Popis jednotky: | Vedoucí práce: Jan Strejček |
| Fyzický popis: | 145 stran : ilustrace |