Deriving Liveness Goals from Temporal Logic Specifications

✍ Scribed by C. CALEIRO; G. SAAKE; A. SERNADAS

• Publisher: Elsevier Science
• Year: 1996
• Tongue: English
• Weight: 729 KB
• Volume: 22
• Category: Article
• ISSN: 0747-7171
• DOI: 10.1006/jsco.1996.0065

✦ Synopsis

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.