• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction *
【24h】

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

机译：有条件下界的模型和目标分离：分离比连接更难*

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

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 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.
机译：给定系统模型和目标模型，模型检查问题将询问模型是否满足目标。我们针对两个基本的ω-正则目标，例如Rabin和Streett目标，在两个经典模型，图和马尔可夫决策过程（MDP）中研究多项式时间问题。对于许多这些问题，最著名的上限是二次方或三次方，但尚无超线性下限。在这项工作中，我们的贡献有两个方面：首先，我们提出了几种改进的算法，其次，我们基于对CNF-SAT和组合布尔矩阵乘法的复杂性的普遍认为的假设，提出了第一个条件超线性下界。关于一个目标的两个模型的分离结果意味着一个模型的条件下限严格高于另一个模型的现有上限，并且对于一个模型的两个目标类似。我们的结果建立了以下分离结果：（1）分离模型（图形和MDP），以分别解决可达性和Büchi目标。 （2）图形和MDP的两种目标分离，即（2a）诸如Streett / Rabin目标之类的双重目标的分离，以及（2b）同一类型的多个目标的合取与分离的分离例如安全性，Büchi和coBüchi。总而言之，我们的结果为各种经典ω-常规目标建立了图形和MDP的第一个模型和目标分离结果。令人惊讶的是，我们为析取目标建立了条件下界，该条件下界严格高于为相同目标的合计而存在的上限。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号