Abstract
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.
Supported by the National Natural Science Foundation of China under Grant No. 60673050.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Rutten, J.: Universal coalgebra: A theory of systems. TCS 249(1), 3–80 (2000)
Sangiorgi, D.: On the origins of bisimulation and coinduction. TOPLAS, Articale 15 31(4) (2009)
Sangiorgi, D.: On the bisimulation proof method. Mathematical Structures in Computer Science 8, 447–479 (1998)
Sangiorgi, D., Walker, D.: The pi-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Rothe, J., Tews, H., Jacobs, B.: The coalgebraic class specification language CCSL. Journal of Universal Computer Science 7(2), 175–193 (2001)
Cîrstea, C.: Integrating Observatins and Computations in the Specification of State-based, Dynamical Systems. PhD thesis, University of Oxford (2000)
Kurz, A.: Specifying coalgebras with modal logic. TCS 260(1-2), 119–138 (2001)
Rößiger, M.: From modal logic to terminal coalgebras. TCS 260, 209–228 (2001)
Goldblatt, R.: Equational logic of polynomial coalgebras. In: Balbiani, P., Suzuki, N.-Y., Wolter, F., Zakharyaschev, M. (eds.) Advances in Modal Logic, vol. 4, pp. 149–184. King’s College Publications (2003)
Bonsangue, M., Rutten, J., Silva, A.: Regular expressons for polynomial coalgebras. CWI Report SEN-E0703 (2007)
Bonsangue, M., Rutten, J., Silva, A.: An algebra for Kripke polynomial coalgebras. In: 24th Annual IEEE Symposium on Logic in Computer Science, pp. 49–58. IEEE Press, Los Alamitos (2009)
Jacobs, B.: Towards a duality result in coalgebraic modal logic. ENTCS 33 (2000)
Goldblatt, R.: A calculus of terms for coalgebras of polynomial functors. ENTCS 44, 161–184 (2001)
Rößiger, M.: Languages for coalgebras on datafunctors. ENTCS 19, 39–60 (1999)
Jacobs, B.: The temporal logic of coalgebras via galois algebras. Technical Report CSI-R9906, Computer Science Institution, University of Nijmegen (1999)
Rutten, J.: Elements of stream calculus (an extensive exercise in coinduction). ENTCS 45, 1–66 (2001)
Jacobs, B.: Exercises in coalgebraic specification. In: Backhouse, R., Crole, R., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS, vol. 2297, pp. 237–280. Springer, Heidelberg (2002)
Moss, L.: Coalgebraic logic. APAL 96(1-3), 277–317 (1999)
Jacobs, B.: Many-sorted coalgeraic modal logic: a model-theoretical study. ITA 35(1), 31–59 (2001)
Pattinson, D.: Coalgebraic modal logic: soundness, completeness and decidability of local consequence. TCS 309(1-3), 177–193 (2003)
Lenisa, M.: From set-theoretic coinduction to coalgebraic coinduction: some resuults, some problems. ENTCS 19, 1–21 (1999)
Bartels, F.: Generalised coinduction. Mathematical Structures in Computer Science 13, 321–348 (2003)
Lingyun, L.: An effective coalgebraic bisimulation proof method. ENTCS 164, 105–119 (2006)
Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observations. Book Draft (2005), http://www.cs.ru.nl/~bart
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhou, Xc., Li, Yj., Li, Wj., Qiao, Hy., Shu, Zm. (2010). Bisimulation Proof Methods in a Path-Based Specification Language for Polynomial Coalgebras. In: Ueda, K. (eds) Programming Languages and Systems. APLAS 2010. Lecture Notes in Computer Science, vol 6461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17164-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-17164-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17163-5
Online ISBN: 978-3-642-17164-2
eBook Packages: Computer ScienceComputer Science (R0)