Minimization of automata representing obligation formulae
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- Authors
- Felix Abecassis
- Type
- techreport
- Year
- 2010
- Number
- 1004
Abstract
Model checking is a research field addressing the automatic verification of the correctness of finite-state systems towards a specification. Spot is a model checking library based on an automata approach: the system is translated into a transition-based generalized Büchi automaton, the specifications are expressed as linear temporal logic (LTL) formulae and then translated into a Büchi automaton. LTL formulae can be classified into a hierarchy depending on the type of property they express. We will study the case of LTL formulae representing obligation properties. These can be recognized by a restricted class of automata which have a computable canonical minimal form.