Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas

König B, Mika-Michalski C, Schröder L (2020)

Publication Type: Conference contribution

Publication year: 2020

Journal

Lecture Notes in Computer Science Springer Verlag

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)

Event location: Dublin IE

ISBN: 9783030572006

DOI: 10.1007/978-3-030-57201-3_8

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.

Authors with CRIS profile

Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik)

Related research project(s)

Probabilistische Beschreibungslogik als Fragment der Probabilistischen Logik Erster Stufe (ProbDL) April 1, 2011 - April 1, 2014

Involved external institutions

Universität Duisburg-Essen (UDE) DE Germany (DE)

How to cite

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