Name
Title | ||
|---|---|---|
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 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. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-57201-3_8 | CMCS |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Barbara König | 1 | 78 | 8.13 |
| Mika-Michalski Christina | 2 | 0 | 0.34 |
| Lutz Schröder | 3 | 597 | 64.16 |