Translation of an extended LTL into TBGA in Spot
From LRDE
- Authors
- Damien Lefortier
- Type
- techreport
- Year
- 2008
- Number
- 0807
- Projects
- Spot
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.