Branching Time Refinement
Brief Announcements, Twenty-Second ACM Symposium on Principles of Distributed Computing (PODC 2003), pages 334-334. ACM Press, July 2003. © ACM, 2003.
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.