Bisimulation Learning
This addresses the challenge of efficient verification for complex systems in fields like software model checking, though it is incremental as it builds on existing bisimulation and learning techniques.
The paper tackles the problem of computing finite bisimulations for large or infinite state transition systems by introducing a data-driven approach that learns a state classifier and ranking functions from samples, verified via satisfiability modulo theory solving in a counterexample-guided loop. It demonstrates faster verification results than state-of-the-art tools on benchmarks from reactive verification and software model checking, producing succinct and interpretable abstractions.
We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems, which we characterize as the problem of learning a state classifier together with a ranking function for each class. Our procedure learns a candidate state classifier and candidate ranking functions from a finite dataset of sample states; then, it checks whether these generalise to the entire state space using satisfiability modulo theory solving. Upon the affirmative answer, the procedure concludes that the classifier constitutes a valid stutter-insensitive bisimulation of the system. Upon a negative answer, the solver produces a counterexample state for which the classifier violates the claim, adds it to the dataset, and repeats learning and checking in a counterexample-guided inductive synthesis loop until a valid bisimulation is found. We demonstrate on a range of benchmarks from reactive verification and software model checking that our method yields faster verification results than alternative state-of-the-art tools in practice. Our method produces succinct abstractions that enable an effective verification of linear temporal logic without next operator, and are interpretable for system diagnostics.