König B, Mika-Michalski C, Schröder L (2020)
Publication Type: Conference contribution
Publication year: 2020
Publisher: Springer
Book Volume: 12094 LNCS
Pages Range: 133-154
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISBN: 9783030572006
DOI: 10.1007/978-3-030-57201-3_8
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.
APA:
König, B., Mika-Michalski, C., & Schröder, L. (2020). Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas. In Daniela Petrisan, Jurriaan Rot (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 133-154). Dublin, IE: Springer.
MLA:
König, Barbara, Christina Mika-Michalski, and Lutz Schröder. "Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas." Proceedings of the 15th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2020, colocated with the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin Ed. Daniela Petrisan, Jurriaan Rot, Springer, 2020. 133-154.
BibTeX: Download