Branching Bisimulation Learning

We introduce an algorithm for synthetizing bisimulations for non-deterministic transition systems. We extend pre-existing work, known as "bisimulation learning", which is applicable to deterministic systems only and afford model checking of linear-time properties. Starting from a system with a bounded number of outgoing transitions per state, this method computes a finite-state, stutter-insensitive bisimulation quotient that preserves properties expressed in CTL* without the Next operator. We adapt the proof rule for well-founded bisimulations to an iterative procedure that refines candidate system abstractions from sample transitions of the system, and checks their validity over the entire transition relation using SMT solving. Our technique is sound, entirely automated, and yields abstractions that are both succinct and effective for formal verification and system diagnostics. We demonstrate the efficacy of our method on several benchmarks modelling diverse 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.