Branching Bisimulation Learning

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.