A new translation from LTL into TGBA in Spot
From LRDE
- Authors
- Damien Lefortier
- Type
- techreport
- Year
- 2010
- Number
- 0912
- Projects
- Spot
Abstract
Spot is a model checking library centered around the automata-theoretic approach, and 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 three algorithms to translate LTL formulæ to TGBA, one of the main stages of the approach. We present a forth translation algorithm introduced by Tauriainen which uses TAA (Transition-based Alternating Automata) as an intermediate representation. We also compare it to the three algorithms already present in Spot.