Complexity of Monadic inf-datalog. Application to temporal logic

TL;DR

This paper analyzes the computational complexity of evaluating Monadic inf-Datalog programs, showing linear and polynomial bounds for various modal logics and their fragments, with implications for model checking efficiency.

Contribution

It provides a unified proof of complexity bounds for model checking in modal and mu-calculus logics using Monadic inf-Datalog evaluation.

Findings

Model checking for CTL and alternation-free modal μ-calculus is linear in data and program complexity.

Linear-space complexities are established for these logics.

Polynomial-time data complexity is shown for fixed alternation-depth μ-calculus.

Abstract

In [11] we defined Inf-Datalog and characterized the fragments of Monadic inf-Datalog that have the same expressive power as Modal Logic (resp. $CTL$, alternation-free Modal $\mu$-calculus and Modal $\mu$-calculus). We study here the time and space complexity of evaluation of Monadic inf-Datalog programs on finite models. We deduce a new unified proof that model checking has 1. linear data and program complexities (both in time and space) for $CTL$ and alternation-free Modal $\mu$-calculus, and 2. linear-space (data and program) complexities, linear-time program complexity and polynomial-time data complexity for $L\mu\_k$ (Modal $\mu$-calculus with fixed alternation-depth at most $k$).}