# Technical Report MSC-2021-12

 TR#: MSC-2021-12 Class: MSC Title: On-the-fly Model Checking with Guided Abstraction Authors: Gal Sade Supervisors: Orna Grumberg PDF Currently accessibly only within the Technion network Abstract: Model checking is an automatic verification method that gets a system model and a specification, and checks whether the model satisfies the specification. CTL is a branching time temporal logic suitable for specifying behaviors of both software and hardware systems. It enables specifying properties that cannot be expressed in linear time logics, such as LTL. An example of such a property is restartability, which means that in every reachable state, the system may return to its initial state, due to a reset or a recovery. Further, in many cases, CTL model checking algorithms can be easily extended to handle the alternation-free fragment of the powerful $\mu$-calculus logic. In this work, we present a novel approach, OMG, that combines on-the-fly verification with abstraction in order to obtain an efficient CTL model checking algorithm. On-the-fly verification ensures that only parts that are needed for determining the satisfaction of the specification are developed. The abstraction is used to form inductive invariants, allowing OMG to determine satisfaction of the CTL specification without traversing the entire state-space. We formalize the correctness of OMG, and present both an explicit version of the algorithm and a symbolic one. We implemented our algorithm on top of a combination of explicit and symbolic representations, where symbolic representations are handled with SAT/SMT solvers. Our experiments show that on a few examples, our algorithm outperforms a state-of-the-art SAT-based algorithm for CTL. Copyright The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2021/MSC/MSC-2021-12), rather than to the URL of the PDF files directly. The latter URLs may change without notice.