We present a novel algorithmic framework for Three-valued Abstraction Refinement, which extends Counterexample-guided Abstraction Refinement with the ability to verify all properties of mu-calculus including recovery (the ability of the system to always return to a certain state). The framework performs refinement on abstract system inputs rather than abstract states, avoiding problems of previous frameworks. We formalise input-based refinement by introducing the concept of generating automata, and prove that our framework is sound, monotone, and complete. We evaluate the usefulness of the framework on its implementation in our free and open-source formal verification tool.

翻译：本文提出了一种新颖的三值抽象精化算法框架，该框架通过扩展反例引导的抽象精化方法，使其能够验证包括恢复性（系统始终能返回特定状态的能力）在内的所有μ演算属性。本框架在抽象系统输入而非抽象状态层面执行精化操作，从而避免了先前框架存在的问题。我们通过引入生成自动机的概念形式化定义了基于输入的精化过程，并证明了该框架具有可靠性、单调性与完备性。我们通过在本团队开发的开源形式化验证工具中实现该框架，评估了其实用价值。