The Modal Logic of Abstraction Refinement

TL;DR

This paper explores how system property truth values change during abstraction refinement in model checking, using modal logic to formalize and analyze these changes across various abstraction scenarios.

Contribution

It introduces a modal logic framework with alethic modalities for abstraction refinement, providing bounds and techniques for analyzing property preservation.

Findings

Bounds for modal logics in abstraction refinement scenarios

Development of control statement techniques for modal logic analysis

Formalization of property truth value changes during refinement

Abstract

Iterative abstraction refinement techniques are one of the most prominent paradigms for the analysis and verification of systems with large or infinite state spaces. This paper investigates the changes of truth values of system properties expressible in computation tree logic (CTL) when abstractions of transition systems are refined. To this end, the paper utilizes modal logic by defining alethic modalities expressing possibility and necessity on top of CTL: The modal operator $\lozenge$ is interpreted as "there is a refinement, in which ..." and $\Box$ is interpreted as "in all refinements, ...". Upper and lower bounds for the resulting modal logics of abstraction refinement are provided for three scenarios: 1) when considering all finite abstractions of a transition system, 2) when considering all abstractions of a transition system, and 3) when considering the class of all transition systems. Furthermore, to prove these results, generic techniques to obtain upper bounds of modal logics using novel types of so-called control statements are developed.