Translation of an extended LTL into TBGA in Spot



Spot is a model checking library centered around the automata approach, which can be used to verify properties expressed using LTL (Linear Temporal Logic) formulæ on models represented as TGBA (Transition-based Generalized Büchi automata). The library offers two translation algorithms from LTL formulæ into TGBA, one of the main stages of the approach. We present an extension of one of these algorithms to an extended LTL where operators are represented by finite automata, allowing Spot to verify properties that were not expressible before. We also present how we could integrate some features of PSL (Property Specification Language) in our extension.