Translation of an extended LTL into TBGA in Spot



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.