DEDUCING FAIRNESS PROPERTIES IN UNITY LOGIC - A NEW COMPLETENESS RESULT

We explore the use of UNITY logic in specifying and verifying fairness properties of UNITY and UNITY-like programs whose semantics can be mo deled by weakly fair transition systems. For such programs, strong fai rness properties in the form of ''if p holds infinitely often then q a lso holds infinitely often'', or ''square lozenge p double right arrow square lozenge p'', can be expressed as conditional UNITY properties of the form ''Hypothesis: true --> p Conclusion: true --> q''. We show that UNITY logic is relatively complete for proving such properties; in the process, a simple inference rule is derived. Specification and verification of weak fairness properties are also discussed.