Deriving Liveness Goals from Temporal Logic Specifications

A propositional temporal logic is briefly introduced and its use for reactive systems specification is motivated and illustrated. G-automata are proposed as a new operational semantics domain designed to cope with fairness/liveness properties. G-automata are a class of labelled transition systems with an additional structure of goal achievement which forces the eventual fulfilment of every pending goal. An algorithm is then presented, that takes a finite system specification as input and that, by a stepwise tableaux analysis method, builds up a canonical G-automaton matching the specification. Eventuality formulae correspond to goals of the automaton their satisfaction being thus assured. The direct execution of G-automata, and consequently of specifications, is then discussed and suggested as an alternative approach to the execution of propositional temporal logic. A short overview of the advantages of applying the techniques to the specific field of database monitoring is presented.