Simulations and Bisimulations For Coalgebraic Modal Logics

Gorin D, Schröder L (2013)


Publication Language: English

Publication Type: Conference contribution, Original article

Publication year: 2013

Journal

Publisher: Springer-verlag

Edited Volumes: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

City/Town: Berlin

Book Volume: 8089

Pages Range: 253-266

Conference Proceedings Title: 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013

Event location: Warsaw

URI: http://link.springer.com/chapter/10.1007%2F978-3-642-40206-7_19

DOI: 10.1007/978-3-642-40206-7_19

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. © 2013 Springer-Verlag Berlin Heidelberg.

Authors with CRIS profile

Related research project(s)

How to cite

APA:

Gorin, D., & Schröder, L. (2013). Simulations and Bisimulations For Coalgebraic Modal Logics. In 5th Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 (pp. 253-266). Warsaw: Berlin: Springer-verlag.

MLA:

Gorin, Daniel, and Lutz Schröder. "Simulations and Bisimulations For Coalgebraic Modal Logics." Proceedings of the 5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013, Warsaw Berlin: Springer-verlag, 2013. 253-266.

BibTeX: Download