A new translation from LTL into TGBA in Spot

From LRDE

Revision as of 17:05, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Damien Lefortier | title = A new translation from LTL into TGBA in Spot | year = 2010 | abstract = Spot is a model checking library centered around the...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.