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

Understand

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.