An intensional characterization of the largest bisimulation (Q580963)

The notion of observational equivalence in Milner's CCS can be viewed as a limit of finite approximations of \(P=Q\). This limit is however not uniform and is thus perhaps not the intended one. These problems were solved by Park's introduction of the notion of bisimulations. Since the concept of the largest bisimulation is not formulated as a limit, the uniformity `missing' in Milner's observational equivalence is only implicit. In the following note we use proof objects to formulate \(P=Q\) explicitly as a uniform limit of finite approximations, which gives an intensional characterization of the largest bisimulation.