Translation of an extended LTL into TBGA in Spot

From LRDE

Revision as of 17:05, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Damien Lefortier | title = Translation of an extended LTL into TBGA in Spot | year = 2008 | abstract = Spot is centered around the automata approach to...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

Spot is centered around the automata approach to model checking. The library can be used to verify that every behavior of a model, a transition-based generalized Büchi automata (TGBA), satisfies a given property, expressed using an linear temporal logic (LTL) formula. Spot offers two translation algorithms of LTL into TGBA, one of the two main stages of the approach. We present a new translation into TGBA of a LTL logic which has been extended by adding operators represented by finite automaton. This translation allows Spot to verify properties that were not expressible before.