Published in Volume XIX, 2009, pages 93-144

Authors: A. Sokolova, E. de Vink, and H. Woracek

Abstract

We propose a coalgebraic definition of weak bisimulation for classes of coalgebras obtained from bifunctors in the category Set. Weak bisimilarity for a system is obtained as strong bisimilarity of a transformed system. The particular transformation consists of two steps: First, the behavior on actions is lifted to behavior on finite words. Second, the behavior on finite words is taken modulo the hiding of internal or invisible actions, yielding behavior on equivalence classes of words closed under silent steps. The coalgebraic definition is validated by two correspondence results: one for the classical notion of weak bisimulation of Milner, another for the notion of weak bisimulation for generative probabilistic transition systems as advocated by Baier and Hermanns.

Full Text (PDF)

References

[1] P. Aczel and N. Mendler. A final coalgebra theorem. In D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, and A. Poign´e, editors, Proc. CTCS’89, pages 357-365. LNCS 389, 1989.

[2] A. Aldini. Probabilistic information flow in a process algebra. In K.G. Larsen and M. Nielsen, editors, Proc. CONCUR’01, pages 152-168. LNCS 2154, 2001.

[3] S. Andova, J.C.M. Baeten, and T.A.C. Willemse. A complete axiomatization of branching bisimulation for probabilistic systems with an application in protocol verification. In C. Baier and H. Hermanns, editors, Proc. CONCUR’06, pages 327-342. LNCS 4137, 2006.

[4] S. Andova and T.A.C. Willemse. Equivalences for silent transitions in probabilistic systems. In Proc. EXPRESS’04, pages 53-66. ENTCS 128(2), 2005.

[5] S. Andova and T.A.C. Willemse. Branching bisimulation for probabilistic systems: characteristics and decidability. Theoretical Computer Science, 356:325-355, 2006.

[6] C. Baier. On Algorithmic Verification Methods for Probabilistic Systems. Habilitationsschrift, FMI, Universit¨at Mannheim, 1998.

[7] C. Baier and H. Hermanns. Weak bisimulation for fully probabilistic processes. In O. Grumberg, editor, Proc. CAV’97, pages 119-130. LNCS 1254, 1997.

[8] C. Baier and H. Hermanns. Weak bisimulation for fully probabilistic processes. Technical Report TR-CTIT-12, Twente University, 1999.

[9] C. Baier, J.-P. Katoen, H. Hermanns, and V. Wolf. Comparative branching-time semantics for Markov chains. Information and Computation, 200:149-214, 2005.

[10] F. Bartels, A. Sokolova, and E. de Vink. A hierarchy of probabilistic system types. In H. Peter Gumm, editor, Proc. CMCS’03. ENTCS 82(1), 2003.

[11] F. Bartels, A. Sokolova, and E. de Vink. A hierarchy of probabilistic system types. Theoretical Computer Science, 327:3-22, 2004.

[12] F. Borceux. Handbook of Categorial Algebra, volume 1. Cambridge University Press, 1994.

[13] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In G. Plotkin, editor, Proc. LICS’02, pages 413-422. IEEE, 2002.

[14] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Weak bisimulation is sound and complete for PCTL. In L. Brim, P. Jancar, M. Ketınsky, and A. Kuera, editors, Proc. CONCUR’02, pages 355- 370. LNCS 2421, 2002.

[15] M. Fiore, G.L. Cattani, and G. Winskel. Weak bisimulation and open maps. In Proc. LICS’99, Trento, pages 67-76. IEEE, 1999.

[16] R.J. van Glabbeek, S. A. Smolka, B. Steffen, and C. M. N. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proc. LICS’90, Philadelphia, pages 130-141. IEEE, 1990.

[17] R.J. van Glabbeek, S.A. Smolka, and B. Steffen. Reactive, generative, and stratified models of probabilistic processes. Information and Computation, 121:59-80, 1995.

[18] H. Peter Gumm. Functors for coalgebras. Algebra Universalis, 45:135- 147, 2001.

[19] H.P. Gumm. Elements of the general theory of coalgebras. Technical Report LUATS’99, Rand Afrikaans University, 1999.

[20] H. A. Hansson. Time and Probability in Formal Design of Distributed Systems. PhD thesis, Uppsala Universitet, 1991.

[21] B.P.F. Jacobs and J.J.M.M. Rutten. A tutorial on (co)algebras and (co)induction. Bulletin of the EATCS, 62:222-259, 1996.

[22] R.M. Keller. Formal verification of parallel programs. Communications of the ACM, 19:371-384, 1976.

[23] R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Weak bisimulation for probabilistic timed automata and applications to security. In Proc. SEFM’03, Brisbane, pages 34-43. IEEE, 2003.

[24] K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94:1-28, 1991.

[25] N. Lopez and M. Nunez. Weak stochastic bisimulation for nonMarkovian processes. In Dang Van Hung and M. Wirsing, editors, Proc. ICTAC’05, pages 454-468. LNCS 3722, 2005.

[26] S. MacLane. Categories for the working mathematician. SpringerVerlag, 1971.

[27] J. Markovski and N. Trˇcka. Lumping Markov chains with silent steps. In Proc. QEST’06, Riverside, pages 221-232. IEEE, 2006.

[28] R. Milner. A Calculus of Communicating Systems. LNCS 92, 1980.

[29] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

[30] R. Milner. Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 1201-1242. Elsevier and MIT Press, 1990.

[31] L.S. Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96:277- 317, 1999.

[32] A. Philippou, I. Lee, and O. Sokolsky. Weak bisimulation for probabilistic systems. In C. Palamidessi, editor, Proc. CONCUR 2000, pages 334-349. LNCS 1877, 2000.

[33] G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

[34] A. Popescu. Weak bisimilarity coalgebraically. In A. Kurz, M. Lenisa, and A. Tarlecki, editors, Proc. CALCO’09, pages 157-172. LNCS 5728, 2009.

[35] J. Rothe. A syntactical approach to weak (bi)-simulation for coalgebras. In L.S. Moss, editor, Proc. CMCS’02. pp. 270-285, ENTCS 65, 2002.

[36] J. Rothe and D. Masulovi´c. Towards weak bisimulation for coalgebras. In A. Kurz, editor, Proc. Categorical Methods for Concurrency, Interaction and Mobility. pp. 32-46, ENTCS 68, 2002.

[37] J.J.M.M. Rutten. A note on coinduction and weak bisimilarity for while programs. Theoretical Informatics and Applications (RAIRO), 33:393-400, 1999.

[38] J.J.M.M. Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249:3-80, 2000.

[39] R. Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT, 1995.

[40] R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. In B. Jonsson and J. Parrow, editors, Proc. CONCUR’94, pages 481-496. LNCS 836, 1994.

[41] G. Smith. Probabilistic noninterference through weak probabilistic bisimulation. In Proc. CSFW’03, Pacific Grove, pages 3-13. IEEE, 2003.

[42] A. Sokolova. Coalgebraic Analysis of Probabilistic Systems. PhD thesis, TU Eindhoven, 2005.

[43] A. Sokolova and E. de Vink. Probabilistic automata: system types, parallel composition and comparison. In C. Baier, B.R. Haverkort, H. Hermanns, J.-P. Katoen, and M. Siegle, editors, Validation of Stochastic Systems: A Guide to Current Research, pages 1-43. LNCS 2925, 2004.

[44] A. Sokolova, E. de Vink, and H. Woracek. A companion to coalgebraic weak bisimulation for action-type systems. Technical Report CSR 07- 12, TU Eindhoven, 2007. 64pp.

[45] M.I.A. Stoelinga. Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, Radboud Universiteit Nijmegen, 2002.

[46] E. de Vink and J.J.M.M. Rutten. Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoretical Computer Science, 221:271-293, 1999.

[47] A.C. Zaanen. An Introduction to the Theory of Integration. NorthHolland, 1958.

Bibtex

@article{sacscuza:sokolova2009cwbfas,
  title={Coalgebraic Weak Bisimulation for Action-Type Systems},
  author={A. Sokolova and E. de Vink and H. Woracek},
  journal={Scientific Annals of Computer Science},
  volume={19},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2009},
  pages={93--144 },
  publisher={``A.I. Cuza'' University Press}
}