Bisimulation proof methods in a path-based specification language for polynomial coalgebras

摘要

What reasoning rules can be used for the deduction of bisimulation formulas in coalgebraicrnspecifications is problematic because those rules used in algebraic specifications possiblyrncannot be applied to bisimulation formulas. Although some categorical bisimulation proofrnmethods for coalgebras have been proposed, they are not based on specification languagesrnof coalgebras so that they cannot be used as reasoning rules. In this paper, a specificationrnlanguage based on paths of polynomial functors is proposed to specify polynomialrncoalgebras. Paths of polynomial functors give detailed observations and transitions on thernstate space of coalgebras so that the techniques used in transition system specifications canrnbe applied to such a path-based language. In particular, because bisimulations can berncharacterized by paths, the notions of progressions, respectful functions and faithful contextsrncan be defined based on paths, and then bisimulation up-to proof techniques, includingrnbisimulation up-to bisimilarities and up-to contexts for transition systems can berntransformed into reasoning rules in the language. Several examples illustrate how to reasonrnsyntactically about bisimulations in the language by using the rules induced by thernbisimulation proof techniques.