State Refinement in Process Algebra (Extended Abstract)

) Andrew C. Uselton and Scott A. Smolka Department of Computer Science SUNY at Stony Brook Stony Brook, NY 11794-4400, USA fuselton,sasg@cs.sunysb.edu Abstract We introduce a state refinement operator into BPA with recursive specifications and present a comprehensive technical development of the resulting theory, BPA + SR. Our main technical results are that bisimulation is a congruence in BPA+SR and that guarded recursive specifications have unique solutions. We also have that bisimulation remains a congruence if the merge operator of ACP is added to BPA + SR. This is significant since action refinement, another approach to refinement in process algebra, does not in general preserve semantic equivalences based on interleavings of atomic actions. State refinement, to our knowledge, represents the first attempt to capture the essence of Harel's statecharts --- viz., hierarchically structured state transition behavior --- within a purely process algebraic setting. A succinct, hierar..