Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Branching Bisimulation Learning

Alessandro Abate, Mirco Giacobbe, Christian Micheletti, Yannik Schnitzer

TL;DR

The paper addresses verifying non-deterministic transition systems with bounded branching against CTL^{*}_{\setminus \bigcirc} specifications by learning finite, stutter-insensitive bisimulation quotients. It introduces a formal well-founded bisimulation framework and a counterexample-guided inductive synthesis loop that jointly learns a label-preserving state classifier and a ranking function, extracting a quotient that preserves branching-time properties. The approach leverages binary decision trees for interpretable, parameterised partitions and uses SMT-based solving to ensure global correctness, yielding efficient quotients even for very large or countably infinite state spaces. Experimental results show competitive performance across deterministic and non-deterministic benchmarks, with strong advantages in branching-time model checking for infinite-state systems and transparent, diagnostic quotients for system analysis.

Abstract

We introduce a bisimulation learning algorithm for non-deterministic transition systems. We generalise bisimulation learning to systems with bounded branching and extend its applicability to model checking branching-time temporal logic, while previously it was limited to deterministic systems and model checking linear-time properties. Our method computes a finite stutter-insensitive bisimulation quotient of the system under analysis, represented as a decision tree. We adapt the proof rule for well-founded bisimulations to an iterative procedure that trains candidate decision trees from sample transitions of the system, and checks their validity over the entire transition relation using SMT solving. This results in a new technology for model checking CTL* without the next-time operator. Our technique is sound, entirely automated, and yields abstractions that are succinct and effective for formal verification and system diagnostics. We demonstrate the efficacy of our method on diverse benchmarks comprising concurrent software, communication protocols and robotic scenarios. Our method performs comparably to mature tools in the special case of LTL model checking, and outperforms the state of the art in CTL and CTL* model checking for systems with very large and countably infinite state space.

Branching Bisimulation Learning

TL;DR

The paper addresses verifying non-deterministic transition systems with bounded branching against CTL^{*}_{\setminus \bigcirc} specifications by learning finite, stutter-insensitive bisimulation quotients. It introduces a formal well-founded bisimulation framework and a counterexample-guided inductive synthesis loop that jointly learns a label-preserving state classifier and a ranking function, extracting a quotient that preserves branching-time properties. The approach leverages binary decision trees for interpretable, parameterised partitions and uses SMT-based solving to ensure global correctness, yielding efficient quotients even for very large or countably infinite state spaces. Experimental results show competitive performance across deterministic and non-deterministic benchmarks, with strong advantages in branching-time model checking for infinite-state systems and transparent, diagnostic quotients for system analysis.

Abstract

We introduce a bisimulation learning algorithm for non-deterministic transition systems. We generalise bisimulation learning to systems with bounded branching and extend its applicability to model checking branching-time temporal logic, while previously it was limited to deterministic systems and model checking linear-time properties. Our method computes a finite stutter-insensitive bisimulation quotient of the system under analysis, represented as a decision tree. We adapt the proof rule for well-founded bisimulations to an iterative procedure that trains candidate decision trees from sample transitions of the system, and checks their validity over the entire transition relation using SMT solving. This results in a new technology for model checking CTL* without the next-time operator. Our technique is sound, entirely automated, and yields abstractions that are succinct and effective for formal verification and system diagnostics. We demonstrate the efficacy of our method on diverse benchmarks comprising concurrent software, communication protocols and robotic scenarios. Our method performs comparably to mature tools in the special case of LTL model checking, and outperforms the state of the art in CTL and CTL* model checking for systems with very large and countably infinite state space.

Paper Structure

This paper contains 17 sections, 4 theorems, 18 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Model Checking
  3. Stutter-Insensitive Bisimulations
  4. Well-founded Bisimulations with Bounded Branching
  5. Bisimulation Learning for Non-Deterministic Systems
  6. Procedure
  7. Learner
  8. Verifier
  9. Quotient Extraction
  10. Bisimulation Learning with Binary Decision Trees
  11. An Illustrative Example
  12. Experimental Evaluation
  13. Setup
  14. Results
  15. Discussion
  16. ...and 2 more sections

Key Result

theorem \@thmcountertheorem

Let ${\cal M}$ be a labelled transition system and let $\simeq$ be a label-preserving stutter-insensitive bisimulation on ${\cal M}$. For every $\text{CTL}^{*}_{\setminus \bigcirc }$ formula $\phi$, it holds that ${\cal M} \models \phi$ if and only if ${\cal M}/_\simeq \models \phi$. $\sqcap$$\sqcup

Figures (8)

  • Figure 1: States related under stutter-insensitive bisimulation, with examples of matching paths, consisting of identical subsequences of equivalence classes.
  • Figure 2: A system $\cal M$ and a possible stutter-insensitive bisimulation quotient ${\cal M}/_\simeq$. The abstract state $R$ lacks a self-loop despite an intra-class transition, as all represented concrete states eventually transition to $Q$. Conversely, $Q$ has a self-loop since its concrete states can remain within the class indefinitely.
  • Figure 3: Architecture of branching bisimulation learning.
  • Figure 4: A non-deterministic program and the corresponding stutter-insensitive bisimulation quotient synthesised with branching bisimulation learning.
  • Figure 5: Iterative process of branching bisimulation learning, illustrating three stages with generated counterexample states (purple dots).
  • ...and 3 more figures

Theorems & Definitions (13)

  • definition \@thmcounterdefinition: Transition Systems
  • remark \@thmcounterremark: Bounded vs. Finite Branching
  • definition \@thmcounterdefinition: Partitions
  • definition \@thmcounterdefinition: Quotient
  • definition \@thmcounterdefinition: Stutter-insensitive Bisimulation
  • remark \@thmcounterremark
  • theorem \@thmcountertheorem: DBLP:journals/tcs/BrowneCG88
  • theorem \@thmcountertheorem: DBLP:conf/fsttcs/Namjoshi97
  • theorem \@thmcountertheorem
  • proof
  • ...and 3 more