Abstract of Paper

LTL with past and two-way very-weak alternating automata
by Paul Gastin and Denis Oddoux

Abstract:

It is crucial for a model checker using LTL as a specification 
language to have very efficient translation of LTL formulas to B\"{u}uchi 
automata. Most such algorithms are based on a tableau construction. Recently, 
an implementation using very-weak alternating automata as an 
intermediary step proved to be dramatically faster than previous implementations 
based on the tableau construction. In this paper, we want to 
generalize this method to PLTL (LTL with past modalities). For this, we 
study two-way very-weak alternating automata (2VWAA). Our main result is an 
efficient translation of 2VWAA to generalized B\"{u}chi automata 
(GBA). Since we can easily transform a PLTL formula to an equivalent 
2VWAA, this algorithm allows to use PLTL specifications with classical 
model checkers such as SPIN.