• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

PAIS Lab seminar: Improvements to Translation of LTL Formula to Buchi Automata // O. Kochetova

7.04.2014 - 18:30 - aud. 902

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.

Slides: tbd


 

Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!