Conditionally Optimal Algorithms for Generalized Büchi Games
Chatterjee, Dvořák, Henzinger, Loitzenbauer · cs.DS,cs.LO · 2016-07-20 · 原文
Games on graphs provide the appropriate framework to study several central problems in computer science, such as the verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with n vertices, m edges, and generalized Büchi objectives with k conjunctions. First, we present an algorithm with running time O(k \cdot n^2), improving the previously known O(k \cdot n \cdot m) and O(k^2 \cdot n^2) worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for
讲义
讲义·推断 依据「原文」自动生成的结构化摘要（推断），非原文表述；以原文为准。
1. 人话版
Games on graphs provide the appropriate framework to study several central problems in computer science, such as the verification and synthesis of reactive systems.
One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often.
2. 领域脉络
本文类目：cs.DS、cs.LO，属于其所在研究脉络的最新进展。
3. 机制拆解
We consider graph games with n vertices, m edges, and generalized Büchi objectives with k conjunctions.
4. 证据与数字
We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification.
We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT.
First, we present an algorithm with running time O(k \cdot n^2), improving the previously known O(k \cdot n \cdot m) and O(k^2 \cdot n^2) worst-case bounds.
5. 反例与边界
摘要未声明局限与反例——这是需要警惕的信号，精读时先问边界。
6. 跨领域连接与意外收获
横跨 2 个类目（cs.DS、cs.LO），关注其在你兴趣板块间的迁移面。
7. 可复用方法
把本文机制与你手头项目对照，找一个两周内能验证的最小实验。
8. 术语表
精读时把不熟的术语记入此处，作为下次回忆的锚点。