Better Bounded Bisimulation Contractions

Download

• Preprint

Abstract

Bisimulations are standard in modal logic and, more generally, in the theory of state-transition systems. The quotient structure of a Kripke model with respect to the bisimulation relation is called a bisimulation contraction. The bisimulation contraction is a minimal model bisimilar to the original model, and hence, for (image-)finite models, a minimal model modally equivalent to the original. Similar definitions exist for bounded bisimulations ($k$-bisimulations) and bounded bisimulation contractions. Two finite models are $k$-bisimilar if and only if they are modally equivalent up to modal depth $k$. However, the quotient structure with respect to the $k$-bisimulation relation does not guarantee a minimal model preserving modal equivalence to depth $k$. In this paper, we remedy this asymmetry to standard bisimulations and provide a novel definition of bounded contractions called rooted $k$-contractions. We prove that rooted $k$-contractions preserve $k$-bisimilarity and are minimal with this property. Finally, we show that rooted $k$-contractions can be exponentially more succinct than standard $k$-contractions.

Citation

Bolander, T., and Burigana. 2024. “Better Bounded Bisimulation Contractions”, Advances in Modal Logic, AiML 2024, Prague, Czech Republic, August 19-23, 2024, 249–268. https://www.collegepublications.co.uk/aiml/?00012 .

@inproceedings{conf/aiml/BolanderB2024,
    author    = {Thomas Bolander and
                 Alessandro Burigana},
    editor    = {Agata Ciabattoni and
                 David Gabelaia and
                 Igor Sedl{\'{a}}r},
    title     = {Better Bounded Bisimulation Contractions},
    booktitle = {Advances in Modal Logic, AiML 2024, Prague, Czech Republic, August
                 19-23, 2024},
    pages     = {249--268},
    publisher = {College Publications},
    year      = {2024}
}

Related material

• Slides