Minimization of automata representing obligation formulae

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.