A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems

TL;DR

This paper extends a saturation-based algorithm for the modal mu-calculus to include backwards modalities, enabling direct computation over pushdown system configuration graphs, marking a novel advancement in the field.

Contribution

It introduces the first saturation technique extension for the full mu-calculus with backwards modalities over pushdown systems.

Findings

First extension of saturation method to full mu-calculus with backwards modalities

Enables direct computation of mu-calculus formulas over pushdown systems

Advances verification techniques for systems with backwards modalities

Abstract

We present an extension of an algorithm for computing directly the denotation of a mu-calculus formula X over the configuration graph of a pushdown system to allow backwards modalities. Our method gives the first extension of the saturation technique to the full mu-calculus with backwards modalities.