A Complete, Compositional Proof System for Infinite, Unconditionally FairTransition Systems
Ernie Cohen · 1992
We give a complete UNITY-style proof system for infinite, unconditionally fair transition systems. In contrast to the standard UNITY model (where transitions are deterministic and total and programs are finite), every specification is realized by a ``weakest'''' program. Thus, programs and specifications are interchangeable, and can be freely combined with both infinitary conjunction and infinitary parallel composition.