A Game Semantics of Concurrent Separation Logic
在本文中，我们发展了一个博弈论的帐户并发分离逻辑。对于代码在环境中的每一个执行轨迹，我们都关联了一个规范游戏，其中夏娃为代码而亚当为环境而游戏。Eve和Adam的目的是将执行跟踪的每个中间机器状态分解为三部分：一部分用于代码，一部分用于环境，一部分用于可用的共享资源。我们建立健全的并发分离逻辑解释每一个派生树的逻辑作为一个获胜的策略，这个规范的游戏。
2017-10-06 cs.LO cs.PL
Designing Equilibria in Concurrent Games with Social Welfare and Temporal Logic Constraints
本文研究并发博弈中的均衡设计，通过设计激励使博弈的纳什均衡满足LTL或GR(1)时间逻辑性质，并分析了相关决策与优化问题的复杂性，为理性综合与博弈修复提供了替代方案。
2024-12-03 cs.GT cs.LO cs.MA
Strategy Improvement for Concurrent Safety Games
我们考虑图上的并发博弈。在每一轮游戏中，每个玩家同时独立地选择一步棋，这些棋步共同决定了向后继状态的过渡。两个基本目标是安全性目标：“永远停留在状态集合F中”，以及它的对偶，可达性目标，“达到状态集合R”。本文提出了一种策略改进算法，用于计算并发安全博弈的值，即参与人1执行安全目标的最大概率。该算法产生一个序列的玩家-1的策略，以确保获胜的概率，单调收敛到安全游戏的值。这一结果的意义是双重的。首先，虽然策略改进算法是已知的马尔可夫决策过程和回合制游戏，以及并发可达性游戏，这是第一个并发安全游戏的策略改进算法。其次，也是最重要的，改进算法提供了一种从下面近似并发安全博弈的值的方法（已知的值迭代算法从上面近似值）。因此，当与值迭代算法，或与可达性游戏的策略改进算法一起使用时，我们的算法导致计算可达性和安全游戏的值的收敛上界和下界的第一个实用算法。
2008-04-29 cs.GT cs.LO
Admissibility in Concurrent Games
本文研究了并发对策中随机策略的容许性概念。直觉上，一个可接受的策略是一个参与者“尽可能好地”玩的策略，因为没有其他策略支配它，即，它（几乎肯定）会战胜一组超级对抗策略。我们证明了容许策略总是存在于并发对策，我们精确地证明了他们。然后，当局中人的目标是ω-正则时，我们展示了如何进行假设容许合成，即，如何计算在其他参与人采取可接受策略的假设下（几乎肯定）获胜的可接受策略
2017-02-21 cs.GT cs.LO
Multi-player Equilibria Verification for Concurrent Stochastic Games
并发随机博弈（Concurrent Stochastic Games，CSG）是一种理想的概率系统建模方法，其特点是多个参与者或组件具有不同的目标，同时做出合理的决策。示例包括通信或安全协议和多机器人导航。存在用于CSG的验证方法，但仅限于代理或玩家被分组为两个联盟的场景，其中同一联盟中的那些共享相同的目标。在本文中，我们提出了多联盟的验证技术的CSG。我们使用子博弈完美的社会福利（或社会成本）的最优纳什均衡，这是战略，没有任何联盟单方面改变其战略在任何游戏状态，并在总的组合目标最大化（或最小化）。我们提出了一个扩展的时序逻辑rPATL（概率交替时间时序逻辑与奖励），指定任何数量的不同联盟的基于均衡的属性，和相应的模型检验算法的一个变体停止游戏。我们实现我们的技术在PRISM游戏工具，并将其应用到几个案例研究，包括秘密共享协议和公益游戏。
2020-07-24 cs.LO
Concurrent Strategies on Games with Algebras
针对信息不完全下并发博弈中玩家与对手移动的独立性，本文证明带代数博弈与常规博弈间存在双射，并扩展到中性事件，但良构双范畴的构建仍待解决。
2024-02-07 cs.GT cs.LO
Termination Criteria for Solving Concurrent Safety and Reachability Games
我们考虑图上的并发博弈。在游戏的每一轮，每个玩家同时独立地选择一步棋，这些棋步共同决定了向后继状态的过渡。两个基本目标是永远停留在一组给定状态的安全性目标，以及它的对偶，到达一组给定状态的可达性目标。本文提出了一种计算并发安全对策值的策略改进算法，即局中人1实现安全目标的最大概率。该算法产生一个序列的玩家-1的策略，以确保获胜的概率，单调收敛到安全游戏的值。我们的结果是显着的，因为策略改进算法提供了，第一次，一种方法来近似值的并发安全游戏从下面。由于值迭代算法，或可达性游戏的策略改进算法，可以用来近似相同的值从上面，这两种算法的组合产生一种方法，用于计算收敛序列的上限和下限的并发可达性和安全游戏的值。以前的方法只能从一个方向近似这些游戏的值，并且由于没有已知的收敛速度，它们没有提供解决这些游戏的实用方法。
2008-09-23 cs.GT cs.LO
Equilibrium Design for Concurrent Games
University of Oxford（牛津大学）；University of Göteborg（哥德堡大学）
在博弈论中，机制设计关注的是激励机制的设计，从而使博弈达到预期的结果。在本文中，我们研究的激励措施的设计，以便获得一个理想的均衡，例如，一个均衡满足给定的时间逻辑属性-一个问题，我们称之为均衡设计。我们的研究是基于一个框架，其中系统规范表示为时序逻辑公式，游戏作为定量并发游戏结构，玩家的目标作为平均收益目标。特别地，我们考虑由LTL和GR（1）公式给出的系统规范，并表明，只要存在这样的机制，就可以在PSPACE中实现LTL属性，在NP/ $Σ^{P}_{2}$中实现GR（1）规范。我们还研究了各种相关的决策和优化问题的复杂性，如最优性和唯一性的解决方案，并表明，所有这些问题的复杂性在于多项式层次。作为一个应用，均衡设计可以被用来作为一种替代解决方案的合理综合和验证问题的并发游戏的平均收益目标时，没有解决方案存在，或作为一种技术，以修复，只要可能，并发游戏与不理想的理性结果（纳什均衡）在一个最佳的方式。
2021-06-18 cs.AI cs.GT cs.LO
Concurrent Separation Logic Meets Template Games
并发理论和程序设计语言语义学的一个古老梦想是揭示基本的同步机制，这些机制调节的情况与高阶程序的游戏语义和具有共享内存和锁的并发程序的霍尔逻辑一样不同。在本文中，我们建立了一个深刻的和意想不到的连接最近的两条工作线并发分离逻辑（CSL）和差分线性逻辑（DiLL）的模板游戏语义。由于这种联系，我们重新制定了纯粹的概念风格的模板游戏为迪尔的异步和交互式的解释CSL设计的梅利斯和Stefanesco。我们相信，分析揭示了一些重要的秘密解剖CSL，更具体地说，微妙的相互作用，分类性质，顺序组成，并行产品，错误和锁之间。
2020-05-09 cs.LO cs.PL
Correlated Equilibria and Fairness in Concurrent Stochastic Games
博弈论技术和均衡分析促进了竞争系统的设计和验证。虽然均衡计算的算法复杂性已被广泛研究，但博弈论方法的实际实现和应用是最近才出现的。工具，如PRISM游戏支持自动验证和合成的零和和（ε-最优子博弈完美）社会福利纳什均衡性能并发随机游戏。然而，这些方法变得效率低下的代理人的数量增长，也可能产生的均衡，产生显着的变化，个别代理人的结果。相反，我们考虑相关的均衡，其中玩家可以通过公共信号进行协调，并引入一个替代的社会公平的最优性标准，它可以应用于纳什均衡和相关均衡。我们发现，相关的均衡更容易计算，更公平，也可以改善联合结果。我们实现了范式游戏和更复杂的情况下，多玩家并发随机游戏的时间逻辑规范的算法。
2022-02-01 cs.GT cs.LO
Pure Nash Equilibria in Concurrent Deterministic Games
我们研究纯策略纳什均衡在多个玩家并发确定性游戏，各种偏好关系。我们提供了一种新的结构，称为嫌疑人游戏，它将多玩家并发游戏转换为两个玩家回合制游戏，将纳什均衡转化为获胜策略（对于某些目标，取决于原始游戏中玩家的偏好关系）。我们使用这种转换来设计算法计算纳什均衡在有限的游戏，在大多数情况下有最佳的最坏情况下的复杂性，为大类的偏好关系。这包括纯粹的定性框架，其中每个参与者都有一个单一的欧米伽规则目标，她想满足，但也有更大的类半定量目标，其中每个参与者有几个欧米伽规则目标配备了一个前序（例如，一个参与者可能想满足她的所有目标，或最大化她实现的目标数量）。
2015-06-18 cs.GT cs.LO
Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games
随机博弈的概率模型检验使得能够对包括在随机环境中操作的竞争或协作实体的系统进行形式化验证。尽管在这一领域取得了良好进展，但现有办法侧重于零和目标，无法对赋予各实体不同目标的情景进行推理。在本文中，我们提出了基于纳什均衡的并发随机博弈的概率模型检验技术。我们扩展的时序逻辑rPATL（概率交替时间时序逻辑与奖励），让推理的球员与不同的定量目标，捕捉事件发生的概率或奖励措施。我们提出的算法来合成策略，是子博弈完美的社会福利最优纳什均衡，即，在游戏的任何状态下，没有任何玩家单方面改变策略的激励，同时组合概率或奖励最大化。我们实现我们的技术在PRISM游戏工具，并将其应用到几个案例研究，包括网络协议和机器人导航，显示的好处相比，现有的方法。
2019-07-08 cs.LO
Representation Theorems for Actual Powers over Two-Agent General Concurrent Game Frames
Institute for Logic, Language and Computation, University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）；Beijing Normal University（北京师范大学）；University of Bergen（卑尔根大学）；Shanxi University（山西大学）
本文针对双主体一般并发博弈框架，证明八类框架可由对应邻域框架表示，推广了van Benthem等人的相关结果，解决了标准并发博弈框架假设过强的问题。
2026-10-14 cs.GT cs.LO cs.MA
The Complexity of Pure Strategy Relevant Equilibria in Concurrent Games
本文研究并发博弈中满足社会福利或帕累托最优条件的纯策略纳什均衡的存在性复杂性，证明社会福利条件与受约束纳什均衡问题计算效率相同，而帕累托条件通常上界更高，但在 Büchi 和 Muller 博弈中分别属于 P 类和 PSPACE-complete。
2025-09-22 cs.CC cs.FL cs.GT
The Qualitative Collapse of Concurrent Games (Extended Version)
CNRS, Aix Marseille Univ, LIS（法国国家科学研究中心，艾克斯马赛大学，LIS）
本文构建了从并发博弈范畴到 Scott 域范畴的保解释函子，通过组合引理同步策略状态，为定性-定量对应关系提供了新的具体证明。
2026-10-27 cs.LO
Concurrent games and semi-random determinacy
考虑在图上进行的并发、无限持续时间、两人赢/输游戏。如果获胜条件满足一些简单的要求，则参与人1获胜（有限记忆）策略的存在性等价于许多派生的一人博弈中获胜（有限记忆）策略的存在性。几个经典的获胜条件满足这个简单的要求。在对获胜条件的附加要求下，参与人1不存在从所有顶点获胜的策略等价于参与人2存在几乎必然从所有顶点获胜的随机策略.只有少数经典的获胜条件满足这个额外的要求，但一个公平的变体o
2018-04-29 cs.FL cs.GT cs.LO
Focusing in Asynchronous Games
博弈语义学提供了一个互动的观点证明，这使得人们能够精确地描述他们的动态行为，在削减消除，考虑公式作为游戏的证明诱导策略。我们特别感兴趣的是在这里有关两个这样的语义线性逻辑，非常不同的味道，这两个考虑到并发功能的证明：异步游戏和并发游戏。有趣的是，我们表明，关联的并发策略的异步策略可以被看作是一个语义对应的线性逻辑的聚焦属性。
2010-04-19 cs.GT cs.LO
The Quantitative Collapse of Concurrent Games with Symmetry
我们探讨薄并发游戏的Castellan，Clairambault和Winskel之间的联系，和加权的线性逻辑研究的关系模型莱尔德，Manzonetto，McCusker和帕加尼。更确切地说，我们表明，有一个interpretationpreserving“崩溃”函子从前者到后者。在对象上，函子为每个游戏定义了一组可能的执行状态。定义对态射的作用更加微妙，这是本文的主要贡献。给定一个策略和一个执行状态，我们的函子需要在策略中计算这个状态的见证者。瘦并发博弈中的策略明确地描述了非线性行为，因此一般来说每个见证人存在于可数个对称副本中。挑战在于定义证人的正确概念，在匹配加权关系模型的同时分解出这种无限性。了解证人如何组成是特别微妙的，需要深入研究证人及其对称性的组合学。在其基本形式中，该函子连接瘦并发游戏和由N $\cup$ {+ $\infty$ }加权的关系模型。我们还将考虑一个广义的设置，其中两个模型都加权的任意连续半环的元素，这涵盖了概率的情况下，等等。见证人现在额外地携带来自半环的值，并且我们的解释保持崩溃函子扩展到这种设置。
2021-07-07 cs.LO cs.PL
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
Automatic Verification of Concurrent Stochastic Systems
随机游戏的自动验证技术允许对系统进行正式推理，这些系统具有不确定或概率设置中理性代理之间的竞争或协作行为。现有的工具和技术集中于回合制游戏，其中游戏的每个状态由单个玩家控制，以及零和属性，其中两个玩家或联盟具有直接相反的目标。在本文中，我们提出了并发随机游戏（CSG）的自动验证技术，它提供了一个更自然的并发决策和交互模型。我们还考虑（社会福利）纳什均衡，正式确定的情况下，两个球员或联盟有不同的目标可以合作，以优化他们的联合表现。我们提出了一个扩展的时间逻辑rPATL在这种情况下指定的定量属性，并提出相应的算法验证和策略合成的变体停止游戏。对于有限时域的性质，计算是精确的，而对于无限时域，它是近似使用值迭代。对于零和性质，它需要通过线性规划来求解矩阵博弈，对于基于均衡的性质，我们通过SMT编码的标记多面体方法来找到双矩阵博弈的社会福利或社会成本纳什均衡。我们在PRISM游戏中实现了这种方法，这需要扩展工具的建模语言用于CSG，并将其应用于包括机器人技术，计算机安全和计算机网络在内的领域的案例研究，明确展示了CSG和基于平衡的属性的好处。
2020-08-29 cs.LO
From Thin Concurrent Games to Generalized Species of Structures (Extended Version)
Aix Marseille Univ, CNRS, LIS（艾克斯马赛大学，法国国家科学研究中心，信息系统实验室）；Inria, École Normale Supérieure – PSL, CNRS（法国国家信息与自动化研究所，巴黎高等师范学校-PSL大学，法国国家科学研究中心）
本文在线性逻辑的薄并发博弈动态模型与结构广义物种静态模型间构建形式化桥梁，通过双范畴刻画二维关系，构造对称幺半函子并调整博弈语义方法得到笛卡尔闭伪函子，为λ演算研究提供新视角。
2025-10-27 cs.LO
Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games
Technical University of Munich（慕尼黑技术大学）；Masaryk University（马萨里大学）；Ruhr-University Bochum（波鸿鲁尔大学）
针对并发随机博弈中的值迭代，提出有界（区间）值迭代方法，通过补充上近似序列并基于上下近似ε-接近的停止准则，确保近似精度。
2025-09-10 cs.AI cs.LO cs.MA
Antichains for Concurrent Parameterized Games
Universit\'e de Rennes, Inria, CNRS, IRISA, Rennes, France；LMF, CNRS \& ENS Paris-Saclay,\ \'e Paris-Saclay, Gif-sur-Yvette, France
针对并发参数化可达性博弈的Eve获胜区域问题，提出基于反链的符号方法及两个不动点算法，实现后在基准测试中验证了性能。
2026-10-09 cs.LO
Incentive Engineering for Concurrent Games
本文研究并发博弈中通过静态或动态征税方案激励多智能体实现LTL目标的问题，分析委托人能否使目标在均衡策略下至少一条或所有运行路径上满足，并探讨模型博弈论性质与决策问题计算复杂性。
2023-07-11 cs.GT cs.LO cs.MA
Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games (Full Version)
本文研究并发多玩家平均收益博弈，引入合作博弈理论的核心作为解概念，利用离散几何刻画其非空性并证明多项式见证者的存在，进而解决理性验证决策问题并给出紧致复杂度界限。
2023-11-27 cs.FL cs.GT cs.LO
Thin Games with Symmetry and Concurrent Hyland-Ong Games
本文基于事件结构构建笛卡尔闭范畴Cho，以精细解释高阶有状态并发程序，兼具Hyland-Ong博弈的保守性与更强表达力，并应用于理想化并行Algol。
2019-03-01 cs.LO math.LO
Concurrent Games over Relational Structures: The Origin of Game Comonads
该研究提出将Spoiler-Duplicator博弈视为事件结构的新框架，给出单边博弈共代数的通用构造方法，刻画双边博弈策略，为有限模型理论提供范畴论新工具。
2025-06-14 cs.LO cs.PL math.CT
Logics and Games for True Concurrency
我们研究了基于过渡系统，Petri网和事件结构的各种偏序模型的并发性的基本数学性质，并表明这些系统的并发行为可以通过两个简单的和一般的对偶局部行为以统一的方式捕获。这种对偶性被用来定义新的μ演算和逻辑游戏，用于分析具有偏序语义的并发系统。这项工作的一些结果是：一些mu-演算的定义，在某些类的系统，诱导相同的标识作为一些最有名的互模拟等价的并发性;和定义（无限）高阶逻辑游戏的互模拟和模型检查，其中的球员的游戏给予（本地）一元二阶权力的一组元素，他们被允许发挥。更具体地说，我们表明，我们的游戏是健全的和完整的，因此，确定;此外，它们是可判定的有限情况下，并支持新的决策程序的互模拟和模型检查。由于这些mu演算和逻辑游戏概括了著名的不动点逻辑和博弈论决策程序的并发系统与交织语义，本文的结果给出了一些基础的设计一个基于逻辑的，博弈论的框架研究，在一个统一的方式，几个并发系统，无论他们是否有交织或偏序语义。
2010-11-04 cs.LO
The Complexity of Concurrent Rational Synthesis
在本文中，我们研究了合理的合成问题的并发博弈结构的各种目标，从可达性的Muller条件。我们提出了一个新的算法，建立了非合作的理性综合问题，完全依赖于博弈论技术，而不是以前的方法，是基于逻辑的可判定性。由于这种方法，我们构建了一个零和回合制游戏，可以适应上述每一个目标，从而获得新的复杂性结果。特别是，我们表明，可达性，安全性，Büchi，和合作Büchi条件是PSpace完全的，穆勒，街，和拉宾是PSpace硬和ExpTime。
2018-06-08 cs.GT cs.LO
Antichains for Concurrent Parameterized Games (Long Version)
Université de Rennes, Inria, CNRS, IRISA（雷恩大学，Inria，CNRS，IRISA）；LMF, CNRS & ENS Paris-Saclay, Université Paris-Saclay（LMF，CNRS 与巴黎萨克雷高等师范学院，巴黎萨克雷大学）；Nantes Université, École Centrale Nantes, CNRS, LS2N（南特大学，南特中央理工学院，CNRS，LS2N）
针对并发参数化博弈，提出基于反链的符号方法计算知识博弈中Eve的获胜区域，给出最小知识需求，并实现两种不动点算法与性能对比。
2026-09-07 cs.GT cs.LO
Strategy Complexity of Concurrent Stochastic Games with Safety and Reachability Objectives
我们考虑有限状态并发随机博弈，由k>=2个参与者进行无限轮的博弈，其中在每一轮中，每个参与者同时且独立于其他参与者选择一个行动，此后，后继状态由当前状态和所选择的行动给出的概率分布确定。我们认为可达性目标，给定的目标集的状态要求，在目标中的一些状态被访问，和双重安全目标，给定的目标集要求，只有在目标集中的状态被访问。我们感兴趣的是固定策略的复杂性，衡量他们的耐心，这是定义为最小的非零概率的倒数。我们的主要结果如下：我们证明了在两人零和并发随机对策中，（一个局中人的可达性目标和另一个局中人的互补安全目标）：（i）对于两个局中人，最优策略和ε-最优策略的耐心的最优界都是双指数的;和（ii）即使在一个单一的非吸收状态指数（在行动的数量）耐心的游戏是必要的。在一般情况下，我们研究类的非零和游戏承认固定的ε-纳什均衡。我们证明了如果至少有一个局中人具有可达性目标，那么双指数耐心可能是必需的双-纳什均衡策略，而与此相反，如果所有局中人都具有安全目标，则双-纳什均衡策略的最优耐心界限仅是指数的。
2015-06-08 cs.GT cs.LO
Finite-horizon Equilibria for Neuro-symbolic Concurrent Stochastic Games
我们提出了新的技术，神经符号并发随机游戏，最近提出的建模形式主义表示一组概率代理人在连续空间环境中使用组合的神经网络为基础的感知机制和传统的符号方法。迄今为止，只研究了该模型的零和变体，当代理人有明确的目标时，这是过于限制性的。我们正式这些模型的平衡概念，并提出算法来合成它们。集中在有限时域设置，（全球）社会福利子博弈完美的最优性，我们考虑两种不同的类型：纳什均衡和相关均衡。我们首先表明，一个精确的解决方案的基础上逆向归纳可能会产生任意坏的平衡。然后，我们提出了一个近似算法冻结子博弈改进，通过迭代求解非线性规划。我们开发了一个原型实现，并证明了我们的方法的好处，两个案例研究：自动停车场系统和飞机防撞系统。
2022-06-18 cs.GT cs.LO
Robust Verification of Concurrent Stochastic Games
Department of Computer Science, University of Oxford, Oxford OX1 2JD, UK（计算机科学系，牛津大学，牛津 OX1 2JD，英国）
本文提出鲁棒并发随机游戏模型及验证框架，用于处理多智能体系统中转移概率的不确定性问题。
2026-01-21 cs.AI cs.GT cs.LO
Reachability and Safety Games under TSO Semantics
该研究针对TSO弱内存模型下并发程序的可达性与安全博弈，证明其可归约为单进程程序分析且为有限状态，引入公平性约束后两类问题均变为不可判定。
2024-10-30 cs.LO
Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems
Rice University（莱斯大学）
本文研究有限视界概率多智能体并发博弈系统中给定策略配置是否为纳什均衡或子博弈完美均衡的验证问题，发现子博弈完美均衡验证属于PSPACE，而纳什均衡验证为EXPTIME完全，这一反直觉结果表明子博弈完美均衡验证可能更简单。
2026-05-19 cs.GT cs.LO
Robust PAC Learning of Concurrent Stochastic Games
University of Oxford（牛津大学）
提出带转移不确定性的一般和并发随机博弈的鲁棒PAC学习框架，通过维护转移核置信集、引入纳什边际特征，在满足可达性条件下以多项式样本复杂度终止，基准博弈实验验证其性能与理论一致性。
2026-10-08 cs.GT cs.LG cs.LO
Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics
Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004（南特大学，中央理工学院南特分校，法国国家信息与自动化研究所，LS2N实验室）
本文建立λ演算的π演算编码与操作博弈语义的紧密联系，推导其等价关系一致性，实现结果与技术双向转移，得到新行为等价关系及完全抽象结果，并针对按值调用与按名调用展开说明。
2026-10-07 cs.LO
How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract)
我们提出了一个逻辑框架，结合了对多人博弈中代理人通过优化收益或结果偏好来实现定量目标的能力的博弈论研究，以及对玩家实现玩家定性目标的能力的逻辑分析，即，达到或保持具有期望属性的游戏状态。我们丰富的并发游戏模型与支付的范式游戏与模型的状态，并提出了一个定量扩展的逻辑ATL*，使定量和定性推理相结合。
2013-03-04 cs.LO cs.MA
Qualitative Concurrent Stochastic Games with Imperfect Information
我们研究了一个模型的游戏，结合并发性，不完美的信息和随机方面。这些是有限状态博弈，在每一轮中，两个参与者同时独立地选择一个行动。然后，根据前一个状态和参与者选择的一对行动，根据某个固定的概率分布来选择后继状态。不完全信息模型如下：两个玩家在状态上有一个等价关系，而不是观察确切的状态，他们只知道它属于哪个等价类。因此，如果某个参与者无法区分两种局部策略，那么他在这两种策略中的行为应该是相同的。我们考虑可达性（戏剧最终会访问最终状态吗？）和Büchi目标（是否发挥访问无限经常一个最终状态？）。我们的主要贡献是证明了以下问题是2-ExpTime完全的：决定第一个玩家是否有一个策略，确保她几乎肯定会赢得任何可能的策略，她oponent。我们还讨论了第一个几乎肯定会赢的玩家所需要的策略。
2011-08-30 cs.FL cs.GT cs.LO
Reachability and Safety Games under TSO Semantics (Extended Version)
研究TSO弱内存模型下并发程序迁移图上的双人博弈，证明其可达性与安全问题可归约为有限状态的单进程分析，但引入公平性概念后这两个问题均变得不可判定。
2024-06-04 cs.GT cs.LO
Operational Semantics of Games
我们将操作语义引入到游戏中。基于操作语义，建立了一个完整的博弈代数，包括基本博弈代数、并发博弈代数、递归和抽象。在博弈论的支持下，代数可以广泛用于系统（不仅是计算系统）行为的推理。
2019-09-03 cs.LO
Big, but not unruly: Tractable norms for anonymous game structures
我们提出了一个新的战略逻辑NCHATL，允许推理规范遵守并发游戏结构，满足匿名性。我们代表这样的游戏结构competencies，避免模型，有指数大小的代理人的数量。然后，我们表明，模型检验可以在多项式时间就这个紧凑的表示，即使是规范的系统，不是匿名的。也就是说，只要潜在的游戏结构是匿名的，模型检验规范公式是易于处理的，即使规范可以规定不同的禁止行为集不同的代理。
2014-05-27 cs.LO cs.MA
Synthesizing safe coalition strategies
具有固定数量的代理的并发游戏已经被深入研究，各种解决方案的概念和目标的代理。在本文中，我们考虑并发游戏与任意数量的代理，并研究了问题的合成联盟战略，以实现全球安全目标。这个问题是不平凡的，因为代理人不知道先验有多少，他们是当他们开始游戏。我们证明了安全目标的安全任意大联盟策略的存在性是一个PSPACE困难问题，可以在指数空间中决定。
2020-09-30 cs.LO
Games and Strategies as Event Structures
在2011年，Rideau和Winskel引入了并发博弈和策略作为事件结构，推广了先前关于博弈因果公式的工作。在本文中，我们给出了一个详细的，自包含的和略有更新的帐户的结果Rideau和Winskel：一个概念的前战略的基础上的事件结构;这些前战略的表征（视为战略），这是保留的组合与模仿策略;和建设的双范畴的这些战略。此外，我们证明了相应的范畴有一个紧凑的封闭结构，从而形成了并发高阶计算的语义的基础。
2017-09-27 cs.LO math.LO
Concurrent Strategies as Street Fibrations
Inria（法国国家数字技术研究所）；École Normale Supérieure Paris（巴黎高等师范学院）；Queen Mary University of London（伦敦大学玛丽女王学院）
本文刻画了并发博弈中两类具有恒等元的策略，证明弱等价类恰为诱导Street纤维化的策略，并建立了博弈与集合值预层范畴的联系。
2026-11-03 cs.LO math.CT
Effectful Semantics in Bicategories: Strong, Commutative, and Concurrent Pseudomonads
本文在双范畴中建立强、交换及并发伪幺半群理论，用弱交换律统一描述并行与顺序复合，并通过并发博弈语义的延续伪幺半群展示其效应语义价值。
2024-06-11 cs.LO math.CT
Learning to Count up to Symmetry
在本文中，我们开发的理论，如何计数，在薄并发游戏，配置的策略，见证它达到一定的配置的游戏。这在并发博弈的许多最新发展中起着核心作用，每当一个人的目标是将并发策略与加权关系模型联系起来时。当然，困难在于对称性：在对称性存在的情况下，策略的许多配置在道德上是相同的不同实例，只是在复制索引的非本质选择上有所不同。我们怎么知道该算哪一个？本文的目的是澄清这一点，揭示许多奇怪的现象和迷人的病理学例子。为了说明结果，我们表明，一个简单的加权关系模型简单计数证人的崩溃操作下的组合，提供的策略不死锁。
2020-06-09 cs.LO cs.PL
Nash Equilibrium and Bisimulation Invariance
本文发现标准策略模型下互模拟不保持纳什均衡存在性，提出三种保持该性质的策略模型，为策略推理逻辑提供新语义基础并研究受限场景。
2019-09-19 cs.LO
Effect-Dependent Transformations for Concurrent Programs
我们描述了一个指称语义的抽象效果系统的高阶，共享变量并发程序设计语言。我们证明了一些一般的基于效果的程序等价物的合理性，包括并行化方程，该方程指定了用并行组合物替换顺序组合物的充分条件。效果注释是相对于由合约指定的抽象位置而不是物理足迹，这使我们特别能够显示涉及细粒度并发数据结构（例如Michael-Scott队列）的某些转换的可靠性，这些转换允许并发访问可变数据结构的不同部分。我们的语义是基于改进的痕迹为基础的语义的一阶程序，由于布鲁克斯。通过从具体位置移动到抽象位置，并添加类型细化来捕获表达式及其并发环境的可能副作用，我们能够验证许多在未细化模型中不存在的等价性。类型的含义是使用基于游戏的逻辑关系在轨迹集上表达的。两个程序$e_1$和$e_2$是逻辑相关的，如果一个程序能够解决一个两人游戏：对于任何轨迹，结果值$v_1$在$e_1$（挑战）的语义中，玩家提出，对手可以提出一个（响应）等价的轨迹，在$e_2$的语义中，具有逻辑相关的结果值$v_2$。
2015-10-08 cs.LO cs.PL
Relaxing Exclusive Control in Boolean Games
IBISC, Université d’Evry（埃夫里大学 IBISC 实验室）；IRIT, CNRS, Toulouse（图卢兹 IRIT 实验室，法国国家科学研究中心）；IRIT, University of Toulouse（图卢兹大学 IRIT 实验室）
在布尔博弈（BG）的典型框架中，每个参与者都可以改变一些命题原子的真值，同时试图使她的目标为真。在标准BG目标是命题公式，而在迭代BG目标是线性时态逻辑的公式。BG的这两个概念的特征在于代理对它们的原子集具有排他性控制，这意味着没有两个代理可以控制同一个原子。在目前的贡献，我们放弃了排他性的假设，并探讨结构中，一个原子可以由多个代理控制。我们介绍了具有共享命题控制的并发博弈结构（CGS-SPC），并证明了它们可用于几类重复博弈，包括迭代布尔博弈、影响博弈和聚合博弈。我们的主要结果表明，就验证而言，CGS-SPC可以归结为具有排他控制的并发博弈结构。这一结果为CGS-SPC上的交替时序逻辑规范的模型检验问题提供了一个多项式约简。
2017-07-27 cs.AI cs.LO
Strategy Synthesis for Zero-Sum Neuro-Symbolic Concurrent Stochastic Games
University of Oxford（牛津大学）；University of Glasgow（格拉斯哥大学）
针对神经符号系统正确性验证需求，提出神经符号并发随机博弈模型，证明零和折扣奖励下价值函数性质，首次给出两类实用迭代算法求解该连续状态博弈子类的价值与策略合成问题。
2024-07-11 cs.AI cs.GT cs.LO
A minimal coalition logic
IRIT-CNRS, University of Toulouse, France（法国图卢兹大学IRIT-CNRS研究中心）；School of Philosophy, Beijing Normal University, China（北京师范大学哲学学院）
本文提出并证明了一个基于无串行性、独立性和确定性假设的一般并发博弈模型的极简联盟逻辑的完备性，用于推理联盟权力。
2025-09-11 cs.AI cs.LO
Asynchronous Agents with Perfect Recall: Model Reductions, Knowledge-Based Construction, and Model Checking for Coalitional Strategies
KTH Royal Institute of Technology（皇家理工学院）；Institute of Computer Science, Polish Academy of Sciences（波兰科学院计算机科学研究所）；Faculty of Mathematics and Computer Science, Nicolaus Copernicus University（尼古拉·哥白尼大学数学与计算机科学学院）
针对有记忆智能体策略能力的模型检测难题，本文证明偏序归约可推广至有记忆情形，并改造基于知识的子集构造以适用于异步MAS，同时提出融合并发博弈结构与交错解释系统的新策略执行语义。
2025-10-20 cs.LO cs.MA
Game Semantics: Easy as Pi
游戏语义已被证明是一种强大的方法，为各种高阶程序设计语言提供组合语义。然而，由于大多数游戏模型的复杂性，游戏语义仍然是非专家难以接近。在本文中，我们的目标是使游戏语义更容易通过查看它作为一个句法翻译成会话类型的π演算，被称为元语言，其次是一个特定的游戏模型的元语言的语义解释。可以为各种各样的程序设计语言定义语法转换，而不需要知道所使用的特定游戏模型。对模型的简单推理（可靠性和充分性）可以在元语言级别完成，避免了通常在游戏语义中发现的繁琐的技术证明。我们称这种方法为编程游戏语义。我们设计了一个元语言（PiDiLL）的灵感来自差分线性逻辑（DiLL），这是简洁的，但表达能力足以支持并发游戏语义所需的功能。然后，我们证明了我们的方法，产生的第一个因果关系，非天使和交互式的CML，一个高阶调用的共享内存并发的值的语言的游戏模型。我们将CML翻译成PiDiLL，并表明翻译是足够的。我们给出了一个因果和非天使的游戏语义模型，使用事件结构，它支持一个简单的语义解释的PiDiLL。结合这两个结果，我们得到的第一个交互式模型的并发语言的这种表现力是足够的标准弱互模拟，并充分抽象的上下文等价的二阶项。我们已经实现了一个原型，可以探索产生的因果对象从一个子集的OCaml。
2020-11-10 cs.LO cs.PL
