HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Explaining Non-bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas

Abstract : Behavioural equivalences can be characterized via bisimulation, modal logics, and spoiler-duplicator games. In this paper we work in the general setting of coalgebra and focus on generic algorithms for computing the winning strategies of both players in a bisimulation game. The winning strategy of the spoiler (if it exists) is then transformed into a modal formula that distinguishes the given non-bisimilar states. The modalities required for the formula are also synthesized on-the-fly, and we present a recipe for re-coding the formula with different modalities, given by a separating set of predicate liftings. Both the game and the generation of the distinguishing formulas have been implemented in a tool called T-Beg.
Document type :
Conference papers
Complete list of metadata

Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, May 21, 2021 - 2:57:39 PM
Last modification on : Friday, May 21, 2021 - 3:05:11 PM
Long-term archiving on: : Sunday, August 22, 2021 - 6:48:25 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document


Distributed under a Creative Commons Attribution 4.0 International License



Barbara König, Christina Mika-Michalski, Lutz Schröder. Explaining Non-bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas. 15th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2020, Dublin, Ireland. pp.133-154, ⟨10.1007/978-3-030-57201-3_8⟩. ⟨hal-03232346⟩



Record views