Faster Game Solving by Fixpoint Acceleration
University of Liverpool（利物浦大学）
提出通过计算DAG吸引子函数的嵌套不动点加速求解具有无环子结构的奇偶博弈，并设计经济构造将Emerson-Lei博弈转化为奇偶博弈以实现加速求解。
2025-11-04 cs.GT cs.LO
Quasipolynomial Computation of Nested Fixpoints
众所周知，具有$n$节点和$k$优先级的奇偶博弈的获胜区域可以被计算为合适函数的$k$嵌套不动点;该嵌套不动点的直接计算需要函数的$\mathcal{O}(n^{\frac{k}{2}})$迭代。Calude等人最近的quasipolynomial-time parity game solving algorithm基本上展示了如何通过将parity game减少到quasipolynomialy大小的安全game来仅在quasipolynomialy多次迭代中计算相同的不动点。通用图已被用来模块化的奇偶性游戏，以等效的安全游戏，通过结合原始游戏与通用图。我们表明，这种方法自然地推广到有限格上的\emph{any}不动点方程系统的解的计算，因此，不动点方程系统的解可以通过方程的拟多项式多次迭代来计算。我们目前的应用程序模式不动点逻辑和游戏超越关系语义。以能量$μ$ -演算、有限格化$μ$ -演算、分次和有限格化$μ$ -演算为例，讨论了能量$μ$ -演算、有限格化$μ$ -演算、分次和有限格化$μ$-演算的模型检验问题。（二值）概率$μ$ -微积分--用二进制编码的数字--可以通过函数的嵌套不动点来求解，这些函数与奇偶博弈的函数有很大不同，但仍然可以在准多项式时间内计算;因此，我们的结果意味着对这些$μ$演算的模型检验是在QP中。此外，我们改进了指数在已知的指数界的可满足性检查。
2021-03-19 cs.CC cs.LO
Parity Games and Automata for Game Logic (Extended Version)
Parikh的游戏逻辑是一个类似PDL的不动点逻辑，它在单调邻域框架上解释，表示玩家在确定的两人游戏中的战略力量。博弈逻辑转化为单调$μ$ -演算的一个片段，而单调模式自动机又在表达上等价于单调模式自动机。奇偶博弈和自动机是处理模态不动点逻辑（如模态$μ$ -演算）中嵌套不动点的组合复杂性的重要工具。本文（1）讨论了邻域结构上博弈逻辑的奇偶博弈语义a，（2）利用这些博弈得到了对应于博弈逻辑的单调$μ$ -演算片段的自动机理论刻画。我们的证明广泛使用的结构，我们称之为语法图，结合了易于使用的语法树的公式与自动机的灵活性和简洁性。它们本质上是一个基于图的观点的交替树自动机，介绍了威尔克在研究模态$μ$ -演算。
2017-09-03 cs.LO
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
本文提出参数化模型检测工具 COOL-MC，支持多种 μ-演算实例，并通过归约奇偶博弈或惰性局部算法进行检测和基准评估。
2023-11-03 cs.LO
Universal Algorithms for Parity Games and Nested Fixpoints
给出了一种用于求解奇偶博弈的吸引子分解元算法，该算法推广了经典的McNaughton-Zielonka算法及其最近的准多项式变体，这些变体是由Parys（2019）以及Lehtinen，Schewe和Wojtczak（2019）提出的。研究和利用的中心概念是吸引子分解的dominia在奇偶游戏和有序树描述的诱导结构的吸引子分解。通用算法产生McNaughton-Zielonka，Parys和Lehtinen-Schewe-Wojtczak算法作为特殊情况下，适当的通用树作为输入。主要的技术成果提供了一个统一的证明的正确性和结构的见解，这些算法。将奇偶对策的通用算法适当地应用于不动点对策，给出了有限完备格上计算嵌套不动点的拟多项式时间算法。奇偶对策和嵌套不动点的通用算法可以符号化实现。它展示了如何使用$O(\lg d)$符号空间复杂度来实现这一点，改进了Chatterjee，Dvotelák，Henzinger和Svozil（2018）为奇偶游戏实现的$O(d \lg n)$符号空间复杂度，其中$n$是顶点的数量，$d$是奇偶游戏中不同优先级的数量。
2022-08-29 cs.DS cs.FL cs.GT
Least and greatest fixpoints in game semantics
我们展示了如何解决许多递归竞技场方程可以计算在一个自然的方式，允许循环竞技场。然后，我们为竞技场配备获胜功能和总获胜策略。我们提出了两个自然获胜条件兼容的循环建设，分别提供了初始代数和终端余代数的一大类连续函子。最后，我们引入了一个直观的微积分，扩展与语法结构的最小和最大的不动点，并证明它有一个健全的和（在一定的弱意义上）完整的解释，在我们的游戏模型。
2010-01-05 cs.GT cs.LO cs.PL
A Lattice-Theoretical View of Strategy Iteration
策略迭代是一种经常用于两人游戏的技术，以确定获胜者或计算收益，但据我们所知，没有考虑策略迭代的一般框架。受以前简单随机游戏工作的启发，我们提出了一个一般形式化的策略迭代求解最小不动点方程在一个合适的类的完整的格，基于MV链。我们设计的算法，可用于非扩张不动点函数表示为所谓的最小，分别，最大分解。相应地，我们开发了两种不同的技术：从上面的策略迭代，它必须解决迭代可能达到一个不动点的问题，而从下面的，这是算法上更简单，但需要一个更复杂的正确性参数。我们应用我们的方法来解决能量游戏和计算概率自动机的行为度量。
2022-12-13 cs.LO
Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic Games
University of Padua（帕多瓦大学）；Universität Duisburg-Essen（杜伊斯堡-埃森大学）
本文提出改进的阻尼曼迭代方法，用于计算学习函数的不动点，适用于高维问题和概率模型，如简单随机游戏。
2026-01-22 cs.LG cs.LO
The Complexity of Model Checking Higher-Order Fixpoint Logic
高阶不动点逻辑（Higher-Order Fixpoint Logic，HFL）是简单类型λ演算和模态λ演算的混合。这使得它成为一个高度表达的时态逻辑，能够表达模态λ演算中无法表达的程序的各种有趣的正确性属性。本文给出了其模型检验问题的复杂性结果。特别是，我们认为这些片段的HFL只使用类型的有界阶k和arity m。我们建立k倍指数时间完备性的模型检验每个这样的片段。对于上界，我们使用不动点消除，以获得可达性游戏，是单指数的大小的公式和k倍指数的大小的底层过渡系统。这些博弈可以在确定性线性时间内求解。作为一个简单的结果，我们得到一个指数时间上界的表达复杂性的每个这样的片段。下界是由交替（k-1）重指数空间有界图灵机的字问题的一个简化而建立的。由于有固定的机器的类型，其字的问题已经很难相对于k倍指数时间，我们得到，作为一个推论，k倍指数时间完整性的数据复杂性的片段的HFL，提供m超过3。这也产生了表达能力的层次结构。
2007-06-29 cs.LO
Combining fixpoint and differentiation theory
本文提出一个结合不动点与导数的范畴框架，通过引入新公理统一两者，并应用于牛顿-拉弗森优化及高阶语言扩展。
2024-07-17 cs.LO math.CT
Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics
虽然在扩展完整布尔基的逻辑中进行推理是困难的，但限制于模态语言的合取片段有时允许即使在存在最大不动点的情况下也进行易于处理的推理。一个这样的例子是EL家族的描述逻辑;在这里，有效的推理是基于满意度检查在适当的小模型，表征公式的模拟。然而，众所周知，并不是每一种合取模态语言都有一个易于处理的推理问题。自然的问题是，这些易处理的片段有多常见，以及如何识别它们。在这项工作中，我们提供了足够的条件，在一般的方式，考虑未标记的Tableau规则，为一个给定的模态逻辑的易处理性。我们工作的框架内的coalgebraic逻辑作为一个统一的语义设置。除了恢复已知的结果描述逻辑，如EL和FL 0，我们获得了新的关联和非关联模态逻辑的最大不动点的合取片段。最值得注意的是，我们发现了游戏逻辑和交替时间μ演算的易处理片段。
2014-06-06 cs.LO
Characterising Probabilistic Alternating Simulation for Concurrent Games
概率博弈结构结合了非确定性和随机性，参与者重复地同时采取行动，以进入并发博弈的下一个状态。概率交替模拟是比较不同概率博弈结构行为的重要工具。在本文中，我们提出了一个健全的和完整的模态特性的模拟关系，提出了一个新的逻辑概率分布的基础上。该逻辑使玩家能够在下一个状态或分布中强制执行属性。它的不动点扩张也是模拟关系的特征，在实际应用中可以表达许多有趣的性质。
2019-07-09 cs.LO
Certification for mu-calculus with winning strategies
我们定义了内存高效的证书$μ$演算模型检查问题的基础上，众所周知的对应关系的$μ$演算模型检验赢得一定的奇偶校验游戏。获胜策略可以在低多项式时间内独立检验，方法是观察奇偶博弈图中不存在最大优先级为奇数的可达强连通分支。获胜策略的计算遵循$μ$ -演算的朴素语义，通过不动点迭代。我们对$μ$ -演算模型检验的通常的不动点迭代进行检测，以便它以获胜策略的形式产生证据;这些获胜策略可以在$|S|$和空间$O(|S|^2 |ϕ|^2)$中以多项式时间计算，其中$|S|$是状态空间的大小，$|ϕ|$是公式$ϕ$ \@的长度。这里主要的技术贡献是部分获胜策略的概念和代数。在技术层面上，我们的工作可以被看作是一个新的，更简单的，直接建设性的证明之间的对应关系$μ$ -演算和奇偶游戏。
2014-01-08 cs.LO
Diamonds Are Forever: Stabilization Semantics for Unrestricted Aggregation and Recursion in Logica
Google LLC（谷歌有限责任公司）；University of Illinois, Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；Gonzaga University（贡萨加大学）
针对 Logica 语言中自由组合递归与聚合带来的语义挑战，提出 Defendant-Opponent (DO) 语义，一种基于稳定化的非单调逻辑程序语义框架，并通过博弈论和模态逻辑两种等价刻画，兼容传统不动点语义并为无不动点收敛程序提供严格解释。
2026-06-03 cs.LO
An infinitary model of linear logic
在本文中，我们构造了线性逻辑关系模型的无限变体，其中指数模态被解释为有限或可数多集的集合。我们解释如何解释在这个模型中的不动点算子Y作为一个康威算子交替定义在一个归纳或共归纳的方式。然后，我们扩展的关系语义的颜色或优先级的意义上的奇偶性游戏的概念。这种扩展使我们能够定义一个新的不动点算子Y结合归纳和共归纳的政策。最后，我们勾勒出的结果模型之间的联系，递归和高阶模型检查的演算。
2015-01-28 cs.LO
COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics
本研究开发了面向代数模态不动点逻辑的通用推理器COOL 2，可实例化为多种模态逻辑的推理工具，并在多类基准集上完成了评估。
2023-06-15 cs.FL cs.LO
Countdown $μ$-calculus
我们介绍了倒计时$μ$ -演算，扩展的模态$μ$ -演算的顺序近似的不动点算子。除了经典微积分中可定义的性质外，它还可以表达（无）有界性，例如存在任意长的特定动作序列。与奇偶游戏和自动机的标准对应关系扩展到适当定义的倒计时游戏和自动机。然而，与经典的设置，标量片段是可证明的弱于完整的向量演算，并对应于自动机满足一个简单的语法条件。我们建立了一些事实，特别是可判定性的模型检验问题和严格的层次结构所引起的最大允许嵌套我们的新运营商。
2022-07-31 cs.LO
Filtration and canonical completeness for continuous modal mu-calculi
连续模态μ演算是模态μ演算的一个片段，其中不动点算子的应用仅限于其函数解释是斯科特连续的公式，而不仅仅是单调的。通过博弈论的手段，我们表明，这个相对表现力的片段仍然允许基本模态逻辑，这是出了名的失败的充分模态μ演算：过滤和规范模型的两个重要技术。特别是，我们证明了过滤定理的公式在语言中的连续模态μ演算。因此，我们得到了有限的模型属性在广泛的模型类。此外，我们证明了，如果一个基本模态逻辑L是标准的和类的L-框架允许过滤，那么通过添加连续不动点算子L得到的逻辑是健全的和完整的关于类的L-框架。这概括了最近的结果严格较弱的片段的模态μ演算，即PDL。
2021-09-17 cs.LO
Logics and Games for True Concurrency
我们研究了基于过渡系统，Petri网和事件结构的各种偏序模型的并发性的基本数学性质，并表明这些系统的并发行为可以通过两个简单的和一般的对偶局部行为以统一的方式捕获。这种对偶性被用来定义新的μ演算和逻辑游戏，用于分析具有偏序语义的并发系统。这项工作的一些结果是：一些mu-演算的定义，在某些类的系统，诱导相同的标识作为一些最有名的互模拟等价的并发性;和定义（无限）高阶逻辑游戏的互模拟和模型检查，其中的球员的游戏给予（本地）一元二阶权力的一组元素，他们被允许发挥。更具体地说，我们表明，我们的游戏是健全的和完整的，因此，确定;此外，它们是可判定的有限情况下，并支持新的决策程序的互模拟和模型检查。由于这些mu演算和逻辑游戏概括了著名的不动点逻辑和博弈论决策程序的并发系统与交织语义，本文的结果给出了一些基础的设计一个基于逻辑的，博弈论的框架研究，在一个统一的方式，几个并发系统，无论他们是否有交织或偏序语义。
2010-11-04 cs.LO
First-Order Game Logic and Modal Mu-Calculus
本文研究了一阶博弈逻辑和一阶模态μ演算，它们用解释效果的一阶模态（如变量赋值）扩展了命题模态逻辑。不像在命题的情况下，这两个逻辑被证明具有相同的表达能力和他们的证明演算具有相同的演绎能力。两种结石也相互比较完整。在微分方程的存在下，推论获得了微分博弈逻辑（混合博弈的演绎验证逻辑）和微分μ演算（混合系统的模态μ演算）之间的可用和完整的翻译。微分μ-演算相对于一阶不动点逻辑是完备的，微分对策逻辑相对于它的无常微分的片段是完备的。
2022-02-11 cs.GT cs.LO math.LO
A Parity Game Tale of Two Counters
奇偶博弈是在有限图上进行的简单的无限博弈，其获胜条件具有足够的表现力以捕获嵌套的最小和最大不动点。通过它们与模态μ演算的紧密关系，它们在实践中用于μ演算以及相关时态逻辑（例如LTL和CTL）的模型检查和综合问题。解决奇偶博弈是一个引人注目的复杂性理论问题，因为该问题位于UP和co-UP的交叉点，并且被认为是多项式时间的解决方案，激励研究人员找到这样的解决方案或找到现有算法的超多项式下界，以提高对奇偶博弈的理解。我们提出了一个参数化的奇偶性游戏称为两个计数器的游戏，它提供了一个指数下界的吸引子为基础的奇偶性游戏求解算法。我们是第一个为延迟提升策略的优先级提升提供指数下限的人，也是第一个为缠结学习提供这样的下限的人。
2019-09-17 cs.GT cs.LO
Satisfiability Games for Branching-Time Logics
分支时间时态逻辑如CTL*、CTL和CTL+的可满足性问题在程序规范和验证中有重要的应用。它们的计算复杂性是已知的：CTL* 和CTL+对于双指数时间是完全的，CTL对于单指数时间是完全的.这些逻辑的一些决策程序是已知的;它们使用树自动机，tableaux或公理系统。在本文中，我们提出了一个统一的博弈论框架，这些分支时间时序逻辑的可满足性问题。我们定义可满足性游戏的完整的分支时间时序逻辑CTL* 使用高层次的定义获胜的条件，抓住了最少不动点展开的本质的良好基础。这些获胜条件构成了ω-词的形式语言。我们分析了在何种情况下需要哪种确定性ω-自动机来识别这些语言。然后，我们得到一个减少的问题，解决奇偶校验或Büchi游戏。所获得的算法的最坏情况下的复杂性匹配这些逻辑的已知下界。这种方法提供了一个统一的，但复杂性理论上的最佳处理分支时间时序逻辑的可满足性。它将时序逻辑机器的使用与自动机的使用分开，从而保留了输入公式和表示可满足性的对象之间的语法关系，即奇偶或Büchi游戏中的获胜策略。这里介绍的游戏只在输入公式的Fischer-Ladner闭包上工作。最后但并非最不重要的是，这里提出的游戏来尝试提供工具支持复杂的分支时间逻辑，如CTL* 和CTL+的可满足性问题。
2013-10-15 cs.LO
EXPTIME Tableaux for the Coalgebraic mu-Calculus
模态逻辑的共代数方法提供了一个统一的框架，它可以捕获结构上不同的模态逻辑的语义，包括分级和概率模态逻辑和联盟逻辑。在本文中，我们介绍了coalgebraic μ演算，一般（coalgebraic）框架的扩展与不动点算子。我们的主要结果是相关的Tableau演算的完整性和EXPTIME的可判定性守护公式。从技术上讲，这是通过将可满足性减少到非良基场景的存在来实现的，而非良基场景的存在又相当于平价博弈中获胜策略的存在。我们的结果是参数的基础类的模型和产量，作为具体的应用，以前未知的复杂性界限的概率μ演算和扩展的联盟逻辑与不动点。
2011-08-09 cs.LO math.LO
NP Reasoning in the Monotone $μ$-Calculus
单调模态逻辑的可满足性检验是NP完全的。我们表明，这仍然是真实的逻辑时，扩展与conjunctive和交替自由不动点算子以及通用模态;由此产生的逻辑-conjunctive交替自由单调$μ$ -演算与通用模态-包含并发命题动态逻辑（CPDL）和交替自由片段的游戏逻辑片段。我们得到了我们的结果，通过多项式多Eloise节点的Büchi游戏的可满足性的表征。
2020-05-04 cs.FL cs.GT cs.LO
A coherent differential PCF
本文基于无需加性的范畴框架，开发了确定性版本的微分 lambda 演算语法，作为 PCF 的微分扩展并提供了完全确定性的操作语义。
2023-10-25 cs.LO
Complete Game Logic with Sabotage
本文提出带破坏行为的博弈逻辑 GLs，通过增加设置陷阱的原语扩展 Parikh 博弈逻辑，证明其表达力与模态 μ-演算相当，并给出 Hilbert 风格证明演算的完全性。
2024-06-04 cs.GT cs.LO math.LO
The temporal logic of coalitional goal assignments in concurrent multi-player games
我们介绍和研究交替时间时序逻辑ATL的自然扩展，称为联盟目标的时序逻辑（TLCGA）。它的特点是只有一个，但很有表现力，联盟战略运营商，即联盟目标分配运营商，这是基于映射分配给游戏中的每组球员的联盟目标，形式化的TLCGA语言的路径公式，即一个公式前缀与时间运营商X，U，或G，代表相应的联盟的时间目标，描述满足该目标的策略的属性。建立了TLCGA的μ-演算扩展中时间目标分配的不动点刻画，讨论了它的表达性并举例说明，证明了它相对于适当定义的互模拟概念的互模拟不变性和Hennessy-Milner性质，构造了TLCGA的一个完善的公理系统，并通过有限模型性质得到了它的可判定性.
2022-02-22 cs.GT cs.LO cs.MA
Differential Hybrid Games
本文介绍了微分混合对策，它结合了微分对策和混合对策。在这两种博弈中，两个参与者都是以连续的动态进行互动的。不同的是，混合博弈也提供了混合系统和离散博弈的所有特征，但只有确定性微分方程。相反，微分游戏提供了两个玩家的连续时间游戏输入的微分方程，但不是混合游戏的奢侈品，如模式切换和离散时间或交替对抗互动。这篇文章增加了微分博弈逻辑与形式的微分混合博弈的组合动力学。介绍了混合对策如何超越微分对策，并引入微分对策不变量和微分对策变量来归纳证明微分对策的性质。
2017-02-24 cs.GT cs.LO cs.PL
Differential Game Logic
微分博弈逻辑（英语：Differential game logic，dGL）是一种用于指定和验证混合博弈属性的逻辑，即结合离散、连续和对抗动态的博弈。与混合系统不同，混合博弈允许系统动态中的选择由具有不同目标的不同参与者对抗性地解决。逻辑dGL可以用来研究这种混合博弈的获胜策略的存在性，即以某种方式解决玩家的选择，使他通过实现对手的所有选择而获胜。混合博弈是确定的，即从每个状态，一个玩家有一个获胜的策略，但计算他们的获胜区域可能需要很多步骤。然而，相对于任何表达逻辑，dGL逻辑有一个健全而完整的公理化。分离公理确定区分混合动力游戏混合动力系统。最后，dGL被证明是严格的表达比相应的逻辑的混合系统的表达性特征。
2015-07-24 cs.LO math.LO
Computability Aspects of Differential Games in Euclidian Spaces
我们研究微分对策的可计算性理论方面。我们的重点是在欧几里得空间中进行的追逐和规避对策，这是Rado的“狮子对人”游戏的传统。在某些方面，这些游戏可以被视为可达性游戏的连续版本。我们证明了微分对策的基本不可判定性，并研究了欧几里得空间中的追逃对策的自然类，其中获胜者可以通过可计算策略获胜。贝西科维奇为传统的“狮子对人”找到的人的获胜策略是不可计算的。我们将展示如何修改它，以产生一个可计算的非确定性获胜策略，并提出了一个问题，人类是否可以赢得一个可计算的和确定性的方式。
2019-03-02 cs.GT cs.LO math.OC
Differential games, locality and model checking for FO logic of graphs
我们介绍微分游戏FO逻辑的图形，一个变种的Escherichfeucht-Fraïssé游戏中，游戏只在一个图和移动的两个球员的限制。我们证明，在一定意义上说，这些游戏是足够强大的，以捕捉必要的信息，从图类是可解释的无处密集的图形类的图形。这一点，再加上新引入的概念，差分局部性和事实，即限制可能的移动的球员，很容易决定在某些情况下，游戏的赢家，导致一个新的方法FO模型检验问题的解释无处密集的图形类。
2020-07-22 cs.DM cs.LO math.CO
Uniform Substitution for Differential Game Logic
本文提出了一种微分对策逻辑的一致替换演算（dGL）.丘奇的统一替换在任何地方都用一个项或公式代替一个函数或谓词符号。在将它们推广到微分博弈逻辑并允许用混合博弈替换博弈符号之后，统一替换使得只使用公理而不是公理模式成为可能，从而大大简化了实现。而不是微妙的模式变量和健全的关键侧条件的逻辑变量的出现模式，以限制无限多的公理模式实例健全的，由此产生的公理化只采用了有限数量的普通dGL公式作为公理，统一的替代实例健全。本文证明了单调模态逻辑dGL的一致替换的可靠性和完备性。由此产生的公理化承认一个简单的模块化实现dGL定理证明。
2018-04-16 cs.GT cs.LO cs.PL
