Upper and Lower Bounds for Graph Problems in Computer Aided Verification
Talkat Computational Complexity of Low-Polynomial Time Problems (Simons Institute workshop, 2015) · on Tuesday, 2015-12-08
summary
Defines graph and MDP objectives and proves fine-grained separations: disjunctive reachability on MDPs requires roughly K·M^(2−o(1)) time under triangle/OV hypotheses, while graphs admit O(M+N·K); gives matching MDP upper bounds of O(K·M + time to compute maximal end-component decomposition) and states MEC can be computed in min(N^2, M^1.5). Shows Street < Rabin (easier) and that disjunction is harder than conjunction across objectives.
AI-written summary · about
chapters (18)
- 0:00Intro
- 0:49Model Checking in Formal Verification
- 1:47Model 2
- 3:57Infinite Paths Induced by Token
- 13:52Algorithmic Question (2): Winning Set
- 17:58Conjunctive and Disjunctive Objectives
- 18:52Street and Rabin Objectives Rabin objective
- 20:37Definitions
- 20:58Algorithmic Question (3): Disjunctive Queries
- 21:19Disjunctive Objective vs. Disjunctive Queries Example for Reachability
- 24:11Fine-grain Approach to Model-Checking Problems
- 25:33Model Separation (MDPS vs Graphs)
- 26:31Dual Objective Separation on Graphs
- 26:58Dual Objective Separation on MDPS Dual objectives behave differently with disjunction
- 27:12Separating Conjunction and Disjunction
- 39:40Reachability in MDPS
- 41:47Maximal End-Component Decomposition
- 45:49Open Problems