Bounded Game-Theoretic Semantics for Modal Mu-Calculus and Some Variants

TL;DR

This paper introduces a bounded game-theoretic semantics for the modal mu-calculus that uses finite paths, simplifying analysis and enabling new variants with PTime model checking, with applications to model transformation and size games.

Contribution

It presents a novel bounded GTS for the mu-calculus that replaces parity games with finite-path evaluation games, offering new tools and variants for the logic.

Findings

Finite-path evaluation games replace parity games.

Applications include model transformation and PTime variants.

New formula size game developed for the logic.

Abstract

We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some applications to demonstrate its uses. For example, we consider a natural model transformation procedure that reduces model checking games to checking a single, fixed formula in the constructed models, and we also use the GTS to identify new alternative variants of the mu-calculus with PTime model checking.