# A Compositional Theory of Refinement for Branching Time

Panagiotis Manolios.

*CHARME 2003, the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Method*. © Springer-Verlag

# Abstract

I develop a compositional theory of refinement for the branching
time framework based on stuttering simulation and prove that if
one system refines another, then a refinement map always exists.
The existence of refinement maps in the linear time framework was
studied in an influential paper by Abadi and Lamport. My
interest in proving analogous results for the branching time
framework arises from the observation that in the context of
mechanical verification, branching time has some important
advantages. By setting up the refinement problem in a way that
differs from the Abadi and Lamport approach, I obtain a proof of
the existence of refinement maps (in the branching time
framework) that does not depend on any of the conditions found in
the work of Abadi and Lamport *e.g.*, machine closure, finite
invisible nondeterminism, internal continuity, the use of history
and prophecy variables, etc. A direct consequence is that
refinement maps always exist in the linear time framework,
subject only to the use of prophecy-like variables.

Gzipped Postscript (67K) © Springer-Verlag

PDF (195K) © Springer-Verlag

Postscript (206K) © Springer-Verlag