Explaining Non-bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas - Coalgebraic Methods in Computer Science Access content directly
Conference Papers Year : 2020

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.
Fichier principal
Vignette du fichier
493577_1_En_8_Chapter.pdf (706.17 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03232346 , version 1 (21-05-2021)

Licence

Attribution

Identifiers

Cite

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⟩
27 View
16 Download

Altmetric

Share

Gmail Facebook X LinkedIn More