PAIS Lab seminar: Improvements to Translation of LTL Formula to Buchi Automata // O. Kochetova
7.04.2014 - 18:30 - aud. 902Olga 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.
Slides: tbd
Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!
Сервис предназначен только для отправки сообщений об орфографических и пунктуационных ошибках.