Translation of Linear Temporal Logic to Omega-Automata /
Překlad logiky lineárního času (Linear Temporal Logic - LTL) na různé typy ɷ-automatů je intenzivně studovaná oblast, která má mnoho aplikací. Metoda LTL ověřovaní modelu (LTL model checking) je rozšířená a plně automatizovaná technika, která se používá k ověření, zda daný systém splňuje požadovanou...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2017
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/143254/fi_d/ |
| Shrnutí: | Překlad logiky lineárního času (Linear Temporal Logic - LTL) na různé typy ɷ-automatů je intenzivně studovaná oblast, která má mnoho aplikací. Metoda LTL ověřovaní modelu (LTL model checking) je rozšířená a plně automatizovaná technika, která se používá k ověření, zda daný systém splňuje požadovanou specifikaci. Jedním z klíčových kroků je překlad logiky LTL na Büchiho automaty. Různé vlastnosti, jako velikost a determinismus použitého automatu, mohou mít velký vliv na celkový výkon a průběh metody ověřování modelu. Jiné typy automatů, například deterministické Rabinovy automaty, se používají při ověřování modelu pravděpodobnostních systémů. Překlad LTL na ɷ-automaty má kromě metody ověřovaní modelu využití i v jiných oblastech jako jsou kontrola správnosti (sanity checking), detekce prázdnosti (vacuity detection), syntéza kontrolérů (controller synthesis) a syntéza reaktivních modulů (synthesis of reactive modules). Zlepšení různých překladů LTL na ɷ-automaty se v minulosti věnovalo Translation of Linear Temporal Logic (LTL) into ɷ-automata of various types is a heavily studied area with wide range of applications. The translation of LTL formulae into Büchi automata represents one of the crucial steps for LTL model checking, a wide-spread fully-automated technique used to verify whether a given system satisfies a desired specification. Properties, such as size and determinism, of a produced automaton can have a significant impact on the overall performance of the model checking procedure. Other types of automata, such as deterministic Rabin automata, are employed in the context of model checking of probabilistic systems. Besides model checking, the LTL to ɷ-automata translation has its utilization also in areas like sanity checking, vacuity detection, controller synthesis, and synthesis of reactive modules. Much effort was already devoted to improve various LTL to ɷ-automata translations, however, there is still some space for further improvements and tuning. In |
|---|---|
| Popis jednotky: | Vedoucí práce: Mojmír Křetínský |
| Fyzický popis: | vii, 152 stran |