Minimization of automata representing obligation formulae

From LRDE

Revision as of 17:02, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Felix Abecassis | title = Minimization of automata representing obligation formulae | year = 2010 | number = 1004 | abstract = Model checking is a rese...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.