Linear Temporal Logic and Buchi Automata

We have seen how automata, in particular Buchi automata, may be used to describe the behaviors of a concurrent system. Buchi automata “localize” temporal dependency between occurrences of events (represented by propositions) to relations between states and tend to be of lower level. We will study an alternative formalism, namely linear temporal logic. Temporal logic formulae describe temporal dependency without explicit references to time points and are in general more abstract.