Learning Optimal Strategies for Temporal Tasks in Stochastic Games
Duke University（杜克大学）；University of Florida（佛罗里达大学）
本文提出一种无需环境模型的强化学习方法，通过确定性奇数自动机构建产品博弈，利用折扣奖励优化策略以满足LTL规范，解决大规模颜色问题并验证方法有效性。
2023-08-31 cs.AI cs.LG cs.LO
Secure Control in Partially Observable Environments to Satisfy LTL Specifications
本文研究了在部分可观察环境中，在对手存在的情况下，必须满足时序逻辑规范的智能体的控制策略的合成。代理（防御者）与对手的相互作用被建模为部分可观察的随机博弈。我们的目标是生成一个防御者的政策，以最大限度地满足给定的时间逻辑规范下的任何对手的政策。搜索策略仅限于有限状态控制器的空间，这导致了一个易于处理的方法来确定策略。我们的规范达到（子集）经常性状态的马尔可夫链的满意度。我们提出了一个算法来确定一组防守者和对手的有限状态控制器的固定大小，将满足时序逻辑规范，并证明它是健全的。然后，我们提出了一个值迭代算法，以最大限度地满足时间逻辑规范下的有限状态控制器的固定大小的概率。最后，我们将此设置扩展到防御者的有限状态控制器的大小可以增加以提高满意度概率的情况。我们用一个例子来说明我们的方法。
2020-11-05 cs.CR cs.GT cs.LO
From Realizability Modulo Theories to Synthesis Modulo Theories Part 1: Dynamic approach
本文提出首个理论反应式合成方法，结合布尔化LTL静态控制器与动态求解器查询，实现理论中的完整控制器合成。
2023-10-11 cs.LO
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
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
我们提出了一个统一的翻译LTL公式到确定性拉宾自动机，有限确定性Büchi自动机，和不确定性Büchi自动机。翻译产生自动机的渐近最佳大小（双或单指数，分别）。所有三种翻译都是从一个纯粹逻辑性质的主定理推导出来的。主定理将公式的语言分解为语言的正布尔组合，这些语言可以通过初等方法转化为ω-自动机。特别是，Safra的，排名，和断点结构中使用的其他翻译是不需要的。
2018-05-02 cs.LO
Reactive Synthesis from Extended Bounded Response LTL Specifications
反应合成是一个关键技术的设计正确的建设系统，并已在过去的几十年里进行了深入的研究。它包括在一个控制器的合成，反应环境的输入满足给定的时序逻辑规范。常见的方法是基于自动机的显式构造和它们的确定性，这限制了它们的可扩展性。在本文中，我们引入了一个新的片段的线性时序逻辑，称为扩展有界响应LTL（\LTLEBR），它允许一个结合有界和普遍无界的时间运营商（从而涵盖了大量的实际情况），我们表明，反应合成从\LTLEBR规范可以减少到解决一个安全游戏的确定性的符号自动机直接从规范。我们证明了所提出的方法的正确性，我们成功地评估它在各种基准。
2020-08-12 cs.FL cs.LO cs.SE
Finite LTL Synthesis is EXPTIME-complete
LTL综合--构造满足线性时序逻辑中的逻辑规范的函数--是一个2 EXPTIME完全问题，在控制器综合和无数人工智能应用中具有相关应用。在本研究中，我们考虑德贾科莫和瓦尔迪的变体的综合问题的LTL公式解释有限，而不是无限的痕迹。而令人惊讶的是，鉴于现有的索赔的复杂性，我们建立的LTL合成是EXPTIME完成的有限解释，而不是2 EXPTIME完成以前报道的。我们的结果很好地符合规划的角度，其中非确定性规划与充分的可观测性是EXPTIME-完全和部分可观测性增加的复杂性，以2 EXPTIME-完全;最近的相关结果LTL合成表明，在有限的情况下，部分可观测性，问题是2 EXPTIME-完全。
2016-11-17 cs.AI cs.LO
LTLf Synthesis on Probabilistic Systems
Rice University（莱斯大学）；University of Colorado, Boulder（科罗拉多大学博尔德分校）
许多系统自然地被建模为马尔可夫决策过程（MDP），结合了概率和战略行动。给定一个作为MDP的系统模型和一些系统行为的逻辑规范，综合的目标是找到一个最大化实现这种行为的概率的策略。定义行为的一个流行选择是线性时态逻辑（LTL）。关于LTL中规定的特性的MDP的政策综合已经得到了很好的研究。然而，LTL是在无限迹上定义的，而许多感兴趣的属性本质上是有限的。有限迹上的线性时序逻辑（LTLf）已被用来表达这样的属性，但没有工具存在，以解决策略合成MDP行为的有限迹属性。我们提出了两种算法来解决这个合成问题：第一个通过减少LTLf到LTL和第二个使用本地工具的LTLf。我们比较了这两种方法的可扩展性的合成，并表明，本机的方法提供了更好的可扩展性相比，现有的自动机生成工具的LTL。
2020-09-23 cs.AI cs.LO
Model-Free Learning of Safe yet Effective Controllers
Duke University（杜克大学）
本文研究学习安全且有效的控制策略，通过强化学习算法优先保证安全，再满足LTL规范，最后优化控制性能奖励。
2021-09-26 cs.FL cs.LG cs.LO
Model-Free Reinforcement Learning for Stochastic Games with Linear Temporal Logic Objectives
Duke University（杜克大学）
本文研究了在未知环境中合成满足线性时序逻辑（LTL）目标的控制策略问题，提出了一种无模型强化学习方法，通过确定性拉宾自动机（DRA）的接受条件来最大化满足LTL规范的概率，并在两个运动规划案例中验证了方法的适用性。
2020-10-02 cs.LO cs.RO
Safety-Guarantee Controller Synthesis for Cyber-Physical Systems
由于控制组件和软件组件使用不同的建模抽象，网络物理系统的验证和确认是一个困难的问题。最近解决这一困难的一个趋势是通过采用按设计纠正的方法来减少对核查的需要。根据正确的设计范式，一个寻求自动合成的控制器，可以细化为代码，并强制执行时间规范的信息物理系统。在本文中，我们考虑这个问题的一个实例，其中的规格是由一个片段的线性时序逻辑（LTL）和物理环境描述的一个光滑的微分方程。本文的贡献是表明，合成的网络物理系统是可行的，考虑一个片段的LTL，是表达足够的描述有趣的属性，但足够简单，以避免萨夫拉的建设。我们报告的两个例子说明了这些技术的工具PESSOALTL的初步实施。
2010-10-27 cs.LO
Finite LTL Synthesis with Environment Assumptions and Quality Measures
University of Toronto（多伦多大学）；CNRS（法国国家科学研究中心）；Univ. Montpellier（蒙彼利埃大学）；Inria（法国国家信息与自动化研究所）
在本文中，我们调查的问题，线性时序逻辑（LTL）规范，解释了有限的痕迹-一个问题，是中央的控制器，机器人程序和业务流程的自动化建设的合成策略。我们研究了有限LTL综合问题的一个自然变体，其中策略保证是基于指定的环境行为。我们进一步探索LTL的定量扩展，支持质量措施的规范，利用它来合成高质量的战略。我们提出了新的概念，最优性和相关的算法，产生的战略，最好满足指定的质量措施。我们的算法利用自动机游戏的方法，通过现有的国家的最先进的技术，为未来的实施定位。
2018-08-31 cs.AI cs.LO
Logically-Constrained Reinforcement Learning
University of Oxford（牛津大学）
我们提出了第一个无模型强化学习（RL）算法来合成一个未知的马尔可夫决策过程（MDP）的政策，这样一个线性时间属性是满意的。给定的时间属性被转换成一个有限的确定性Buchi自动机（LDBA）和一个强大的奖励函数定义在MDP的状态-动作对根据所得到的LDBA。有了这个奖励函数，策略综合过程就受到给定规范的“约束”。这些约束指导MDP探索，以便通过仅考虑与LTL属性的满意度相关的MDP部分来最小化求解时间。这通过避免在整个状态空间上的穷举更新而提高了所提出的方法的性能和可扩展性，而标准方法（诸如动态规划）的效率被过多的存储器需求所阻碍，所述过多的存储器需求是由在存储器中存储完整模型的需要引起的。此外，我们表明，RL过程设置了一个局部值迭代方法，有效地计算满足给定属性的最大概率，在任何给定的状态的MDP。我们证明，我们的算法是保证找到一个政策的痕迹概率满足LTL属性，如果这样的政策存在，此外，我们表明，我们的方法产生合理的控制政策，即使LTL属性不能得到满足。通过一组数值算例对算法的性能进行了评估。我们观察到的一个数量级的改进，所需的合成迭代的数量相比，现有的方法。
2019-02-16 cs.LG cs.LO
Guiding Multi-agent Multi-task Reinforcement Learning by a Hierarchical Framework with Logical Reward Shaping
Dalian University of Technology（大连理工大学）；Westlake University（西湖大学）；Guangzhou University（广州大学）
针对现有多智能体分层强化学习算法仅适用于单任务的局限，提出带逻辑奖励塑形的多智能体协作算法，结合LTL表达任务逻辑与价值迭代协调机制，在类Minecraft环境中验证了其提升多任务学习性能的效果。
2024-11-02 cs.AI cs.LO
Two Variable vs. Linear Temporal Logic in Model Checking and Games
用一阶逻辑表示的模型检验线性时间性质具有非初等复杂性，因此采用各种受限逻辑语言。在本文中，我们考虑两个这样的限制规格说明逻辑，线性时序逻辑（LTL）和两个变量的一阶逻辑（FO 2）。LTL更有表现力，但FO 2可以更简洁，因此不清楚哪一个更容易验证。我们需要一个全面的看看这个问题，给出了一个比较的验证问题FO 2，LTL，以及各种子逻辑在广泛的模型。特别是，我们看看一元时序逻辑（UTL），LTL的一个子集，这是表现等价于FO 2;我们还考虑了无口吃的FO 2片段，通过省略后继关系，和表现等价的UTL片段，通过省略下一个和上一个连接词。我们给出了三个逻辑自动机的翻译，可用于给FO 2和UTL和各种子逻辑的上界。我们应用这些来获得新的边界的非确定性系统（分层和递归状态机，游戏）和概率系统（马尔可夫链，递归马尔可夫链，马尔可夫决策过程）。我们用匹配的下界参数来耦合它们。接下来，我们将研究如何将FO 2验证技术与LTL验证技术相结合。我们在这里提出了一种语言，包括FO 2和LTL，并继承了这两种语言的模型检验属性。我们的研究结果给出了一个统一的方法来理解的行为FO 2和LTL，随着这些逻辑及其子逻辑验证的复杂性几乎全面的图片。
2013-05-22 cs.FL cs.LO
Mode-Target Games: Reactive Synthesis for Control Applications
本文提出了一类线性时序逻辑（LTL）规范，可在多项式时间内合成控制器。该规范称为模式-目标（MT），受控制应用中多种模式及其对应目标的启发。将合成 enforcing MT 规范的控制器问题建模为游戏，并提供一个需要 O(∑i ti n²) 符号步骤的算法。
2016-12-17 cs.GT cs.LO cs.SY
Structural Synthesis for GXW Specifications
我们定义的GXW片段的线性时序逻辑（LTL）的基础上合成嵌入式控制软件的安全关键型应用程序。由于GXW包括使用弱直到操作符，我们能够指定一些不同的可编程逻辑控制（PLC）的问题，我们已经从工业训练集编译。对于GXW控制器规范，我们开发了一种新的方法来合成一组同步通信的基于演员的控制器。该综合算法通过对GXW规范的结构进行递归，并根据公式结构生成一组专用的同步通信子控制器。在后续步骤中，2QBF约束求解识别并尝试解决各个GXW规范之间的潜在冲突。GXW合成的这种结构化方法支持安全关键软件认证制度所要求的需求和生成的控制代码之间的可追溯性。GXW规范的合成是在PSPACE中进行的，而2EXPTIME是完整的LTL合成。事实上，我们的实验结果表明，GXW合成规模以及工业规模的控制合成问题，20个输入和输出端口及以上。
2016-07-06 cs.LO cs.SE
Symbolic Parity Game Solvers that Yield Winning Strategies
奇偶博弈在LTL合成中起着重要的作用，最近LTL合成的突破证明了这一点，这部分依赖于奇偶博弈的解决。然而，如果我们想扩展到更大的系统或规格，状态空间爆炸仍然是一个主要问题。为了解决这个问题，我们需要研究符号方法，如BDD，它在过去已经成功地解决了指数大系统。因此，它是必不可少的，有符号奇偶博弈求解算法，使用BDD操作，是快速的，可以产生获胜的策略，用于合成LTL合成的控制器。当前的符号奇偶博弈求解算法不产生获胜策略。我们现在提出两个符号算法，产生获胜的战略，基于最近提出的两个不动点算法。我们实现了算法，并使用从SYNTCOMP 2020获得的基准进行了经验评估。我们的结论是，算法的竞争力或更快比Zielonka的递归算法的早期符号实现，同时还提供了获胜的策略。
2020-09-23 cs.LO
Universal Safety Controllers with Learned Prophecies
针对通用安全控制器中预言精确计算与验证的计算难题，本文提出基于学习的近似合成算法，从小示例被控对象推导CTL公式作为预言，经实验验证其兼具泛化性、紧凑性与可解释性。
2025-11-14 cs.LO
Specification and Reactive Synthesis of Robust Controllers
本文研究了从区间时序逻辑QDDC中给出的正则性质的逻辑规范综合鲁棒控制器的问题。我们的规范包括硬鲁棒性和软鲁棒性。在这里，硬鲁棒性保证承诺在用户指定的放松（弱化）假设下的不变性。一个系统的框架，逻辑上指定的假设弱化的公式，称为鲁棒性标准，提出。软鲁棒性涉及控制器保持尽可能多的输入的承诺的能力，而不管任何假设。我们提出了一个统一的方法来合成一个强大的控制器，保证指定的硬鲁棒性，它优化指定的软鲁棒性。该方法使用DCSynth工具实现，该工具提供软需求优化的控制器合成。通过一个同步总线仲裁器的案例研究，我们的实验表明，硬鲁棒性标准以及软鲁棒性的综合控制器的能力，以满足承诺的影响“尽可能多”。分析了最坏情况和预期情况下的行为。
2019-05-27 cs.LO
Synthesis of Universal Safety Controllers
本文提出一种仅从逻辑规范转换的博弈中构建通用安全控制器的新方法，通过prophecies预测受控对象行为以确保动作安全，提升了可扩展性、适应性和可解释性。
2025-01-30 cs.LO
GenSys: A Scalable Fixed-point Engine for Maximal Controller Synthesis over Infinite State Spaces
无限状态系统最大容许控制器的综合有许多实际应用。这样的控制器直接对应于逻辑上指定的无限状态两人游戏中的最大获胜策略。在本文中，我们介绍了一个名为GenSys的工具，这是一个不动点引擎，用于计算无限状态安全游戏中玩家的最大获胜策略。GenSys的一个关键特性是它利用现有的现成求解器的功能来实现其定点引擎。GenSys在这一领域的表现远远优于最先进的工具。我们的工具已经解决了这个领域中的一些挑战性问题，是可扩展的，也合成紧凑的控制器。这些控制器尺寸相对较小，更容易理解。GenSys可免费使用，并在开源许可证下提供。
2021-08-16 cs.LO cs.SY eess.SY
Overview of Logical Foundations of Cyber-Physical Systems
每当计算机技术与物理世界交互时，网络物理系统（CPS）就很重要，就像在自动驾驶汽车或飞机控制支持系统中一样。由于它们的许多微妙之处，网络物理系统的控制器应该被保持最高的正确性标准。它们的正确运行至关重要，这解释了对其数学模型的安全分析技术的广泛兴趣，这些数学模型被称为混合系统，因为它们将离散动态与连续动态相结合。微分动态逻辑（dL）为混合系统提供了逻辑规范和严格推理技术。逻辑dL在定理证明器KeYmaera X中实现，它在验证地面机器人控制器、铁路系统和下一代机载防撞系统ACAS X中发挥了重要作用。本章提供了一个非正式的概述，这种逻辑方法CPS的安全，详细介绍了最近的教科书上的逻辑基础的网络物理系统。它还解释了在验证模型的土地上获得的安全保证如何达到CPS执行的水平。
2019-10-24 cs.LO cs.PL math.LO
LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning
University of Oxford（牛津大学）；Amazon Inc（亚马逊公司）
LCRL是一个软件工具，它在未知的马尔可夫决策过程（MDP）上实现无模型强化学习（RL）算法，合成满足给定线性时间规范的最大概率的策略。LCRL利用部分确定性有限状态机（称为有限确定性Buchi自动机（LDBA））来表达给定的线性时间规范。基于LDBA的结构，RL算法的奖励函数是动态成形的。在适当假设下的理论保证确保RL算法收敛到最大化满意概率的最优策略。我们提出的案例研究，以证明LCRL的适用性，易用性，可扩展性和性能。由于LDBA引导的探索和LCRL无模型架构，我们观察到了强大的性能，与标准RL方法相比（适用于LTL规范时）也具有很好的扩展性。有关如何执行本文中所有案例研究的完整说明，请参见LCRL发行版www.github.com/grockious/lcrl附带的GitHub页面。
2022-09-21 cs.AI cs.LG cs.LO
Model checking memoryful linear-time logics over one-counter automata
我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。
2010-01-18 cs.LO
Efficient Reactive Synthesis Using Mode Decomposition
针对LTL反应式综合计算复杂度高、难以适配大规模场景的问题，提出基于模式的新型分解算法，将复杂安全规约分解为子问题后顺序组合解，证明了方法的正确性并通过案例验证了可行性。
2023-12-14 cs.LO cs.SE
Model-checking Quantitative Alternating-time Temporal Logic on One-counter Game Models
我们考虑定量扩展的交替时间时序逻辑ATL/ATL称为定量交替时间时序逻辑（QATL/QATL），其中计数器的值可以比较使用等式，不等式和模约束的常数。我们解释这些逻辑在一个计数器的游戏模型，这是无限的持续时间的游戏有限的控制图，每个过渡可以增加或减少一个无界计数器的值。也就是说，这些游戏的状态空间通常是无限的。我们考虑的模型检验问题的逻辑QATL和QATL的一个计数器的游戏模型与VASS语义，我们开发的算法，并提供匹配的下界。我们的算法是基于减少的模型检验问题的模型检验游戏。这种方法使我们很容易处理扩展的逻辑语言以及无限的状态空间。该框架一方面概括了定性问题，如有限状态系统的ATL/ATL模型检验、单计数器过程上的分支时间时序逻辑CTL和CTL的模型检验以及LTL规范的可实现性问题。另一方面，QATL/QATL的模型检验问题推广了定量问题，如能源博弈（在QATL的情况下）和能源平价博弈（在QATL的情况下）的固定初始信用问题。我们的结果是积极的，因为我们表明，泛化是不是太昂贵的复杂性。作为一个副产品，我们获得了新的结果的复杂性模型检验CTL在一个计数器的过程中，并表明，决定赢家在一个计数器的游戏与LTL的目标是2 ExpSpace完成。
2014-09-19 cs.LO
