Abstract
Simulations serve as a proof tool to compare the behaviour of reactive systems. We define a notion of Λ-simulation for coalgebraic modal logics, parametric in the choice of a set Λ of monotone predicate liftings for a functor T. That is, we obtain a generic notion of simulation that can be flexibly instantiated to a large variety of systems and logics, in particular in settings that semantically go beyond the classical relational setup, such as probabilistic, game-based, or neighbourhood-based systems. We show that this notion is adequate in several ways: i) Λ-simulations preserve truth of positive formulas, ii) for Λ a separating set of monotone predicate liftings, the associated notion of Λ-bisimulation corresponds to T-behavioural equivalence (moreover, this correspondence extends to the respective finite-lookahead counterparts), and iii) Λ-bisimulations remain sound when taken up to difunctional closure. In essence, we arrive at a modular notion of equivalence that, when used with a separating set of monotone predicate liftings, coincides with T-behavioural equivalence regardless of whether T preserves weak pullbacks. That is, for finitary set-based coalgebras, Λ-bisimulation works under strictly more general assumptions than T-bisimulation in the sense of Aczel and Mendler.
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
Barr, M.: Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci. 114, 299–315 (1993)
Enqvist, S.: Homomorphisms of coalgebras from predicate liftings. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 126–140. Springer, Heidelberg (2013)
Hansen, H., Kupke, C.: A coalgebraic perspective on monotone modal logic. In: Coalgebraic Methods in Computer Science (CMCS 2004). ENTCS, vol. 106, pp. 121–143. Elsevier (2004)
Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299–309. Springer, Heidelberg (1980)
Kurz, A., Leal, R.A.: Modalities in the Stone age: A comparison of coalgebraic logics. Theor. Comput. Sci. 430, 88–116 (2012)
Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)
Levy, P.B.: Similarity quotients as final coalgebras. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 27–41. Springer, Heidelberg (2011)
Marti, J., Venema, Y.: Lax extensions of coalgebra functors. In: Pattinson, D., Schröder, L. (eds.) CMCS 2012. LNCS, vol. 7399, pp. 150–169. Springer, Heidelberg (2012)
Pattinson, D.: Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoret. Comput. Sci. 309, 177–193 (2003)
Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Logic 45, 2004 (2002)
Pauly, M.: Bisimulation for general non-normal modal logic (1999) (unpublished Manuscript)
Pauly, M.: Logic for social software. Ph.D. thesis, Universiteit van Amsterdam (2001)
Schröder, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log. 10, 13:1–13:33 (2009)
Schröder, L.: Expressivity of coalgebraic modal logic: The limits and beyond. Theoret. Comput. Sci. 390(2-3), 230–247 (2008)
Schröder, L., Pattinson, D.: Coalgebraic correspondence theory. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 328–342. Springer, Heidelberg (2010)
Sokolova, A.: Probabilistic systems coalgebraically: A survey. Theoret. Comput. Sci. 412, 5095–5110 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gorín, D., Schröder, L. (2013). Simulations and Bisimulations for Coalgebraic Modal Logics. In: Heckel, R., Milius, S. (eds) Algebra and Coalgebra in Computer Science. CALCO 2013. Lecture Notes in Computer Science, vol 8089. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40206-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-40206-7_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40205-0
Online ISBN: 978-3-642-40206-7
eBook Packages: Computer ScienceComputer Science (R0)