We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data objects. Compared to the original cones and foci method from Groote and Springintveld cite{GroSpr01}, our method is more generally applicable, and does not require a preprocessing step to eliminate $ au$-loops. We prove soundness of our approach and give an application.

Requirements/Specifications (acm D.2.1), Network Protocols (acm C.2.2)
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (msc 68N30), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)
Software (theme 1)
CWI
Software Engineering [SEN]
Software Analysis and Transformation

Fokkink, W.J, & Pang, J. (2002). Cones and foci for protocol verification revisited. Software Engineering [SEN]. CWI.