Proving Boolean Combinations of Deterministic Properties
Bowen Alpern, Fred B. Schneider · 1987
This paper gives a method for providing that a program satisfies a temporal property that has been specified in terms of Buchi automata. The method permits extraction of proof obligations for a property formulated as the Boolean combination of properties, each of which is specified by a deterministic Buchi automaton, directly from the indiviudal automata. The proof obligations can be formulated as Hoare triples. The method is proved sound and relatively complete. A simple example illustrates application of the method.