Model Checking as Program Verification by Abstract Interpretation (Extended Version)

TL;DR

This paper presents a novel approach to model checking by encoding temporal logic formulas as programs in MOKA and applying abstract interpretation, enabling more flexible abstractions and dynamic precision tuning.

Contribution

It introduces MOKA, a language for encoding temporal logics as programs, and demonstrates model checking as program verification using abstract interpretation with dynamic refinement.

Findings

MOKA can encode universal temporal logics as programs.

Abstract interpretation on MOKA programs improves analysis precision.

The approach reduces false alarms through counterexample-guided refinement.

Abstract

Abstract interpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions based on (bi)simulation and property-preserving state relations have been successfully applied to abstract model checking. Here, we pursue a different track in which model checking is seen as an instance of program verification. To this purpose, we introduce a suitable language-called MOKA (for MOdel checking as abstract interpretation of Kleene Algebras)-which is used to encode temporal formulae as programs. In particular, we show that (universal fragments of) temporal logics, such as ACTL or, more generally, universal mu-calculus can be transformed into MOKA programs. Such programs return all and only the initial states which violate the formula. By applying abstract interpretation to MOKA programs, we pave the way for reusing more general abstractions than partitions as well as for tuning the precision of the abstraction to remove or avoid false alarms. We show how to perform model checking via a program logic that combines under-approximation and abstract interpretation analysis to avoid false alarms. The notion of locally complete abstraction is used to dynamically improve the analysis precision via counterexample-guided domain refinement.