Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction

TL;DR

This paper investigates the complexity of model-checking problems for graphs and MDPs with respect to various $$-regular objectives, establishing new algorithms and conditional lower bounds that reveal fundamental separations between models and objectives.

Contribution

It introduces the first conditional super-linear lower bounds for model-checking problems and demonstrates model and objective separation results for classical $$-regular objectives.

Findings

Conditional super-linear lower bounds based on CNF-SAT and Boolean matrix multiplication assumptions.

Separation results showing disjunctive queries are harder than conjunctive ones for models and objectives.

New algorithms improving existing upper bounds for key model-checking problems.

Abstract

Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental $\omega$-regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and B\"uchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as reachability/safety (for disjunctive questions) and Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, B\"uchi, and coB\"uchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical $\omega$-regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives.