Optimal Strategy Synthesis for Request-Response Games
Florian Horn, Wolfgang Thomas, Nico Wallmeier, Martin Zimmermann
我们的存在性和有效的可计算性的最佳获胜策略的请求-响应游戏的情况下，发挥的质量是衡量的极限优越的平均累积等待时间之间的请求和他们的反应。
We show the existence and effective computability of optimal winning strategies for request-response games in case the quality of a play is measured by the limit superior of the mean accumulated waiting times between requests and their responses.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
2.5玩家平价游戏结合了2.5玩家可达性游戏和平价游戏的定性分析所带来的挑战。这两种类型的问题最好用不同类型的算法来处理：2.5玩家可达性游戏的策略改进算法和奇偶游戏定性分析的递归算法。我们提出了一种方法，与现有的技术相比，解决这两个方面的最适合的方法，并专门在2.5玩家游戏本身。由此产生的技术足够强大，可以处理数百万个状态的游戏。
Deciding the synthesis problem for hybrid games through bisimulation
本文通过交替互模拟将初始化奇异混合博弈归约为时间博弈，并利用策略翻译引理，借助时间博弈工具为混合博弈合成获胜策略。
Opportunistic Synthesis in Reactive Games under Information Asymmetry
反应式合成是一类在动态和不可控环境下，相对于时序逻辑规范来构造可证明正确的控制系统（称为机器人）的方法。这是通过将机器人与其环境之间的交互建模为两人零和游戏来实现的。然而，现有的反应合成方法假设双方都有完整的信息，这是不是在许多战略互动的情况下。在本文中，我们使用一个变种的超博弈模型的机器人和它的环境之间的相互作用，其中有不完整的信息，机器人的规格。该模型允许我们识别游戏状态的子集，机器人可以利用不对称信息来实现更好的结果，如果两个玩家都有对称和完整的信息，这是不可能的。然后，我们介绍了一种新的方法，机会合成定义一个马尔可夫决策过程（MDP）下的超博弈时序逻辑规范。当环境中发挥一些随机策略，在其认为肯定赢，肯定输的游戏区域，我们表明，通过以下的机会主义策略，机器人是确保只有改善游戏的结果-测量子规格的满意度-每当有机会成为可用。我们证明了这种方法的正确性和最优性使用机器人运动规划的例子中存在的对手。
Non-Zero Sum Games for Reactive Synthesis
在这邀请的贡献，我们总结了新的解决方案的概念，有用的合成反应系统，我们已经介绍了在最近的几个出版物。这些解决方案的概念是在非零和游戏的背景下发挥图形。它们是在欧洲研究理事会资助的投资项目中获得的部分捐款。
Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis
针对基于Manna-Pnueli层级的LTLfp和PPLTLp逻辑，提出首个反应式综合求解器：基于Emerson-Lei博弈的符号求解器及原生嵌入目标的Manna-Pnueli博弈求解器，实验证明后者常更高效，结合两者可提升性能。
Controller Synthesis for Parametric Timed Games
本文提出一种半算法，用于计算参数化时间博弈中的获胜策略，并将其转换为参数化时间自动机以构建控制器，通过生产单元案例验证了可行性。
Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games
我们通过超越最坏情况来扩展定量合成框架。一方面，两人博弈的经典分析涉及对手（模拟系统的环境），这是纯粹的对抗性，并要求严格的保证。另一方面，像马尔可夫决策过程这样的随机模型代表了系统面临纯随机环境的情况：目标是优化预期收益，而不保证个人结果。我们引入超越最坏情况的综合问题，这是构建策略，保证在最坏的情况下的一些定量要求，同时提供一个更高的期望值对一个特定的随机模型的环境作为输入。这个问题与生产在日常情况下提供良好的预期性能的系统控制器有关，同时即使在非常糟糕（虽然不太可能）的情况下也确保严格（但宽松）的性能阈值。本文研究了两个重要的定量设置：平均收益和最短路径的超最坏情况综合问题，在这两种情况下，我们展示了如何判断满足该问题的有限记忆策略的存在性，以及如何综合一个，如果存在的话。我们建立算法，我们研究的复杂性界限和内存要求。
Security-Aware Synthesis Using Delayed-Action Games
本文提出了一种基于延迟动作游戏（DAG）的策略合成和分析框架，用于解决多智能体反应系统中隐藏信息游戏的建模问题，并展示了该框架在无人 aerial 车系统面临隐蔽攻击时的应用。
Towards Efficient Controller Synthesis Techniques for Logical LTL Games
本文将经典有限状态不动点算法扩展到符号逻辑 LTL 博弈，并在 GenSys-LTL 中实现，可计算最大获胜区域与最大宽容控制器，相对现有方法取得46.38倍加速。
Synthesis of Deceptive Strategies in Reachability Games with Action Misperception (Technical Report)
战略欺骗是一种操纵对手感知以获得战略优势的行为。本文研究了行动集信息单侧不完全的图上两人回合制零和可达博弈中欺骗性获胜策略的合成问题。特别是，我们考虑一类游戏中，玩家1（P1）开始与一个非空的私人行动，她可能会“透露”的玩家2（P2）在游戏过程中。P2配备了一个推理机制，每当一个新的动作被揭示时，他就会更新他对P1的动作集的感知。在这种信息结构下，P1的目标是达到博弈图中的一组目标状态，而P2的目标是阻止它。我们解决的问题是：P1如何利用她的信息优势来欺骗P2选择反过来有利于P1的行动？为此，我们引入了一个动态的超博弈模型来捕捉可达性游戏与不断发展的误解P2。通过对博弈的定性分析，我们设计了合成欺骗性必胜区和几乎必胜区的算法，得到了两个关键结果：（1）在必胜条件下，欺骗性必胜策略与非欺骗性必胜策略是等价的--即使用欺骗手段没有优势;（2）在几乎必胜条件下，欺骗性必胜策略可能比非欺骗性必胜策略更有效。我们说明了我们的算法使用一个捕获的旗帜游戏，并演示了使用所提出的方法，以更大的一类游戏的时间逻辑目标。
Church Synthesis on Register Automata over Linearly Ordered Data Domains
本文研究线性有序数据域上寄存器自动机规范的Church综合，提出单侧Church博弈并证明其可判定性（ExpTime），并应用于换能器综合。
Control strategies for off-line testing of timed systems
部分能观性和部分能控性是交互系统测试用例综合中的两个重要问题。我们解决的问题，部分控制的测试用例的合成时间自动机规格。tioco定时测试框架的基础上，我们扩展了以前的游戏解释的测试合成问题，从不定时的定时设置。这种扩展需要对模型、游戏解释和测试合成算法进行深度改造。我们展示了一个游戏的策略，试图尽量减少控制损失和距离，以满足测试目的，并证明他们在一些公平的假设下获胜。这意味着，当把这些策略转化为测试用例时，我们得到了测试合成方法的可靠性和穷举性等属性。
On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version)
针对参数化时间博弈的可达性获胜参数综合问题，本文调整实现 On-The-Fly 算法并引入剪枝启发式，通过两个大型案例验证可行性，且证明其在极限下可给出全部正确参数取值。
Secure-by-synthesis network with active deception and temporal logic specifications
本文研究了具有主动网络欺骗的网络系统中的策略综合问题。网络中的主动欺骗采用诱饵系统和其他防御措施来进行防御规划，以防止已被传感系统确认的恶意攻击者的入侵。在这种情况下，防御者的目标是确保满足时序逻辑公式中指定的安全属性。我们制定的问题，欺骗性的规划与诱饵系统和其他防御作为一个两个玩家的游戏与非对称信息和布尔支付的时间逻辑。我们使用2级超博弈的时间逻辑目标，以捕捉不完整/不正确的知识的攻击者对网络系统作为一个回报的误解。真正的支付函数是防御者的私人信息。然后，我们扩展了$omega$ -正则博弈的解的概念，分析了攻击者在不完全信息下的理性策略。通过将2级超对策的解从范式推广到扩展形式，我们扩展了具有安全时序逻辑目标的对策的解，以决定防御者是否能够确保安全属性满足概率1，给定任何可能的策略，被攻击者认为是理性的.此外，我们使用的解决方案的游戏与co-safe（可达性）的时间逻辑目标，以确定是否防御者可以从事攻击者，通过引导攻击者的高保真蜜罐。所提出的综合方法的有效性说明与合成网络系统的蜜罐。
Strategy Synthesis for Stochastic Rabin Games with Discounted Reward
本文研究了在具有质量目标的拉宾获胜条件和定量目标的折扣奖励的两人回合随机游戏中合成最优几乎确定胜利策略的问题，证明最优策略可能需要无限记忆，但ε最优策略可以使用有限记忆或无记忆。
A Retraction Theorem for Distributed Synthesis
我们提出了一个一般性定理的分布式综合问题的协调对策与$ω$ -定期目标的形式：如果存在一个获胜的战略联盟，那么存在一个“本质”的获胜策略，这是通过收回给定的。一般来说，这不会导致有限状态获胜策略，但当代理的知识保持有界时，我们可以解决综合问题。我们的研究是在这样的环境中进行的，其中目标是以可能观察到\emph{not}的事件来表达的。这在不完全信息的博弈中是很自然的，而不是通常的假设，即目标是用所有主体都能观察到的事件来表达的。利用知识状态的有限性和由知识状态导出的有限同余类，研究了可判定的分布式综合问题。
Rabin Games Revisited
本研究重访拉宾1972年的拉宾博弈递归算法，将其改造为基于竞技场的显式求解器，通过记忆化消除阶乘依赖，引入拉宾指数递归变体，为时态综合用直接拉宾博弈求解器奠定基础。
Synthesis of Deceptive Strategies in Reachability Games with Action Misperception
我们考虑一类图上的两个玩家回合制零和博弈，称为可达性博弈，其中玩家1（P1）的目标是达到一组目标状态，而玩家2（P2）的目标是阻止这一点。特别是，我们考虑的情况下，球员有关于彼此的行动能力的信息不对称：P2开始与P1的动作集的不完整的信息（误解），并更新误解时，P1使用以前未知的P2的行动。当P1意识到P2的错误感知时，关键问题是P1是否能够控制P2的感知，从而欺骗P2选择对P1有利的行动？我们表明，可能存在一个欺骗性的获胜策略P1，确保P1的目标是从一个国家，否则失去P1的概率实现，信息是对称的和完整的。我们提出了三个关键的结果：首先，我们引入了一个动态的超博弈模型来捕捉可达性游戏与不断发展的误解P2。其次，我们提出了一个不动点算法来计算欺骗性几乎确定获胜（DASW）区域和DASW策略。最后，我们表明，DASW策略是至少一样强大的几乎肯定赢（ASW）的策略在游戏中，P1不占P2的误解。我们说明了我们的算法使用机器人运动规划在对抗性的环境。
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
本文提出两种分析 Emerson-Lei 目标无限时长博弈的方法，通过基于不动点的特征化实现符号求解，并推广了已知条件下的算法与复杂度结果，同时提出一个可符号处理的 LTL 新表达片段用于反应式合成。
Fully Generalized Reactivity(1) Synthesis
本文提出基于COCOA的统一综合方法，弥合GR(1)到LTL的效率差距，在保持GR(1)效率的同时处理超出GR(1)的规范。
Strategies Resilient to Delay: Games under Delayed Control vs. Delay Games
本文证明延迟控制下的博弈与延迟博弈在确定性获胜策略存在性上可相互归约，从而迁移复杂性与延迟界结果，并指出随机几乎必然获胜情形不存在该对应。
Simplicity Lies in the Eye of the Beholder: A Strategic Perspective on Controllers in Reactive Synthesis
该特邀论文从博弈论控制器综合背景出发，聚焦多种综合场景下的策略复杂度，讨论内存与随机性相关的最新成果，并探索传统策略复杂度概念之外的内容。
Beyond Winning Strategies: Admissible and Admissible Winning Strategies for Quantitative Reachability Games
本文研究定量可达性博弈中的可采纳策略与可采纳获胜策略，证明其历史依赖性和存在性条件，提出综合算法，并在网格世界和机器人机械臂场景中验证。
Efficient Symbolic Approaches for Quantitative Reactive Synthesis with Finite Tasks
本文提出高效符号化算法解决资源受限机械臂与人交互完成时序逻辑任务的定量反应式综合问题，通过双人博弈和遗憾最小化策略鼓励合作，显著提升计算效率并支持更大规模问题实例。
One-clock synthesis problems
研究单时钟自动机在定时游戏中的合成问题，证明了所有变体中的普遍不可决定性，并刻画了有限记忆策略与控制器的关系。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。