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

Bisimulation is one of the fundamental concepts of the theory of coalgebras. However, it is difficult to verify whether a relation is a bisimulation. Although some categorical bisimulation proof methods for coalgebras have been proposed, they are not based on specification languages of coalgebras so that they are difficult to be used in practice. In this paper, a specification language based on paths of polynomial functors is proposed to specify polynomial coalgebras. Since bisimulation can be defined by paths, it is easy to transform Sangiorgi's bisimulation proof methods for labeled transition systems to reasoning rules in such a path-based specification language for polynomial coalgebras. The paper defines the notions of progressions and sound functions based on paths, then introduces the notion of faithful contexts for the language and presents a bisimulation-up-to context proof technique for polynomial coalgebras. Several examples are given to illustrate how to make use of the bisimulation proof methods in the language.