A Compositional Theory of Refinement for Branching Time

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,...

• Type: Conference
• Year: 2003
• Where: CHARME
• Authors: Panagiotis Manolios
• Keywords: Branching Time Framework, CHARME 2003, Hardware, Refinement Maps, Time Framework