×

Enhanced coalgebraic bisimulation. (English) Zbl 1380.68300

In the paper under review a systematic study of bisimulation-up-to techniques for coalgebras is presented. This improves, simplifies and extends the bisimulation proof method for a large class of state-based systems, including labelled transition systems, but also stream systems and weighted automata. The proposed approach allows for compositional reasoning about the soundness of enhancements. Applications include the soundness of bisimulation up to bisimilarity, up to equivalence and up to congruence. It can be concluded that this method gives a powerful and modular framework for simplified coinductive proofs of equivalence.
The first studies on bisimulation belong to R. Milner [A calculus of communicating systems. Berlin-Heidelberg-New York: Springer-Verlag (1980; Zbl 0452.68027)] and D. Park [Lect. Notes Comput. Sci. 104, 167–183 (1981; Zbl 0457.68049)]. Then, R. Milner [Theor. Comput. Sci. 25, 267–310 (1983; Zbl 0512.68026)] proposed a bisimulation-up-to technique for modular reasoning about bisimilarity. Many enhancements to the theory of bisimulation-up-to for labelled transition systems were proposed by D. Sangiorgi [Math. Struct. Comput. Sci. 8, No. 5, 447–479 (1998, Zbl 0916.68057)]. The first account of bisimulation-up-to at the level of coalgebras was given by M. Lenisa [in: CMCS ‘99. Proceedings of the 2nd workshop on coalgebraic methods in computer science. Amsterdam: Elsevier. Electronic Paper No. 2 (1999; Zbl 0918.68029)].
A new generalization of bisimulation-up-to to coalgebras was introduced by a subset of the authors in [Lect. Notes Comput. Sci. 7741, 369–381 (2013; Zbl 1303.68088)]. In the present paper, this generalization is taken as a starting point.
In Section 2 the authors recall coalgebras and bisimilations. A coalgebra for a functor \(F: \mathrm{Set}\to \mathrm{Set}\) is a pair \((X,\alpha)\) consisting of a set \(X\) and a function \(\alpha: X\to FX\). A function \(f: X\to Y\) is a homomorphisms between \(F\)-coalgebras \((X,\alpha)\) and \((Y,\beta)\) if \(Ff\circ\alpha= \beta\circ f\). For any relation \(R\subseteq X\times X\), denote by \(\pi_1: R\to X\) and \(\pi_2: R\to X\) the functions defined as \(\pi_1(x,y)=x\) and \(\pi_2(x,y)=y\).
For a coalgebra \(\alpha: X\to FX\) and relations \(R, S\subseteq X\times X\), we say \(R\) progresses to \(S\), denoted \(R \rightarrowtail S\), if there exists \(\gamma: R\to FS\) such that \(\alpha\circ \pi_i= F\pi_i\circ \gamma\) for all \(i\in \{1,2\}\) (Definition 1). A relation \(R\) is called a bisimulation if \(R \rightarrowtail R\).
In Appendix A, the standard notion of bisimulation on different \(F\)-coalgebras is given. Bisimilarity, denoted by \(\sim\), is defined as the largest bisimulation.
For instance, deterministic automata on the alphabet \(A\) can be considered as coalgebras for the functor \(FX= 2\times X^A\) because a deterministic automaton is a pair \((X, \langle o, t \rangle)\) where \(X\) is a set of states and \(\langle o, t \rangle: X \to 2\times X^A\) is a function with two components: \(o\), the output function, takes the values \(o(x)=1\) for final states, and \(o(x)=0\) otherwise; and \(t\), the transition function, returns for each input letter \(a\in A\) the next state. Bisimilarity coincides with the standard notion of language equivalence, which can thus be proved by providing a suitable bisimulation (Example 1).
Labelled transition systems over a set of labels \(A\) are coalgebras for the functor \(FX= {\mathcal P}(A\times X)\). Bisimilarity and bisimulation instantiate to the classical notions by Milner and Park (Example 2).
Other examples are considered: Weighted automata, generalized weighted automata, stream systems over the reals (Examples 3–5).
In Section 3 the bisimulation-up-to is introduced for coalgebras.
Definition 2. Let \((X,\alpha)\) be a coalgebra and \(f: {\mathcal P}(X\times X)\to {\mathcal P}(X\times X)\) be a function on relations. A bisimulation up to \(f\) is a relation \(R\) such that \(R \rightarrowtail f(R)\). We say that \(f\) is sound if \(R\subseteq \sim\) for all \(R\) such that \(R\rightarrowtail f(R)\).
Consider the function \(e\) mapping a relation \(R\) to its equivalence closure \(e(R)\). A bisimulation up to \(e\) is called a bisimulation up to equivalence. Similarly one can define up-to-transitivity and up-to-symmetry.
Example 6 shows that there is a deterministic automaton (Example 1) and a relation that is not a bisimulation, but which is a bisimulation up-to-equivalence.
Up-to-union, up-to-union-and-equivalence, and up-to-bisimilarity bisimulations are introduced for coalgebras. Example 7 is devoted to bisimulation up to \(\sim\)-union and equivalence on a stream system. The function \(b(R)= \sim\circ R\circ \sim\) defines a bisimulation up to \(b\) corresponding to the concept of bisimulation up to bisimilarity, in which derivatives (i.e., the arriving states) do not need to be related directly but may be bisimilar to elements that are. When the state space of a coalgebra carries some kind of algebraic structure it can be considered bisimulation up to context. A \(T\)-algebra for an endofunctor \(T\) is a pair \((X, \beta)\) where \(X\) is a set and \(\beta: TX\to X\) is a function. For a \(T\)-algebra \((X,\beta)\), the contextual closure of a relation \(R\subseteq X\times X\) is defined as \[ c_{\beta}(R)= \{\langle \beta \circ T\pi_1, \beta \circ T\pi_2\rangle \mid t\in TR\}. \] Whenever \(\beta\) is clear from the context we write \(c(R)\). A bisimulation up to \(c\) is called a bisimulation up to context.
In Example 8, the contextual closure \(c(R)\subseteq T_{\Sigma}\times T_{\Sigma}\) is considered, where \(\Sigma\) is a set of operations with associated arities and \(T_{\Sigma}X\) consists of all \(\Sigma\)-terms with variables in \(X\). Example 9 is devoted to bisimulation up to context for weighted automata. Example 10 belongs to J. Rot et al. [Lect. Notes Comput. Sci. 7810, 480–492 (2013; Zbl 1333.68173)]. It is devoted to bisimulation up to context for a deterministic automaton \({\mathcal P}(A^*)\) of all languages with an alphabet \(A\). In Example 11 a bisimulation \(R\) up to congruence for the tropical semiring \(\mathbb T\) is constructed. It is shown that \(R\) is not a bisimulation up to context. In Example 12 a relation \(R\) for a stream system is established. It is shown that \(R\) is a bisimulation up to \(\sim\)-union, context, and equivalence. But \(R\) is not a bisimulation.
Section 4 is devoted to the algebra of enhancements.
Definition 3. Let \(f\) be a function on binary relations.
– A \(b\)-simulation up to \(f\) is a relation \(R\) such that \(R\subseteq b(f(R))\);
– \(f\) is \(b\)-sound if all \(b\)-simulations up to \(f\) are contained in \(b\)-similarity;
– \(f\) is \(b\)-compatible if it is monotone and \(f\circ b\subseteq b\circ f\).
Theorem 1. All \(b\)-compatible functions are \(b\)-sound.
In Section 5 it is shown how to characterize bisimulation and bisimulation-up-to in terms of monotone functions.
Let \((X,\alpha)\) be an \(F\)-coalgebra. An endofunction \(\varphi_{\alpha}\) is defined on \({\mathcal P}(X\times X)\) as follows: \[ \varphi_{\alpha}(R)= \{(x,y) \mid \exists z\in FR ~{\text{s.t.}}~ F(\pi^R_1(z))=\alpha(x) ~\text{and} ~F(\pi^R_2(z))=\alpha(y)\}. \] Instead of \(\varphi_{\alpha}\), one can write \(\varphi\) if it is clear from the context. Example 13 is devoted to \(\varphi_{\alpha}\) for deterministic automata, labelled transition systems, and stream systems.
For any coalgebra \((X,\alpha)\) the function \(\varphi_{\alpha}\) is monotone (Lemma 3). For any relations \(R\), \(S\), the following assertion holds: \(R\subseteq \varphi_{\alpha}(R)\) iff \(R\rightarrowtail S\) (Lemma 4).
Corollary 1. For any coalgebra \((X,\alpha)\): \(R\) is a bisimulation iff \(R\subseteq \varphi_{\alpha}(R)\).
In other words, a \(\varphi\)-simulation is the same as a bisimulation.
Corollary 2. Let \(f: {\mathcal P}(X\times X) \to {\mathcal P}(X\times X)\) be monotone. For any coalgebra \((X,\alpha)\):
1. \(R\subseteq X\times X\) is a bisimulation up to \(f\) iff it is a \(\varphi_{\alpha}\)-simulation up to \(f\);
2. If \(f\) is \(\varphi_{\alpha}\)-compatible (Definition 3), then \(f\) is sound (Definition 2).
In Section 6, compatibility results for the instances of bisimulation-up-to are proved.
Recall that a weak pullback is a commutative square consisting of morphisms \(p_1: P\to X_1\), \(p_2: P\to X_2\), \(f_1: X_1\to X\), \(f_2: X_2\to X\) satisfying the following condition: for any object \(Q\) and morphisms \(q_1: Q\to X_1\), \(q_2: Q\to X_2\) such that \(f_1\circ q_1= f_2\circ q_2\), there exists a morphism \(h: Q\to P\) such that \(p_1\circ h=q_1\) and \(p_2\circ h=q_2\). (If the morphism \(h\) is unique, then we have an ordinary pullback.)
Theorem 2. Let \((X,\alpha)\) be a coalgebra for a functor \(F\). The following functions are \(\varphi_{\alpha}\)-compatible:
1. \(r\) – the reflexive closure;
2. \(s\) – the symmetric closure;
3. \(u_S\) – union with \(S\) (for a bisimulation \(S\));
If \(F\) preserves weak pullbacks, then the following are \(\varphi_{\alpha}\)-compatible:
4. \(t\) – the transitive closure;
5. \(e\) – the equivalence closure;
6. \(b\) – bisimilarity;
7. \(e\circ u_S\) – \(S\)-union and equivalence (for a bisimulation \(S\)).
Bisimulation up to bisimilarity and bisimulation up to equivalence are not sound in general, and consequently not compatible either. This is illustrated by Example 14.
Then the authors recall some fundamental results relating preservation of weak pullbacks to composition of relations (Theorem 3).
Definition 4. Let \(T\), \(F\) be endofunctors on Set.
– An \((F,T)\)-bialgebra is a triple \((X, \beta, \alpha)\) where \(X\) is a set, \((X,\beta)\) is a \(T\)-algebra and \((X,\alpha)\) is an \(F\)-coalgebra.
– Given a natural transformation \(\lambda: TF \Rightarrow FT\) we say \((X, \beta, \alpha)\) is a \(\lambda\)-bialgebra if \(\alpha\circ\beta= F\beta\circ \lambda_X \circ T\alpha\).
Theorem 4. Let \((X, \beta, \alpha)\) be a \(\lambda\)-bialgebra for \(\lambda: TF\Rightarrow FT\). The contextual closure function \(c_{\beta}\) is \(\varphi_{\alpha}\)-compatible. If \(F\) preserves weak pullbacks then the following are \(\varphi\)-compatible as well:
1. \(e\circ c_{\beta}\circ r\) – congruence;
2. \(e\circ c_{\beta}\circ u_S\) – context, reflexivity and bisimilarity;
3. \(b\circ c_{\beta}\circ r\) – context, reflexivity and bisimilarity.
There are examples of bialgebras \((X, \beta, \alpha)\) such that \((X, \beta, \langle \alpha, \mathrm{id}\rangle)\) is a \(\lambda\)-algebra. In such cases one wants to consider bisimulation(-up-to) on the coalgebra \(\alpha\) and not on \(\langle \alpha, \mathrm{id}\rangle\). The theorem gives us \(\varphi_{\langle \alpha,\mathrm{id} \rangle}\)-compatibility of contextual closure \(c_{\beta}\), but it does not provide \(\varphi_{\alpha}\)-compatibility. A counterexample is given in Example 15, invented by D. Pous and D. Sangiorgi [in: Advanced topics in bisimulation and coinduction. Cambridge: Cambridge University Press. 233–289 (2012; Zbl 1285.68111)].
Section 7 contains a similar development of up-to techniques for behavioural equivalence.
For a coalgebra \(\alpha: X \to FX\) and relations \(R, S\subseteq X\times X\), we say \(R\) progresses to \(S\) (with respect to behavioural equivalence), denoted \(R\rightsquigarrow S\), if \(Fq\circ\alpha\circ \pi_1= Fq\circ \alpha\circ \pi_2\), where \(q\) is the quotient map of \(e(S)\) (Definition 5). If \(R\rightsquigarrow R\) then \(R\) is called a behavioural equivalence.
\(R\) is a behavioural equivalence iff the quotient map of \(R\) is a coalgebra homomorphism. The largest behavioural equivalence is denoted by \(\approx\).
Definition 6. If \(R \rightsquigarrow f(R)\) for a function \(f: {\mathcal P}(X\times X)\to {\mathcal P}(X\times X)\) then we say \(R\) is a behavioural equivalence up to \(f\). We say that \(f\) is sound (w.r.t. behavioural equivalence) if \(R\subseteq \approx\) for all \(R\) such that \(R \rightsquigarrow f(R)\).
Then the authors proceed to characterize behavioural equivalence as a fixed point of a monotone function. They define the function \(\psi_{\alpha}: {\mathcal P}(X\times X)\to {\mathcal P}(X\times X)\) as \[ \psi_{\alpha}(R)= \{(x,y) \mid Fq\circ \alpha(x)= Fq\circ \alpha(y)\} \] where \(q: X\to X/e(R)\) is the quotient map of \(e(R)\).
For any coalgebra \((X,\alpha)\) the function \(\psi_{\alpha}\) is monotone (Lemma 5). For any relations \(R, S\subseteq X\times X\) the following property holds: \(R\subseteq \psi(S)\) iff \(R \rightsquigarrow S\) (Lemma 6). Consequently, behavioural equivalence up to any \(\psi\)-compatible function is sound. But, in general, it does not hold that \(\psi(R)\circ \psi(S)\subseteq \psi(R\circ S)\) (Example 16). This motivates to prove the compatibility of the equivalence closure \(e\) directly.
Theorem 5. Let \((X,\alpha)\) be any coalgebra. The following are \(\psi_{\alpha}\)-compatible:
1. \(r\) – the reflexive closure;
2. \(e\) – the equivalence closure;
3. \(u_S\) – union with \(S\) (for a behavioural equivalence \(S\)).
A monad \((T, \mu, \eta)\) consists of an endofunctor \(T\) and natural transformations \(\mu: TT\Rightarrow T\), \(\eta: \mathrm{Id}\to T\) such that \(\mu\circ T\eta= \mathrm{id} = \mu\circ \eta T\) and \(\mu\circ \mu T= \mu\circ T\mu\). A \((T,\mu,\eta)\)-algebra is \(T\)-algebra \((X, \beta)\) such that \(\beta\circ \mu_X= \beta\circ T\beta\). A monad is called finitary if its underlying functor preserves filtered colimits.
Theorem 6. Let \((X, \beta, \alpha)\) be a \(\lambda\)-bialgebra for a distributive law \(\lambda: TF\Rightarrow FT\) (between functors), where \(\beta\) is an algebra for a finitary monad \((T, \eta, \mu)\). The following are \(\psi_{\alpha}\)-compatible:
1. \(c_{\beta}\circ r\) – contextual closure;
2. \(e\circ c_{\beta}\circ r\) – congruence;
3. \(e\circ c_{\beta}\circ r\circ u_S\) – context, \(S\)-union, reflexivity, and equivalence;
4. \(\beta \circ c_{\beta}\circ r\) – context, reflexivity and bisimilarity.
In Example 17 the general process algebra with transitions costs (GPA) from [P. Buchholz and P. Kemper, Lect. Notes Comput. Sci. 2165, 184–199 (2001; Zbl 1007.68130)] is considered. Applications of the obtained theorems are shown for the study of the operational semantics of GPA expressed in terms of weighted transtion systems.
Section 8 contains concluding remarks.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
18B20 Categories of machines, automata
18C15 Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
18C50 Categorical semantics of formal languages
68Q55 Semantics in the theory of computing
68Q70 Algebraic theory of languages and automata
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] AcetoL., FokkinkW. and VerhoefC. (2001). Structural operational semantics. In: Handbook of Process Algebra, Elsevier Science, 197-292.10.1016/B978-044482830-9/50021-7 · Zbl 1062.68074
[2] AczelP. and MendlerN. (1989). A final coalgebra theorem. In: Category Theory and Computer Science, LNCS, volume 389, Springer, 357-365. · Zbl 1496.03206
[3] AdámekJ., KoubekV. and VelebilJ. (2000). A duality between infinitary varieties and algebraic theories. Commentationes Mathematicae Universitatis Carolinae41(3)529-542. · Zbl 1035.08004
[4] BartelsF. (2004). On Generalised Coinduction and Probabilistic Specification Formats. Ph.D. thesis, CWI, Amsterdam.
[5] BerstelJ. and ReutenauerC. (1988). Rational Series and Their Languages, Springer. · Zbl 0668.68005
[6] BloomB., IstrailS. and MeyerA. (1995). Bisimulation can’t be traced. Journal of ACM42(1)232-268.10.1145/200836.200876 · Zbl 0886.68027
[7] BonchiF., BonsangueM., BorealeM., RuttenJ. and SilvaA. (2012). A coalgebraic perspective on linear weighted automata. Information and Computation21177-105.10.1016/j.ic.2011.12.002 · Zbl 1279.68235
[8] BonchiF., PetrisanD., PousD. and RotJ. (2014). Coinduction up-to in a fibrational setting. In: HenzingerT.A. and MillerD. (eds.) CSL-LICS 2014, ACM, 20. · Zbl 1395.68195
[9] BonchiF. and PousD. (2013). Checking NFA equivalence with bisimulations up to congruence. In: GiacobazziR. and CousotR. (eds.) POPL, ACM, 457-468. · Zbl 1301.68169
[10] BonsangueM.M., HansenH.H., KurzA. and RotJ. (2013). Presenting distributive laws. In: HeckelR. and MiliusS. (eds.) CALCO. Lecture Notes in Computer Science8089, Springer, Berlin, 95-109.10.1007/978-3-642-40206-7_9 · Zbl 1394.68238
[11] BuchholzP. and KemperP. (2001). Quantifying the dynamic behavior of process algebras. In: de AlfaroL. and GilmoreS. (eds.) PAPM-PROBMIV. Lecture Notes in Computer Science, Springer, Berlin, 184-199. · Zbl 1007.68130
[12] ConwayJ. (1971). Regular Algebra and Finite Machines, Chapman and Hall. · Zbl 0231.94041
[13] EndrullisJ., HendriksD. and BodinM. (2013). Circular coinduction in Coq using bisimulation-up-to techniques. In: BlazyS., Paulin-MohringC. and PichardieD. (eds.) ITP 2013. LNCS7998, Springer, Berlin, 354-369. · Zbl 1317.68209
[14] GorínD. and SchröderL. (2013). Simulations and bisimulations for coalgebraic modal logics. In: HeckelR. and MiliusS. (eds.) Proceedings of the 5th International Conference on Algebra and Coalgebra in Computer Science (CALCO 2013). Lecture Notes in Computer Science8089, Springer, Berlin, 253-266.10.1007/978-3-642-40206-7_19 · Zbl 1394.68250
[15] GummH. (1999). Elements of the general theory of coalgebras. In: LUATCS 99, Rand Afrikaans University, South Africa.
[16] GummH. and SchröderT. (2000). Coalgebraic structure from weak limit preserving functors. Electronic Notes in Theoretical Computer Science33111-131.10.1016/S1571-0661(05)80346-9 · Zbl 0966.68145
[17] GummH.P. and SchröderT. (2001). Monoid-labeled transition systems. Electronic Notes in Theoretical Computer Science44(1)185-204.10.1016/S1571-0661(04)80908-3 · Zbl 1260.68240
[18] HermidaC. and JacobsB. (1998). Structural induction and coinduction in a fibrational setting. Information and Computation145(2)107-152.10.1006/inco.1998.2725 · Zbl 0941.18006
[19] HopcroftJ. and KarpR. (1971). A linear algorithm for testing equivalence of finite automata. Technical Report114, Cornell Univ.
[20] KlinB. (2009). Structural operational semantics for weighted transition systems. In: PalsbergJ. (eds.) Semantics and Algebraic Specification. Lecture Notes in Computer Science5700, Springer, Berlin, 121-139.10.1007/978-3-642-04164-8_7 · Zbl 1253.68214
[21] KlinB. (2011). Bialgebras for structural operational semantics: An introduction. TCS412(38)5043-5069.10.1016/j.tcs.2011.03.023 · Zbl 1246.68150 · doi:10.1016/j.tcs.2011.03.023
[22] LenisaM. (1999). From set-theoretic coinduction to coalgebraic coinduction: Some results, some problems. ENTCS192-22. · Zbl 0918.68029
[23] LenisaM., PowerJ. and WatanabeH. (2000). Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. ENTCS33230-260. · Zbl 0960.18002
[24] LevyP.B. (2011). Similarity quotients as final coalgebras. In: HofmannM. (eds.) FOSSACS 2011. Lecture Notes in Computer Science6604, Springer, Berlin, 27-41.10.1007/978-3-642-19805-2_3 · Zbl 1326.68193
[25] LuoL. (2006). An effective coalgebraic bisimulation proof method. Electronic Notes in Theoretical Computer Science164(1)105-119.10.1016/j.entcs.2006.06.007 · Zbl 1276.68123 · doi:10.1016/j.entcs.2006.06.007
[26] MartiJ. and VenemaY. (2012). Lax extensions of coalgebra functors. In: PattinsonD. and SchröderL. (eds.) 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2012). Lecture Notes in Computer Science, Springer, Berlin, 7399150-169. · Zbl 1328.03060
[27] MilnerR. (1980). A Calculus of Communicating Systems, Lecture Notes in Computer Science, volume 92, Springer. · Zbl 0452.68027
[28] MilnerR. (1983). Calculi for synchrony and asynchrony. TCS25(3)267-310.10.1016/0304-3975(83)90114-7 · Zbl 0512.68026 · doi:10.1016/0304-3975(83)90114-7
[29] ParkD. (1981). Concurrency and automata on infinite sequences. In: DeussenP. (eds.) Theoretical Computer Science. Lecture Notes in Computer Science104, Springer, Berlin, 167-183.10.1007/BFb0017309 · Zbl 0457.68049
[30] PousD. (2007). Complete lattices and up-to techniques. In: Proceedings of the APLAS. Springer Lecture Notes in Computer Science4807351-366.10.1007/978-3-540-76637-7_24 · Zbl 1138.68041
[31] PousD. and SangiorgiD. (2012). Enhancements of the bisimulation proof method. In: Advanced Topics in Bisimulation and Coinduction, Cambridge University Press, 233-289. · Zbl 1285.68111
[32] RotJ., BonsangueM. and RuttenJ. (2013a). Coalgebraic bisimulation-up-to. In: van Emde BoasP., GroenF., ItalianoG., NawrockiJ. and SackH. (eds.) SOFSEM. Springer Lecture Notes in Computer Science7741369-381.10.1007/978-3-642-35843-2_32 · Zbl 1303.68088
[33] RotJ., BonsangueM. and RuttenJ. (2013b). Coinductive proof techniques for language equivalence. In: DediuA.-H., Martín-VideC. and TrutheB. (eds.) LATA. Lecture Notes in Computer Science7810, Springer, Berlin, 480-49210.1007/978-3-642-37064-9_42 · Zbl 1333.68173
[34] RuttenJ. (1998). Relators and metric bisimulations. ENTCS11252-258. · Zbl 0917.68146
[35] RuttenJ. (2000). Universal coalgebra: A theory of systems. TCS249(1)3-80.10.1016/S0304-3975(00)00056-6 · Zbl 0951.68038 · doi:10.1016/S0304-3975(00)00056-6
[36] RuttenJ. (2003). Behavioural differential equations: A coinductive calculus of streams, automata, and power series. TCS308(1-3)1-53.10.1016/S0304-3975(02)00895-2 · Zbl 1071.68050 · doi:10.1016/S0304-3975(02)00895-2
[37] SalomaaA. and SoittolaM. (1978). Automata-Theoretic Aspects of Formal Power Series, Texts and Monographs on Computer Science, Springer. · Zbl 0377.68039
[38] SangiorgiD. (1998). On the bisimulation proof method. Mathematical Structures in Computer Science8(5)447-479.10.1017/S0960129598002527 · Zbl 0916.68057 · doi:10.1017/S0960129598002527
[39] SangiorgiD. (2012). An introduction to Bisimulation and Coinduction, Cambridge University Press. · Zbl 1252.68008
[40] StatonS. (2011). Relating coalgebraic notions of bisimulation. LMCS7(1). · Zbl 1247.68192
[41] TrnkováV. (1980). General theory of relational automata. Fundamenta Informaticae3(2)189-234. · Zbl 0453.68022
[42] TuriD. and PlotkinG. (1997). Towards a mathematical operational semantics. In: LICS, IEEE Computer Society, 280-291.
[43] WinterJ., BonsangueM.M. and RuttenJ.J.M.M. (2011). Context-free languages, coalgebraically. In: CorradiniA., KlinB. and CîrsteaC. (eds.) CALCO. Lecture Notes in Computer Science6859, Springer, Berlin, 359-376.10.1007/978-3-642-22944-2_25 · Zbl 1344.68152
[44] ZhouX., LiY., LiW., QiaoH. and ShuZ. (2010). Bisimulation proof methods in a path-based specification language for polynomial coalgebras. In: APLAS. Lecture Notes in Computer Science6461, Springer, Berlin, 239-254.10.1007/978-3-642-17164-2_17
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.