An approximation-based incremental SMT approach for diagnosability analysis of real-time systems

In this article, we focus on improving the efficiency of diagnosability checking for real-time systems modeled as timed automata. Inspired by a recently introduced extension of the classic CEGAR (CounterExample-Guided Abstraction Refinement) algorithm, namely the RECAR (Recursive Explore and Check Abstraction Refinement) algorithm, we propose new RECAR-like algorithms that combine over-approximation and under-approximation techniques. We use CEGAR to quickly terminate the refinement loop by over-approximation and under-approximation, in the case where the original formula is respectively satisfiable or unsatisfiable, and then show the soundness of our RECAR-like approach applied to an arbitrary formula. We define then several types of parameterized over- and under-approximations along with refinement strategies for the diagnosability problem. Finally, we evaluate the effectiveness of our method and its implementation with the Z3 SMT solver on different benchmarks by comparing it to the direct method without approximation shortcuts.