2024/05/01 by Thomas Bolander, Bolander, Thomas, Alessandro Burigana +1
Economics, Econometrics and Finance · Medicine · #Cardiac Arrhythmias and Treatments #Diverse Scientific and Economic Studies #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Pharmaceutical Economics and Policy
paper · pdf · doi:10.48550/arxiv.2405.00480
openalex publication_date 2024/05/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.