Quantitative Games on Probabilistic Timed Automata
两人零和博弈是一个完善的模型，用于合成优化某些性能标准的控制器。在这样的游戏中，一个玩家代表控制器，而另一个玩家描述（对抗）环境，控制器合成对应于计算控制器在给定标准下的最优策略。Asarin和Maler通过合成控制器来优化到达最终状态的时间，从而开始了对（非概率）时间自动机的定量游戏的研究。他们的方法的正确性和终止性依赖于利用一类特殊的函数的性质，称为简单函数，可以被随机表示。在本文中，我们考虑概率时间自动机上的定量博弈。由于简单函数的概念是不足以解决游戏在这种情况下，我们概括简单的功能，所谓的准简单的功能。然后，利用这类函数，我们证明了在概率时间自动机上求解具有期望可达时间或期望折扣时间准则的博弈问题是在NEXPTIME $\cap$ co-NEXPTIME中。
2010-06-03 cs.GT cs.LO
Synthesis from Weighted Specifications with Partial Domains over Finite Words
本文从定量指标出发研究了终止反应系统的综合问题。这种系统被建模为有限换能器，其执行被表示为$(I\times O)^*$中的有限字，其中$I,O$分别是输入和输出符号的有限集合。加权规格$S$分配一个有理值（或$-\infty$）到$(I\times O)^*$中的单词，并且我们考虑三种用于合成的目标，即阈值目标，其中系统的执行被要求高于某个给定阈值，最佳值和近似目标，其中要求系统通过提供产生最佳值和$\varepsilon$的输出符号来尽可能地执行。最佳值分别为w.r.t. $S$。我们建立了一个景观的可判定性的结果，这三个目标和加权规范与部分域的有限的话，由确定性加权自动机配备和，贴现和平均措施。由此产生的目标是不定期的一般情况下，我们开发了一个无限的游戏框架来解决相应的合成问题，即（加权）关键前缀游戏类。
2021-03-09 cs.FL cs.GT cs.LO
Privacy-preserving Nash Equilibrium Synthesis with Partially Ordered Temporal Objectives
本文提出一种通信协议，在双人图博弈中综合纳什均衡，同时保护玩家私有偏序偏好，通过提前停止通信保证隐私，并证明完备性与隐私性，实验验证其有效性。
2025-10-28 cs.GT cs.LO
Quantitative games with interval objectives
传统的定量博弈，如均值-收益博弈和折扣和博弈，有两个参与者--一个试图最大化收益，另一个试图最小化收益。相关的决策问题，“Eve（最大化者）能获得正收益吗？“可以被认为是一个玩家试图在间隔$(0,\infty)$中获得回报。在本文中，我们考虑更一般的问题，确定是否一个球员可以获得支付在一个有限的联盟的任意区间的各种支付功能（liminf，平均支付，折扣和，总和）。特别是，这包括有趣的精确值问题，“Eve能否获得精确的回报（例如）0吗？"
2014-04-18 cs.GT cs.LO
Synthesis from LTL Specifications with Mean-Payoff Objectives
经典的LTL综合问题是纯定性的：给定的LTL规范是否由反应系统实现。LTL在一些定量方面的表达能力不足以形式化反应系统的正确性。本文将定性LTL合成设置扩展到定量设置。字母表的行动是扩展的权重函数范围内的有理数。无限单词的价值是其字母权重的平均回报。然后，合成问题相当于自动构建（如果可能的话）一个反应系统，其执行都满足给定的LTL公式，并具有大于或等于某个给定阈值的平均回报值。后一个问题被称为LTLMP合成和LTLMP可实现性问题要求检查是否存在这样的系统。我们首先证明了LTLMP的可实现性并不比LTL的可实现性更难：它是2 ExpTime-Complete的。这是通过减少到两个玩家的平均收益平价游戏。虽然需要无限的内存策略来实现LTLMP规范一般，我们表明，ε-最优性可以得到有限的内存策略，任何ε> 0。为了在实践中获得一个有效的算法，我们定义了一个Safraless过程来决定是否存在一个有限的内存策略，实现了给定的规格为一些给定的阈值。这个过程是基于减少到两个玩家的能源安全游戏，这反过来又减少到安全游戏。最后，我们表明，这些安全游戏可以有效地解决利用其状态空间的结构，并通过使用反链作为一个符号的数据结构。我们的所有结果扩展到多维权重。我们已经实现了一个反链为基础的程序，我们报告一些有前途的实验结果。
2013-01-09 cs.GT cs.LO
MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives
Masaryk University（马萨里克大学）；IST Austria（奥地利科学技术研究所）；University of Oxford（牛津大学）
我们提出了MultiGain，一个工具来合成多个平均回报目标的马尔可夫决策过程（MDP）的策略。我们的模型在PRISM中描述，我们的工具使用PRISM现有的接口和模拟器。我们的工具通过为多个平均收益目标添加新算法来扩展PRISM，并且还提供了以下功能：（i）生成策略并探索它们进行模拟，并检查它们的其他属性;以及（ii）为两个平均收益目标生成近似的帕累托曲线。此外，我们提出了一个新的实用算法分析的MDP与多个平均收益目标下的无记忆策略。
2015-01-13 cs.AI cs.LO
A Retraction Theorem for Distributed Synthesis
我们提出了一个一般性定理的分布式综合问题的协调对策与$ω$ -定期目标的形式：如果存在一个获胜的战略联盟，那么存在一个“本质”的获胜策略，这是通过收回给定的。一般来说，这不会导致有限状态获胜策略，但当代理的知识保持有界时，我们可以解决综合问题。我们的研究是在这样的环境中进行的，其中目标是以可能观察到\emph{not}的事件来表达的。这在不完全信息的博弈中是很自然的，而不是通常的假设，即目标是用所有主体都能观察到的事件来表达的。利用知识状态的有限性和由知识状态导出的有限同余类，研究了可判定的分布式综合问题。
2016-04-26 cs.DC cs.FL cs.GT
Optimal LTLf Synthesis
University of Liverpool（利物浦大学）
本文提出最优 LTLf 综合，通过最大化可保证实现的目标数量，解决多目标规范无法全部实现时的策略综合问题，并实验验证了方法的可行性。
2026-05-27 cs.AI cs.LO
Controller synthesis for MDPs and Frequency LTL$\setminus$GU
时态逻辑的数量扩展最近引起了人们的极大关注。在这项工作中，我们研究了频率LTL（fLTL），LTL的扩展，它允许谈论执行过程中事件的频率。这样的扩展是特别有用的概率系统，往往不能满足严格的定性保证的行为。最近已经表明，控制器的马尔可夫决策过程和fLTL的合成是可判定的，当所有的频率上的界限是1。作为一个完整的定量解决方案的一步，我们表明，该问题是可判定的片段fLTL $\setminus$ GU，其中U不发生在G的范围内（但仍然F可以）。我们的解决方案是基于一个新的翻译等定量公式到等价的确定性自动机。
2015-09-14 cs.LO
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
本文针对 MDP 中分布安全性目标难以求解的问题，提出基于模板的仿射分布归纳不变式综合框架，给出两种 PSPACE 算法，分别支持无记忆策略和一般策略，并验证了其有效性。
2023-05-26 cs.LO
Regular Games with Imperfect Information Are Not That Regular
研究不完全信息双人博弈中随机化策略的合成问题，提出正则博弈概念，证明在更一般模型中纯策略归约不适用，但在Buechi目标下随机化策略合成可判定。
2024-07-26 cs.GT cs.LO
Faster Algorithms for Mean-Payoff Parity Games
图游戏为反应过程的建模和综合提供了基础。这种游戏是在图上进行的，其中顶点由两个敌对的玩家控制。我们考虑图游戏的第一个玩家的目标是一个定性目标（指定为奇偶条件）和定量目标（指定为平均回报条件）的结合。这个问题有两种变体，即阈值问题，其中定量目标是确保平均收益值高于阈值，以及价值问题，其中定量目标是确保最佳平均收益值;在这两种情况下，都确保定性平价目标。对于具有$n$顶点、$m$边、具有$d$优先级的奇偶目标以及用于平均支付目标的最大绝对奖励值$W$的博弈图，先前最著名的算法如下：用于阈值问题的$O(n^{d+1} \cdot m \cdot W)$，以及用于值问题的$O(n^{d+2} \cdot m \cdot W)$。我们的主要贡献是更快的算法，我们的算法的运行时间如下：$O(n^{d-1} \cdot m \cdot W)$的阈值问题，和$O(n^{d} \cdot m \cdot W \cdot \log (n\cdot W))$的价值问题。对于具有两个优先级的平均收益奇偶目标，我们的算法与平均收益游戏的算法的最知名的界限相匹配（不与奇偶目标相结合）。我们的结果与具有功能要求（作为定性目标给出）和性能要求（作为定量目标给出）的反应系统的合成相关。
2017-06-19 cs.GT cs.LO
Resource-Aware Automata and Games for Optimal Synthesis
我们考虑定量的奇偶自动机和奇偶游戏的概念，旨在模拟资源感知行为，并研究（内存满）策略展示接受运行，需要最小量的初始资源，分别为赢得一个游戏，最小的初始资源。我们还展示了这样的策略可以被简化为只包括两种类型的移动：前者旨在增加资源，后者旨在满足接受条件。
2019-09-17 cs.GT cs.LO
TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments
我们提出了暴风雨，一个合成工具，自动创建正确的建设反应系统和屏蔽定性或定量的规格在概率环境中。屏蔽是一种特殊类型的用于运行时实施的反应式系统;即，屏蔽件强制执行运行系统的给定定性或定量规范，同时尽可能少地干扰其操作。执行定性或定量规范的屏蔽分别称为安全屏蔽或最优屏蔽。安全防护罩可以作为预防护罩或后防护罩来实现，最佳防护罩作为后防护罩来实现。预屏蔽放置在系统之前，并限制系统的选择。后屏蔽在系统之后实现，并且能够覆盖系统的输出。Tempest是基于概率模型检查Storm，增加了模型检验算法，用于安全和平均回报目标的随机游戏。据我们所知，Tempest是唯一一个能够解决2-1/2玩家游戏的合成工具，具有平均收益目标，而不受状态空间的限制。此外，Tempest还增加了合成安全和最佳策略的功能，这些策略实现了反应式系统和护盾
2021-05-26 cs.LO
Secure-by-synthesis network with active deception and temporal logic specifications
本文研究了具有主动网络欺骗的网络系统中的策略综合问题。网络中的主动欺骗采用诱饵系统和其他防御措施来进行防御规划，以防止已被传感系统确认的恶意攻击者的入侵。在这种情况下，防御者的目标是确保满足时序逻辑公式中指定的安全属性。我们制定的问题，欺骗性的规划与诱饵系统和其他防御作为一个两个玩家的游戏与非对称信息和布尔支付的时间逻辑。我们使用2级超博弈的时间逻辑目标，以捕捉不完整/不正确的知识的攻击者对网络系统作为一个回报的误解。真正的支付函数是防御者的私人信息。然后，我们扩展了$omega$ -正则博弈的解的概念，分析了攻击者在不完全信息下的理性策略。通过将2级超对策的解从范式推广到扩展形式，我们扩展了具有安全时序逻辑目标的对策的解，以决定防御者是否能够确保安全属性满足概率1，给定任何可能的策略，被攻击者认为是理性的.此外，我们使用的解决方案的游戏与co-safe（可达性）的时间逻辑目标，以确定是否防御者可以从事攻击者，通过引导攻击者的高保真蜜罐。所提出的综合方法的有效性说明与合成网络系统的蜜罐。
2020-02-17 cs.FL cs.GT cs.LO
Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis
在布尔合成中，我们给出了一个LTL规范，目标是构建一个转换器，在对抗环境中实现它。通常，一个规范既包含对抗性环境下应该满足的布尔需求，也包含多值组件，这些组件指的是满足的质量，并且我们希望在概率环境下最小化其预期成本。在这项工作中，我们研究，第一次，平均支付游戏中，系统的目标是在概率环境中的预期成本最小化，同时肯定满足$ω$ -经常性条件对抗的环境。我们考虑的情况下，$ω$ -正则条件是作为一个奇偶目标或由LTL公式。我们表明，在一般情况下，最优策略不需要存在，而且，极限值不能近似的有限记忆策略。因此，我们专注于计算的极限值，并给出严密的复杂性界合成$ε$ -最优策略的有限内存和无限内存的战略。我们表明，我们的游戏自然出现在各种情况下的合成与布尔和多值目标。除了直接应用之外，在与某些行为的成本和回报的合成中，它允许我们计算$ω$的最小感测成本-常规规格-一种质量度量，其中我们寻找最小化从输入读取的预期信号数量的传感器。
2016-04-24 cs.FL cs.LO
Admissibility in Quantitative Graph Games
研究了具有布尔目标的无限持续时间博弈的可容许性。我们在这里扩展这项研究的无限持续时间的定量目标的游戏。首先，我们证明了，在最优最坏情况和合作策略存在的假设下，保证存在容许策略。其次，我们使用历史的对抗值和合作值的概念给出了可容许策略的一个特征，并且我们刻画了与可容许策略相容的结果集。最后，我们展示了如何这些特征可以用来设计算法，以决定相关的验证和综合问题。
2016-11-26 cs.GT cs.LO
The Power of Counting Steps in Quantitative Games
该研究聚焦无限图上定量博弈的策略复杂度，证明有限分支场景下部分上极限收益目标可用步计数器类策略实现获胜，同时指出部分下极限总收益目标此类策略不足，完善了波莱尔层级内经典定量目标的策略复杂度结论。
2024-06-25 cs.FL cs.GT cs.LO
Ensuring Logic in the Fog: Sound POMDP Synthesis with LTL Objectives
Imperial College London（伦敦帝国理工学院）；University College London（伦敦大学学院）
本文提出一种新的可靠奖励塑造机制，用于在部分可观测马尔可夫决策过程中实现LTL目标的合成，通过增强的蒙特卡洛规划框架提升在部分可观测环境中的导航能力。
2026-05-12 cs.AI cs.FL cs.LO
Equilibria for Games with Combined Qualitative and Quantitative Objectives
Monash University（蒙纳士大学）；University of Naples “Federico II”（那不勒斯费德里科二世大学）；Sapienza University of Rome（罗马大学）；University of Sydney（悉尼大学）；University of Oxford（牛津大学）
我们的研究的总体目标是开发技术的原因多智能体系统的平衡特性。我们模型的多智能体系统作为并发游戏，其中每个球员是一个过程，被假定为独立和战略性地采取行动，追求个人喜好。在这篇文章中，我们研究这些游戏的背景下，有限记忆策略，我们假设玩家的偏好是由一个定性和定量的目标，这是相关的字典顺序：玩家首先喜欢满足其定性目标（线性时序逻辑的公式），然后更喜欢最小化成本（由平均收益函数）。我们的主要结果是，在这样的游戏中，决定一个严格的Nash纳什均衡的存在是2ExpTime完全的（因此是可判定的），即使球员的偏差实施为无限记忆策略。
2020-08-13 cs.AI cs.GT cs.LO
Beyond Winning Strategies: Admissible and Admissible Winning Strategies for Quantitative Reachability Games
University of Colorado at Boulder（科罗拉多大学波德摩尔分校）
本文研究定量可达性博弈中的可采纳策略与可采纳获胜策略，证明其历史依赖性和存在性条件，提出综合算法，并在网格世界和机器人机械臂场景中验证。
2025-06-06 cs.FL cs.GT cs.LO
MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints
Technical University of Munich（慕尼黑工业大学）；Masaryk University（马萨里克大学）
本文提出 MULTIGAIN 2.0，在 PRISM 上扩展 MULTIGAIN，支持多维长期平均奖励、稳态约束和 LTL 属性的概率系统控制器综合，并通过修改线性规划与可视化 Pareto 曲线改善多目标权衡分析。
2024-05-02 cs.AI cs.LO
Taming Large Bounds in Synthesis from Bounded-Liveness Specifications (Full Version)
从时序逻辑规范的自动合成是一个有吸引力的替代手动系统设计，由于它的能力，从高层次的规范生成正确的建设实现。由于合成问题的高度复杂性，重要的研究工作已经针对开发实际有效的方法，限制规约语言片段。在本文中，我们专注于安全LTL片段的线性时态逻辑（LTL）的语法扩展有界时态算子。我们提出了一种新的合成方法的主要动机，有效地解决了合成问题的规范与有界的时间运营商，特别是那些大的界限。我们的方法的实验评估表明，对于这种类型的规范，它优于国家的最先进的合成工具，表明它是一个很有前途的方法，有效地处理定量的时间限制在安全规范。
2023-01-24 cs.LO
Maximum Realizability for Linear Temporal Logic Specifications
基于线性时序逻辑（LTL）规范的自动综合广泛应用于机器人运动规划、自治系统控制和电网负荷分配等领域。在这样的应用程序中，一个常见的规范模式包括一个LTL公式，描述了对系统的行为的要求，以及一组额外的理想属性。我们研究的综合问题的整体规格是无法实现的设置，更准确地说，当一些理想的属性必须（暂时）违反，以满足系统的目标。我们提供了一个定量的语义集的安全规范，并使用它来正式的“尽力而为”的满足这样的软规范，同时满足硬LTL规范。我们提出了一种算法，用于合成的实现，是最佳的定量语义。我们的方法建立在有界合成方法的思想，我们开发了一个MaxSAT编码，允许最大限度地满足安全规范的定量。我们评估我们的算法从机器人和配电网络的情况。
2018-04-02 cs.LO cs.SE
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
Quantitative Assurance and Synthesis of Controllers from Activity Diagrams
本文提出面向 UML 活动图的全自动定量验证与控制器综合框架，实现到 PRISM 的语义转换及 QASCAD 工具，并通过医院机器人案例和六个文献示例验证其有效性。
2024-02-29 cs.FL cs.LO cs.SE
Deciding the synthesis problem for hybrid games through bisimulation
本文通过交替互模拟将初始化奇异混合博弈归约为时间博弈，并利用策略翻译引理，借助时间博弈工具为混合博弈合成获胜策略。
2024-09-30 cs.FL cs.LO
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
在许多合成问题中，生成不仅满足功能约束而且随机化以提高多样性、鲁棒性或不可预测性的实现是至关重要的。最近提出的控制即兴（CI）的框架提供了技术的正确的建设合成的随机系统受到硬和软的约束。然而，以前的CI工作主要集中在定性规范上，而在机器人规划和其他领域，我们通常有定量的质量指标，可以相互交易。例如，巡逻安全机器人的设计者可能想知道平均巡逻时间需要增加多少，以确保机器人路线的特定方面足够多样化，因此不可预测。在本文中，我们使这种类型的应用程序，通过推广CI问题，以支持定量软约束约束的预期值的一个给定的成本函数，和随机性约束，强制执行多样性的生成的痕迹相对于一个给定的标签功能。我们建立了标记的定量CI问题的基本理论，并开发了有效的算法来解决这些问题时，规格编码的有限自动机。我们还提供了一个近似的即兴算法的基础上约束求解任何规格编码为布尔公式。我们证明了我们的问题制定和算法的实用性与实验应用它们来产生不同的机器人规划问题的近最优计划。
2022-06-06 cs.FL cs.LO cs.SY
Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications
University of Toronto（多伦多大学）；Vector Institute（向量研究所）
综合实现逻辑规范的程序是计算机科学中的经典问题。我们研究了一种特殊类型的程序合成，其目标是合成一种策略，该策略对潜在的敌对环境做出反应，同时确保所有执行满足线性时序逻辑（LTL）规范。不幸的是，通过逻辑推理解决所谓的LTL合成的精确方法不具有规模。在这项工作中，我们铸造LTL合成作为一个优化问题。我们采用了一个神经网络学习Q函数，然后用来指导搜索，并构建程序，随后验证的正确性。我们的方法在将搜索与深度学习相结合以实现LTL合成方面是独特的。在我们的实验中，学习的Q-函数提供了有效的指导与相对较小的规格的综合问题。
2019-12-31 cs.AI cs.FL cs.GT
Quantitative Supermartingale Certificates
本文提出一种使用超鞅证书进行定量模型检查与控制综合的通用方法，通过随机不变量界定时间平移不变规约的满足概率，并提供了首个计算ω-正则与线性时序逻辑规约满足概率上下界的超鞅证书。
2025-04-07 cs.LO cs.SY eess.SY
Compiling Sufficient Governance Context from Declared Losses and Reachable States: Exact Observation-Contract Synthesis with Cardinality and Cost Objectives
Universidad Torcuato Di Tella（托卡托迪特拉大学）
本文针对有限状态模型，提出综合最小充分观察契约的方法，通过穷举或SAT/MaxSAT编码实现基数或成本目标下的精确综合，并验证充分性，实验表明方法高效且有效。
2026-09-23 cs.AI cs.LO cs.SE
Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes
Université de Mons（蒙斯大学）；Université Libre de Bruxelles（布鲁塞尔自由大学）
本文提出基于伪反链的符号算法，用于解决单调马尔可夫决策过程中的最优策略综合问题，适用于期望均值收益和随机最短路径两种量化设置，并在自动规划和LTL综合中展现出良好的性能。
2014-07-21 cs.DS cs.LO cs.SY
Full LTL Synthesis over Infinite-state Arenas
本研究提出了一种基于布尔抽象的完整LTL目标合成方法，通过CEGAR方法提升无限状态竞技场中的合成效率，优于现有最先进方法。
2025-05-27 cs.FL cs.LO cs.PL
LTL-Constrained Steady-State Policy Synthesis
Technical University of Munich（慕尼黑工业大学）
代理的决策政策往往与行为的正式规范得到满足的约束合成。在这里，我们专注于无限视界属性。一方面，线性时态逻辑（LTL）是定性规范的形式主义的一个流行的例子。另一方面，稳态政策综合（SSPS）最近受到了相当大的关注，因为它提供了一个更定量和更行为的角度来看规格，在频率与国家访问。最后，奖励为定量属性提供了一个经典框架。在本文中，我们研究马尔可夫决策过程（MDP）的规格结合所有这三种类型。所得到的策略最大化所有策略的回报，确保LTL规格与给定的概率，并坚持稳态约束。为此，我们提供了一个统一的解决方案，减少了多类型的规范，一个多维的长期平均奖励。这是由有限确定性Büchi自动机（LDBA），最近在MDP的LTL模型检验的背景下研究，并允许通过一个简单的线性程序的优雅的解决方案。该算法还扩展到一般的$ω$ -正则性质，并运行在时间多项式的大小的MDP以及LDBA。
2021-05-31 cs.AI cs.LO cs.SY
