具有条件下界的模型与客观分离：析取比合取更难
Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction
摘要：
给定一个系统的模型和一个目标，模型检查问题询问模型是否满足目标。我们研究多项式时间问题的两个经典模型，图和马尔可夫决策过程（MDP），关于几个基本的$ω$ -经常性的目标，例如，拉宾和斯特里特的目标。对于这些问题中的许多最著名的上界是二次或三次，但没有超线性下界是已知的。在这项工作中，我们的贡献是双重的：第一，我们提出了几个改进的算法，第二，我们提出了第一个条件超线性下界的基础上广泛认为CNF-SAT和组合布尔矩阵乘法的复杂性的假设。两个模型相对于目标的分离结果意味着一个模型的条件下限严格高于另一模型的现有上限，并且类似地，两个目标相对于模型。我们的结果建立了以下分离结果：（1）分离的模型（图和MDP）的可达性和Büchi目标的析取查询。(2)图和MDP的两种目标分离，即（2a）双重目标的分离，例如可达性/安全性（对于析取问题）和Streett/Rabin目标，以及（2b）同一类型的多个目标的合取和析取的分离，例如安全性，Büchi和coBüchi。总之，我们的研究结果建立了第一个模型和客观的分离结果的图和MDP的各种经典$ω$定期目标。非常引人注目的是，我们建立的条件下限分离的目标，严格高于现有的上限相同的目标的结合。
英文摘要：
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 $ω$-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üchi 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üchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical $ω$-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
