Branching Time Refinement

---

Panagiotis Manolios.
Brief Announcements, Twenty-Second ACM Symposium on Principles of Distributed Computing (PODC 2003), pages 334-334. ACM Press, July 2003. © ACM, 2003.

Abstract

I develop notions of refinement for branching time and prove that refinement maps always exist. Reasoning about reactive, distributed, and concurrent, systems often requires relating a concrete system (the implementation) to an abstract system (the specification). This involves the comparison of systems at different levels of abstraction, where a single step of the abstract system may correspond to several steps of the concrete system. The notions of correctness I consider are stuttering bisimulation, introduced by Browne, Clarke, and Grumberg, and stuttering simulation, a weaker variant. I prove a theorem analogous to the well-known theorem on the existence of refinement mappings by Abadi and Lamport, except that it is about refinement in branching time, not linear time, and none of the side conditions required by Abadi and Lamport, including machine closure, finite invisible nondeterminism, internally continuity, etc., are required. I develop the theory of branching time refinement in ways that prove useful for mechanical verification.


Gzipped Postscript (23K) © ACM.
PDF (67K) © ACM.
Postscript (52K) © ACM.