Automata and temporal logic over arbitrary linear time

Julien Cristau
Linear temporal logic was introduced in order to reason about reactive systems. It is often considered with respect to infinite words, to specify the behaviour of long-running systems. One can consider more general models for linear time, using words indexed by arbitrary linear orderings. We investigate the connections between temporal logic and automata on linear orderings, as introduced by Bruyere and Carton. We provide a doubly exponential procedure to compute from any LTL formula with...