Better Bounded Bisimulation Contractions (Preprint)

TL;DR

This work addresses the asymmetry between standard $k$-contractions and full bisimulations by introducing rooted $k$-contractions, which preserve $k$-bisimilarity while achieving world-minimality. The authors define rooted contractions using bounds $b(w)=k-d(w)$ and maximal representatives, proving they are $k$-bisimilar and world-minimal; they further refine the construction to achieve edge-minimality via least $h$-representatives. The key contributions include formal definitions, proofs of $k$-bisimilarity and world- and edge-minimality, and an exponential succinctness result showing rooted contractions can be exponentially smaller than standard contractions. These results have potential impact on bounded-depth reasoning contexts, such as bounded epistemic planning, by enabling compact yet exact reductions of Kripke models. The paper thus strengthens model reduction techniques while preserving precise bounded modal equivalences.

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.

Figures (6)

• Figure 1: Standard (${\lfloor \mathcal{M} \rfloor}_{k}$) and rooted (${\llfloor \mathcal{M} \rrfloor}_{k}^{}$) $k$-contractions of chain $\mathcal{M}$ (symbol ${\llfloor \mathcal{M} \rrfloor}_{k}^{}$ is borrowed from Definition \ref{['def:rooted-k-contr-1']}). Each world $w$ is denoted by a bullet labeled by its name, followed by the atomic propositions that hold in $w$. An arrow labeled with $i$ from $w$ to $v$ means that $w R_i v$. We omit the labels on arrows whenever $|\mathcal{I}| = 1$. The designated world is represented by a circled bullet.
• Figure 2: Depth ($d$) and bound ($b$) of worlds for $k = 1, 2$ and $3$.
• Figure 3: Two $2$-bisimilar pointed models: $\mathcal{N}_1$ (left) and $\mathcal{N}_2$ (right).
• Figure 4: Pointed model $\mathcal{M}$ (left) of Figure \ref{['fig:bound']}, ${\llfloor \mathcal{M} \rrfloor}_{3}^{}$ (center) and ${\llfloor \mathcal{M} \rrfloor}_{2}^{}$ (right).
• Figure 5: Pointed model $\mathcal{M}$ (left) of Example \ref{['ex:k-contr']}, ${\llfloor \mathcal{M} \rrfloor}_{3}^{<}$ (center) and ${\llfloor \mathcal{M} \rrfloor}_{2}^{<}$ (right).

Theorems & Definitions (37)

• definition 1
• definition 2
• definition 3
• proposition 1: book/cup/Blackburn2001
• definition 4
• proposition 2: book/cup/Blackburn2001
• definition 5
• lemma 1: book/cup/Blackburn2001
• definition 6
• lemma 2