Expressiveness and Completeness in Abstraction

TL;DR

This paper compares two notions of expressiveness in abstraction theory for model checking, showing their incomparability, and explores how abstraction parameters influence the completeness of finite models.

Contribution

It establishes the incomparability of two key expressiveness notions and analyzes how abstraction parameters affect the completeness of finite models.

Findings

Kripke Modal Transition Systems are less expressive than Generalised Kripke Modal Transition Systems

Expressiveness notions are generally incomparable in abstraction theory

Completeness depends on abstraction parameters and relates to expressiveness

Abstract

We study two notions of expressiveness, which have appeared in abstraction theory for model checking, and find them incomparable in general. In particular, we show that according to the most widely used notion, the class of Kripke Modal Transition Systems is strictly less expressive than the class of Generalised Kripke Modal Transition Systems (a generalised variant of Kripke Modal Transition Systems equipped with hypertransitions). Furthermore, we investigate the ability of an abstraction framework to prove a formula with a finite abstract model, a property known as completeness. We address the issue of completeness from a general perspective: the way it depends on certain abstraction parameters, as well as its relationship with expressiveness.