Focus-style proofs for the two-way alternation-free $\mu$-calculus

TL;DR

This paper presents a novel cyclic proof system for the two-way alternation-free modal μ-calculus, enabling more effective reasoning about backwards modalities through trace atoms and strategy-based semantics.

Contribution

It introduces a new proof system that handles backwards modalities using trace atoms and strategy semantics, advancing the proof theory of the μ-calculus.

Findings

The system is sound for all sequents.

It is complete for sequents without trace atoms.

The approach connects automata reduction techniques with proof systems.

Abstract

We introduce a cyclic proof system for the two-way alternation-free modal $\mu$-calculus. The system manipulates one-sided Gentzen sequents and locally deals with the backwards modalities by allowing analytic applications of the cut rule. The global effect of backwards modalities on traces is handled by making the semantics relative to a specific strategy of the opponent in the evaluation game. This allows us to augment sequents by so-called trace atoms, describing traces that the proponent can construct against the opponent's strategy. The idea for trace atoms comes from Vardi's reduction of alternating two-way automata to deterministic one-way automata. Using the multi-focus annotations introduced earlier by Marti and Venema, we turn this trace-based system into a path-based system. We prove that our system is sound for all sequents and complete for sequents not containing trace atoms.