DERIVING LIVENESS GOALS FROM TEMPORAL LOGIC SPECIFICATIONS

A propositional temporal logic is briefly introduced and its use for r eactive systems specification is motivated and illustrated. G-automata are proposed as a new operational semantics domain designed to cope w ith fairness/liveness properties. G-automata are a class of labelled t ransition systems with an additional structure of goal achievement whi ch forces the eventual fulfilment of every pending goal. An algorithm is then presented, that takes a finite system specification as input a nd that, by a stepwise tableaux analysis method, builds up a canonical G-automaton matching the specification. Eventuality formulae correspo nd to goals of the automaton their satisfaction being thus assured. Th e direct execution of G-automata, and consequently of specifications, is then discussed and suggested as an alternative approach to the exec ution of propositional temporal logic. A short overview of the advanta ges of applying the techniques to the specific field of database monit oring is presented. (C) 1996 Academic Press Limited.