Compositional Verification and 3-Valued Abstractions Join Forces

Two of the most promising approaches to fighting the state explosion problem are abstraction and compositional verification. In this work we join their forces to obtain a novel fully automatic compositional technique that can determine the truth value of the full

μ

-calculus with respect to a given system.

Given a system

$\ensuremath{M} = \ensuremath{M}_1 \parallel \ensuremath{M}_2$

, we view each component

$\ensuremath{M}_i$

as an abstraction

${\ensuremath{M}_i}\uparrow$

of the global system. The abstract component

${\ensuremath{M}_i}\uparrow $

is defined using a 3-valued semantics so that whenever a

μ

-calculus formula

ϕ

has a definite value (true or false) on

${\ensuremath{M}_i}\uparrow $

, the same value holds also for

$\ensuremath{M}$

. Thus,

ϕ

can be checked on either

${\ensuremath{M}_1}\uparrow $

or

${\ensuremath{M}_2}\uparrow $

(or both), and if any of them returns a definite result, then this result holds also for

$\ensuremath{M}$

. If both checks result in an indefinite value, the composition of the components needs to be considered. However, instead of constructing the composition of

${\ensuremath{M}_1}\uparrow $

and

${\ensuremath{M}_2}\uparrow $

, our approach identifies and composes only the parts of the components in which their composition is necessary in order to conclude the truth value of

ϕ

. It ignores the parts which can be handled separately. The resulting model is often significantly smaller than the full system.

We explain how our compositional approach can be combined with abstraction, in order to further reduce the size of the checked components. The result is an incremental compositional abstraction-refinement framework, which resembles automatic Assume-Guarantee reasoning.