PAIS Lab seminar: Improvements to Translation of LTL Formula to Buchi Automata // O. Kochetova
Olga Kochetova (HSE Student)
Improvements to Translation of LTL Formula to Buchi Automata
Linear Temporal Logic (LTL) is a standard formalism for description of temporal properties of systems. LTL is mainly used as a specification formalism, typically in the context of model checking or control synthesis. Algorithms taking an LTL formula as input usually translate the formula (or its negation) to an equivalent Buchi automaton (BA) and subsequently work with that automaton.
In this talk I will describe how to translate LTL to formula to BA and what impovements to this translation were recently introduced.
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!