Efficient Model Checking for the Alternating-Time {\mu}-Calculus via Effectivity Frames

TL;DR

This paper explores whether using effectivity frames instead of concurrent game frames can improve the efficiency of model checking for the alternating-time {0}-calculus, showing promising performance gains on large systems.

Contribution

It provides a translation method from concurrent game frames to effectivity frames and demonstrates potential performance improvements in model checking.

Findings

Effectivity frames can be more compact than concurrent game frames.

Model checking with effectivity frames shows performance gains on large systems.

Conversion overhead is often offset by faster model checking in practice.

Abstract

The semantics of alternating-time temporal logic (ATL) and the more expressive alternating-time {\mu}-calculus (AMC) is standardly given in terms of concurrent game frames (CGF). The information required to interpret AMC formulas is equivalently represented in terms of effectivity frames in the sense of Pauly; in many cases, this representation is more compact than the corresponding CGF, and in principle allows for faster evaluation of coalitional modalities. In the present work, we investigate whether implementing a model checker based on effectivity frames leads to better performance in practice. We implement the translation from concurrent game frames to effectivity frames and analyse performance gains in model checking based on corresponding instantiations of a generic model checker for coalgebraic {\mu}-calculi, using dedicated benchmark series as well as random systems and formulas. In the process, we also compare performance to the state-of-the-art ATL model checkerMCMAS. Our results indicate that on large systems, the overhead involved in converting a CGF to an effectivity frame is often outweighed by the benefits in subsequent model checking.