Translation of Linear Temporal Logic to Omega-Automata - Babiak, Tomáš (2017)
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