On P-transitive graphs and applications

TL;DR

This paper introduces P-transitive graphs, explores their logical properties, and demonstrates their significance through results on fixpoint hierarchies, undecidability, and model checking complexity, contrasting with transitive graphs.

Contribution

It defines P-transitive graphs, analyzes their logical and computational properties, and establishes key differences from transitive graphs, including undecidability and hierarchy infiniteness.

Findings

The mu-calculus hierarchy is infinite for P-transitive graphs.

Decidability results differ from transitive graphs.

Model checking reduces to P-transitive graphs in polynomial time.

Abstract

We introduce a new class of graphs which we call P-transitive graphs, lying between transitive and 3-transitive graphs. First we show that the analogue of de Jongh-Sambin Theorem is false for wellfounded P-transitive graphs; then we show that the mu-calculus fixpoint hierarchy is infinite for P-transitive graphs. Both results contrast with the case of transitive graphs. We give also an undecidability result for an enriched mu-calculus on P-transitive graphs. Finally, we consider a polynomial time reduction from the model checking problem on arbitrary graphs to the model checking problem on P-transitive graphs. All these results carry over to 3-transitive graphs.