Translation of an extended LTL into TBGA in Spot
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
- 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.