Enriched MU-Calculi Module Checking

TL;DR

This paper studies the complexity of model checking for an enriched mu-calculus with nominals, graded modalities, and inverse programs, providing tight bounds and undecidability results for various fragments.

Contribution

It introduces automata-theoretic algorithms for hybrid graded mu-calculus module checking and establishes tight exponential and double-exponential time bounds, also proving undecidability for the fully enriched variant.

Findings

Hybrid graded mu-calculus module checking is in EXPTIME for finite-state systems.

Pushdown module checking for the same logic is in 2EXPTIME.

Adding inverse programs leads to undecidability.

Abstract

The model checking problem for open systems has been intensively studied in the literature, for both finite-state (module checking) and infinite-state (pushdown module checking) systems, with respect to Ctl and Ctl*. In this paper, we further investigate this problem with respect to the \mu-calculus enriched with nominals and graded modalities (hybrid graded Mu-calculus), in both the finite-state and infinite-state settings. Using an automata-theoretic approach, we show that hybrid graded \mu-calculus module checking is solvable in exponential time, while hybrid graded \mu-calculus pushdown module checking is solvable in double-exponential time. These results are also tight since they match the known lower bounds for Ctl. We also investigate the module checking problem with respect to the hybrid graded \mu-calculus enriched with inverse programs (Fully enriched \mu-calculus): by showing a reduction from the domino problem, we show its undecidability. We conclude with a short overview of the model checking problem for the Fully enriched Mu-calculus and the fragments obtained by dropping at least one of the additional constructs.