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.

我们介绍了一种基于数据驱动的方法来计算具有非常大，可能是无限状态空间的状态转换系统的有限双模拟。我们的新技术计算确定性系统的阻塞不敏感的双模拟，我们将其描述为学习状态分类器与每个类的排名函数的问题。我们的方法从一个有限的样本状态数据集中学习候选状态分类器和候选排名函数；然后，它使用可满足性模理论求解检查这些是否推广到整个状态空间。如果得到肯定答案，该过程得出结论，该分类器构成了系统的有效阻塞不敏感的双模拟。如果得到否定答案，求解器会生成一个反例状态，该状态违反了该分类器的断言，将其添加到数据集中，并在反例引导的归纳合成循环中重复学习和检查，直到找到有效的双模拟。我们在反应性验证和软件模型检查的一系列基准测试中展示了我们的方法在实践中优于其他最先进的工具的更快验证结果。我们的方法产生简洁的抽象，使得能够有效地验证不包含下一个运算符的线性时态逻辑，并且对于系统诊断具有解释能力。