On Modal {\mu}-Calculus over Finite Graphs with Bounded Strongly Connected Components

TL;DR

This paper studies the modal mu-calculus over finite graphs with bounded strongly connected components, showing a hierarchy collapse to a specific level, contrasting with the hierarchy over all graphs.

Contribution

It proves the collapse of the modal mu-calculus hierarchy to Delta2 over SCCk graphs, highlighting a fundamental difference from the hierarchy over all graphs.

Findings

Hierarchy collapses to Delta2 for SCCk graphs

Hierarchy does not collapse to compositions of Sigma1 and Pi1 formulas

Contrast with the hierarchy over all graphs

Abstract

For every positive integer k we consider the class SCCk of all finite graphs whose strongly connected components have size at most k. We show that for every k, the Modal mu-Calculus fixpoint hierarchy on SCCk collapses to the level Delta2, but not to Comp(Sigma1,Pi1) (compositions of formulas of level Sigma1 and Pi1). This contrasts with the class of all graphs, where Delta2=Comp(Sigma1,Pi1).