A Counting Semantics for Monitoring LTL Specifications over Finite Traces
我们考虑的问题，监测的线性时间逻辑（LTL）的规格，定义在无限的路径，在有限的痕迹。例如，我们可能需要对系统是否满足或违反性质“p无穷常成立”做出裁决。“问题是，总是有一个满足该性质的有限迹的延续和一个违反它的不同延续。我们提出了一个两步的方法来解决这个问题。首先，我们引入了一个计数语义，它计算步骤的数量，以证明跟踪中每个位置的公式的满足或违反。第二，我们使用这些信息对不确定的后缀进行预测。特别是，我们认为一个好的后缀是一个短于最长的证人满意，和一个坏的后缀是短于或等于最长的证人违反。基于这一假设，我们提供了一个判决，评估是否在同一系统上执行的继续将可能满足或违反的财产。
2018-04-09 cs.FL cs.LO
A LTL Fragment for GR(1)-Synthesis
从时序逻辑（LTL）规范开始的反应式程序自动合成的想法是相当古老的，但通常被认为是不可行的，由于已知的双指数复杂性的问题。然而，新的想法，最近更新的LTL合成的兴趣：在这一领域的一个主要的新贡献是最近的工作Piterman等人。谁显示了如何多项式时间合成可以实现一个大类的LTL规格，是表达足以涵盖许多实际的例子。这些LTL规范等价于具有所谓GR（1）接受条件的ω-自动机。这种方法已被用于自动合成现实世界的应用程序的实现。为此，手动编写的确定性omega-automata具有GR（1）的条件，而不是原来的LTL规格。然而，手动生成确定性监视器当然是一项困难且容易出错的任务。因此，在本文中，我们提出的算法，自动翻译规格的一个显着的大片段的LTL确定性监测具有GR（1）的接受条件，使合成算法可以开始更可读的LTL规格。
2011-02-21 cs.LO
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
在许多物联网（IoT）应用中，由IoT设备感测到的数据被连续地发送到服务器并针对规范进行监视。由于数据通常包含敏感信息，并且被监视的规范通常是专有的，因此必须对另一端保持私有。我们提出了一个协议，进行不经意的在线监测-在线监测进行不透露每一方的私人信息的其他-对安全LTL规范。在我们的方案中，我们首先将安全LTL公式转换为DFA，并使用DFA进行在线监测。基于全同态加密（FHE），我们提出了两个在线算法（反向和块）运行DFA的遗忘。我们证明了整个协议的正确性和安全性。我们还展示了我们的算法的可扩展性理论和经验。我们的案例研究表明，我们的算法是足够快的在线监测血糖水平，证明了我们的协议的实际意义。
2022-06-03 cs.CR cs.FL cs.LO
LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
AIT Austrian Institute of Technology（奥地利技术研究所）；Aristotle University of Thessaloniki（希腊塞萨洛尼基亚里士多德大学）；Northeatern University（东北大学）
LTLGuard通过结合紧凑语言模型与轻量符号推理，有效生成无冲突的LTL规范，提升形式化验证的效率和准确性。
2026-03-05 cs.AI cs.LO cs.SE
Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications
针对非层次面向对象的实时的【形】Maude规范，提出了一种用于模型检验两类重要度量时态逻辑（MTL）属性（即有界响应和最小分离）的转换方法。我们证明了我们的模型检验算法的正确性，它终止于合理的非Zeno-ness假设时，可达状态空间是有限的。这些新的模型检验功能已集成到实时的【形】Maude中，并用于分析医疗设备网络和4路交通路口系统。
2010-09-22 cs.LO
Policy Synthesis and Reinforcement Learning for Discounted LTL
University of Pennsylvania（宾夕法尼亚大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）
本文针对LTL对转移概率扰动敏感导致无法PAC学习的问题，提出在未知转移概率的MDP中使用折扣LTL进行策略综合，并证明当折扣因子相同时可通过奖励机将其归约为折扣和奖励。
2023-05-29 cs.LG cs.LO
Accelerated Runtime Verification of LTL Specifications with Counting Semantics
运行时验证是一种有效的自动化方法，用于基于规范的离线测试和分析以及复杂系统的在线监控。规约语言通常是正则表达式或流行的时态逻辑（如LTL）的变体。本文提出了一种新的和有效的并行算法验证LTL规范，结合计数语义，嵌套量词可以受到数值约束的更有表现力的版本。这样的约束在评估阈值（例如，Web服务器的预期带宽）。这种扩展的意义在于，它使我们能够推理的正确性的一大类系统，如Web服务器，操作系统内核，和网络行为，其中的属性需要被实例化的参数化请求，内核对象，网络节点等，我们的算法使用流行的{ \em MapReduce}体系结构分裂成基于变量的集群程序跟踪在运行时间。然后，每个集群都被映射到其各自的监视器实例，并在多核CPU或GPU上进行验证和简化。我们的算法是完全实现的，我们报告非常令人鼓舞的实验结果，在现实世界的数据集上的监控开销可以忽略不计。
2014-11-09 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
Constrained LTL Specification Learning from Examples
本文提出约束LTL学习问题，允许用户在正负例之外对目标公式性质施加约束，并通过一阶关系逻辑编码和MaxSAT归约实现求解，实验表明其工具ATLAS能解决新型学习问题且性能优于或媲美现有方法。
2024-12-30 cs.LO cs.SE
Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time
我们考虑提示线性时态逻辑的可实现性问题的优化变体，线性时态逻辑（LTL）的提示最终运营商的范围是由一些参数限制的扩展。在可实现性优化问题中，人们感兴趣的是计算允许实现给定规范的最小界。已知该问题在三次指数时间内是可解的，但不知道它是否可以在双指数时间内完成，即，它是否和解决LTL可实现性一样难。我们采取了一个步骤，解决这个问题，表明最佳的可以近似在一个因素内的两个双指数的时间。此外，我们报告的概念验证的算法实现的基础上有界的LTL合成，计算最小的实现给定的规范。在我们的实验中，我们观察到的实现和它实现的界限的大小之间的权衡。我们调查这种权衡在一般情况下，并证明上限，这减少了搜索空间的算法，和匹配的下限。
2016-09-14 cs.FL cs.LO
Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
从线性时序逻辑（LTL）规范综合反应式系统是可靠的软件和硬件设计中的一个重要方面。我们介绍了经典自动机理论方法对LTL合成的适应，该方法在工具Strix中实现，该工具赢得了最后两次合成竞赛（Syntcomp 2018/2019）。所提出的方法是（1）结构化的，这意味着在构造中使用的状态具有以多种方式利用的语义结构，它执行（2）向前探索，使得它通常仅构造可达状态的一个小子集，并且它是（3）增量的，在这个意义上，它重用来自先前不确定的解决方案尝试的结果。此外，我们提出并研究了不同的指导原则，以确定在哪里扩展按需构建的舞台。此外，我们展示了几种技术提取的实现（Mealy机或电路）从证人的树自动机空检查。最后，所选择的构造使用转换函数的符号表示来减少运行时和内存消耗。我们在Syntcomp 2019基准测试集上评估了所提出的技术，并更详细地展示了所提出的技术与其他领先的LTL合成工具中实现的技术的比较。
2019-10-30 cs.LO
Computing unsatisfiable cores for LTLf specifications
University of Trento（特伦托大学）；Sapienza University of Rome（罗马大学）；FBK IRST（FBK IRST研究院）
针对有限迹线性时序逻辑（LTLf）规约的不可满足核心提取问题，本文通过适配主流LTLf可满足性检查方法提出四种算法，经基准测试验证了算法的可行性、有效性与互补性。
2022-03-09 cs.AI cs.LO
Reactive Synthesis for DECLARE via symbolic automata
给定一个规范的线性时间的时间逻辑解释有限的痕迹（LTLf），反应性合成问题要求找到一个有限表示的，终止控制器的反应，以执行所需的系统规范的不可控的行动的环境。在本文中，我们研究，第一次，反应性的综合问题，DEQUE-一个片段的LTLf广泛用于在理论和实践中指定声明性的，基于约束的业务流程。我们提供三方面的贡献。首先，我们给出了一个朴素的，双指数时间综合算法。第二，我们展示了如何任意的DEPENE规范可以compensarily编码成一个等价的纯过去的LTLf，我们利用这一点来定义一个优化的，单指数时间算法DEPENE合成。第三，我们推导出一个符号版本的算法，通过引入一个新的翻译纯过去的时间公式符号确定性有限自动机。
2022-12-21 cs.FL 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
A High-Level LTL Synthesis Format: TLSF v1.0
我们提出了时序逻辑合成格式（TLSF），一个高层次的格式来描述通过线性时序逻辑（LTL）的合成问题。该格式建立在标准LTL的基础上，但还允许使用高级结构，如集合和函数，以提供紧凑和人类可读的表示。此外，该格式允许识别规范的参数，使得单个描述可以用于定义问题族。我们还提出了一个工具，自动转换成普通的LTL格式，然后可以用于合成的求解器。该工具还允许调整规范的参数，并对结果公式应用标准转换。
2016-01-20 cs.LO
Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
IMDEA Software Institute（IMDEA软件研究所）；Universidad Politécnica de Madrid（马德里理工大学）；CIFASIS
该研究提出首个针对LTLt的完整静态反应式综合方法，结合布尔抽象与函数综合生成确定性控制器，兼具可预测性、高效性及输出优化能力。
2024-07-12 cs.AI cs.LO cs.SE
Sampling Polynomial Trajectories for LTL Verification
本文研究了线性时序逻辑规范（LTL without 'next'）下连续时间多项式样条轨迹的验证问题。每个原子命题被假定为表示由多元多项式不等式描述的状态空间区域。所提出的方法采样的轨迹战略，以捕捉每一个区域的过渡。这就产生了一个离散的词，称为跟踪，它服从于已建立的路径检查的形式化方法。原连续时间轨迹满足规范，当且仅当其迹。一般的拓扑条件的样本点的推导，确保记录的轨迹为任意连续的路径，任意区域的描述。利用计算机代数的技术，当路径和区域边界由多项式定义时，开发了一种轨迹生成算法来满足这些条件。提出的PolyTrace算法具有多项式复杂性的原子命题的数量，并保证产生的任何多项式路径的轨迹。其性能通过数值例子和机器人的案例研究证明。
2022-01-21 cs.FL cs.LO
From Realizability Modulo Theories to Synthesis Modulo Theories Part 1: Dynamic approach
本文提出首个理论反应式合成方法，结合布尔化LTL静态控制器与动态求解器查询，实现理论中的完整控制器合成。
2023-10-11 cs.LO
Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL (full version)
我们继续调查的参数化扩展的线性时序逻辑（LTL），保留有吸引力的算法特性的LTL：多项式空间模型检验算法和双指数时间算法求解游戏。Alfrer等人和Kupferman等人分别证明了参数LTL（PLTL）和PROMPT-LTL的情况，它们的时态算子配备了在时间上限制其范围的变量。后来，这也被证明是正确的参数LDL（PLDL），它扩展PLTL能够表达所有的Ω正则属性。在这里，我们将PLTL推广到有成本的系统，即，我们不是以时间来界定经营者的范围，而是以时间累积的成本来界定经营者的范围。再次，我们表明，模型检验和解决游戏的规格PLTL成本并不比相应的问题LTL。最后，我们讨论了PLDL的成本和扩展到多个成本函数。
2016-01-14 cs.FL cs.LO
A High-Level LTL Synthesis Format: TLSF v1.1
我们提出了时序逻辑合成格式（TLSF），一个高层次的格式来描述通过线性时序逻辑（LTL）的合成问题。该格式建立在标准LTL的基础上，但还允许使用高级结构，如集合和函数，以提供紧凑和人类可读的表示。此外，该格式允许识别规范的参数，使得单个描述可以用于定义问题族。此外，我们提出了一个工具，自动转换成普通的LTL格式，然后可以用于合成的求解器。该工具还允许调整规范的参数，并对结果公式应用标准转换。
2016-11-23 cs.LO
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
A Symbolic Approach to Safety LTL Synthesis
时态综合是一个与环境交互的系统的自动化设计，使用系统行为的声明性规范。提供这种规范的一种流行语言是线性时态逻辑（Linear Temporal Logic，LTL）。然而，一般情况下的LTL合成在实践中仍然是一个难以解决的问题。正因为如此，许多工作都集中在开发特定片段的LTL的合成程序，具有更容易的合成问题。本文主要研究安全LTL，定义它为LTL在否定范式~（NNF）中的Until自由片段，并证明它表示安全LTL公式的一个片段。这个片段的内在动机是观察到，在许多情况下，说某些“好”的事情最终会发生是不够的，我们需要说它何时会发生。我们在这里表明，安全LTL合成是显着简单的算法比LTL合成。我们利用这种简单性在两个方面，首先通过描述一个明确的方法的基础上减少角SAT，这可以解决在线性时间的游戏图的大小，然后通过一个有效的符号建设，允许BDD为基础的符号方法，显着优于现存的LTL合成工具。
2020-08-17 cs.LO
Enumerating Minimal Unsatisfiable Cores of LTLf formulas
University of Calabria（卡拉布里亚大学）；University of Milano-Bicocca（米兰比可卡大学）
针对有限轨迹线性时序逻辑（LTLf）的不可行性解释需求，提出将LTLf公式编码为回答集编程（ASP）规范、利用ASP极小不可满足子集对应原公式极小不可满足核的枚举方法，在基准测试中取得良好性能。
2024-09-14 cs.AI cs.LO
Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance
LTL经常被用来表达许多领域的规范，如嵌入式系统或业务流程。见证者可以帮助理解为什么LTL规范是可满足的，并且存在许多方法可以使理解见证者更容易。在不可满足的规范的情况下，不可满足的核心（UC），即，不可满足公式中本身不可满足的部分是一种已建立的调试方法。然而，很少的工作已经完成，以帮助理解UC的不可满足的LTL公式。在本文中，我们建议提高UC的不可满足的LTL公式的额外信息的时间点，在UC的子公式相关的不可满足性。例如，在“（G p）and（X not p）”中，第一次出现的“p”实际上仅与时间点1（时间从时间点0开始）的不可满足性“相关”。我们提出了一种方法来提取这样的信息，从分辨率图的时间分辨率证明LTL公式的不可满足性。我们在TRP++中实现了我们的方法，并进行了实验评估。
2013-06-12 cs.LO cs.SE
Simplifying LTL Model Checking Given Prior Knowledge
本文提出利用先验知识自动机简化LTL模型检测中的否定性质自动机，从而提升检测效率；实验表明在MCC'22基准上可显著简化或直接解决一半问题。
2025-03-28 cs.FL cs.LO
Temporal logic with predicate abstraction
考虑了一个没有量词但具有谓词抽象机制和等式的谓词线性时态逻辑LTL_{λ,=}。LTL_{λ,=}的模型可以很自然地看作是在某些（可能是无限的）域的元素上移动的卵石（柔性常数）系统。这允许使用LTL_{λ,=}的规范的动态系统使用一些资源，如使用内存位置，移动代理占用一些网站等的进程。另一方面，我们表明，LTL_{λ,=}是不是递归axiomatizable，因此，LTL_{λ,=}规范的全自动验证是不，一般来说，可能的。
2004-10-27 cs.CL cs.LO
Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free (full version)
线性时序逻辑（LTL）是反应式系统的标准规约语言，并成功地应用于工业环境。然而，许多缺点LTL已被确定在文献中，其中有限的表达，缺乏定量特征，无法表达鲁棒性。有克服这些缺点的工作，但其中每一个通常是孤立地解决。这对于所有缺点同时显现的应用是不够的。在这里，我们通过引入解决多个缺点的逻辑来解决这个问题。为此，我们结合逻辑线性动态逻辑，LTL，和强大的LTL，每个解决一个方面，新的逻辑。对于两个方面的所有组合，所得到的逻辑具有与普通LTL相同的期望算法属性。特别是，为LTL开发的高效算法后端也适用于这些新逻辑。最后，我们讨论如何同时解决这三个方面。
2021-04-29 cs.FL cs.LO
OCTAL: Graph Representation Learning for LTL Model Checking
Purdue University（普渡大学）
针对传统符号模型检测的状态空间爆炸问题，提出基于图表示学习的OCTAL框架，将LTL模型检测转化为二分类任务，实现了显著的准确率与最高11倍的整体加速。
2023-08-19 cs.AI cs.LO cs.SE
Maximum Realizability for Linear Temporal Logic Specifications
基于线性时序逻辑（LTL）规范的自动综合广泛应用于机器人运动规划、自治系统控制和电网负荷分配等领域。在这样的应用程序中，一个常见的规范模式包括一个LTL公式，描述了对系统的行为的要求，以及一组额外的理想属性。我们研究的综合问题的整体规格是无法实现的设置，更准确地说，当一些理想的属性必须（暂时）违反，以满足系统的目标。我们提供了一个定量的语义集的安全规范，并使用它来正式的“尽力而为”的满足这样的软规范，同时满足硬LTL规范。我们提出了一种算法，用于合成的实现，是最佳的定量语义。我们的方法建立在有界合成方法的思想，我们开发了一个MaxSAT编码，允许最大限度地满足安全规范的定量。我们评估我们的算法从机器人和配电网络的情况。
2018-04-02 cs.LO cs.SE
Continuous Motion Planning with Temporal Logic Specifications using Deep Neural Networks
University of Waterloo（滑铁卢大学）
针对具有连续状态和动作的运动规划问题，提出了一种无模型强化学习方法来综合控制策略。机器人被建模为一个标记的离散时间马尔可夫决策过程（MDP）与连续的状态和动作空间。线性时序逻辑（LTL）用于指定高级任务。然后，我们训练深度神经网络，以使用行动者-批评者强化学习方法来近似价值函数和策略。LTL规范被转换为带注释的有限确定性Büchi自动机（LDBA），用于连续地塑造奖励，以便在训练期间提供密集的奖励。使用强化学习解决具有LTL规范的运动规划问题的一种简单方法是对轨迹进行采样，然后如果轨迹满足整个LTL公式，则为训练分配高奖励。然而，当我们有一个复杂的连续状态和动作空间的LTL公式时，找到这样的轨迹所需的采样复杂度太高了。因此，如果所有样本轨迹都从自动机的初始状态开始，我们就不太可能获得足够的训练奖励。在本文中，我们提出了一种方法，不仅从状态空间中的初始状态采样，而且在每个训练集开始时自动机中的任意状态。我们测试我们的算法在模拟使用汽车般的机器人，并发现我们的方法可以学习不同的工作配置和LTL规范的政策成功。
2020-09-29 cs.AI cs.LG cs.LO
"Most of" leads to undecidability: Failure of adding frequencies to LTL
有限迹上的线性时态逻辑是形式化验证中常用的一种健壮的规范框架。然而，尽管近年来对逻辑的兴趣很高，但其定量扩展的主题尚未得到充分探讨。这项工作的主要目标是研究添加弱形式的百分比约束（例如，大多数的位置在过去满足给定的条件，或sigma是最频繁的字母发生在过去）的LTL片段的效果。这种扩展可能用于验证影响网络或统计推理。不幸的是，正如我们在论文中证明的那样，事实证明，即使是很小的LTL片段的百分比扩展也具有不可判定的可满足性和模型检查问题。我们的不可判定性证明，不仅锐化了大多数的不可判定性结果的逻辑与算术解释的话从文献中已知的，但也是相当简单的。我们还证明了通过限制否定的允许使用可以避免不可判定性，并简要讨论了不可判定性结果如何转移到一阶词逻辑。
2021-01-03 cs.FL cs.LO
LTLf Synthesis Under Unreliable Input
University of Oxford（牛津大学）；Rice University（莱斯大学）
研究不可靠输入下同时实现 LTLf 目标与备份规约的合成问题，证明其 2EXPTIME 完全，提出直接自动机、信念构造与 QLTLf 三种求解技术，实证发现 MSO 编码性能最佳。
2024-12-19 cs.AI cs.LO
Verifying linear temporal specifications of constant-rate multi-mode systems
本文提出面向恒速率多模式系统的 LTL 变体，并刻画其句法子片段的模型检验复杂度，得到 P 完全、NP 完全或不可判定的统一分类。
2023-04-26 cs.CC cs.FL cs.LO
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
在基于服务的应用程序的执行过程中出现的一个重要问题涉及确定是否可以用具有不同接口的服务来替换正在运行的服务的能力，例如，如果前者不再可用。标准有界模型检验技术可用于执行此检查，但它们必须能够非常快速地提供答案，以免检查妨碍应用程序的可操作性，而不是帮助它。当考虑会话服务时，问题变得更加复杂，即，服务，公开其中具有输入/输出数据依赖关系的操作。在本文中，我们介绍了一个形式化验证技术的线性时序逻辑，允许用户在公式中的整数变量的约束的扩展。这种技术适用于会话服务的可替代性问题被证明是相当快，比现有的内存占用更小。
2010-04-16 cs.LO cs.SE
Taming Large Bounds in Synthesis from Bounded-Liveness Specifications (Full Version)
从时序逻辑规范的自动合成是一个有吸引力的替代手动系统设计，由于它的能力，从高层次的规范生成正确的建设实现。由于合成问题的高度复杂性，重要的研究工作已经针对开发实际有效的方法，限制规约语言片段。在本文中，我们专注于安全LTL片段的线性时态逻辑（LTL）的语法扩展有界时态算子。我们提出了一种新的合成方法的主要动机，有效地解决了合成问题的规范与有界的时间运营商，特别是那些大的界限。我们的方法的实验评估表明，对于这种类型的规范，它优于国家的最先进的合成工具，表明它是一个很有前途的方法，有效地处理定量的时间限制在安全规范。
2023-01-24 cs.LO
LTL Verification of Memoryful Neural Agents
Imperial College London（帝国理工学院）
提出针对有记忆神经多智能体系统的LTL验证框架，支持有界与无界规范，通过边界模型检测与约束求解技术，首次实现无界规范验证并大幅提升有界验证效率。
2025-03-04 cs.AI cs.LG cs.LO
Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis
本文提出用混合zonotope后向可达性分析构造时序逻辑树，以计算高效且能表示非凸、不相交几何形状的方式形式化验证自主系统的LTL规范。
2024-04-04 cs.LO cs.SY eess.SY
Learning Interpretable Models in the Property Specification Language
Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；Ben-Gurion University（本-古里安大学）
我们解决的问题，学习人类可解释的描述一个复杂的系统，从一组有限的积极和消极的例子，其行为。在这方面的最新工作，它侧重于线性时序逻辑（LTL）表示的描述，我们开发了一个学习算法的公式在IEEE标准时序逻辑PSL（属性规约语言）。我们的工作是出于这样一个事实，即许多自然属性，如事件发生在每第n个时间点，不能在LTL中表示，而它很容易在PSL中表示这样的属性。此外，PSL中的公式比LTL中的公式更简洁，更容易解释（由于在PSL公式中使用了正则表达式）。我们的学习算法建立在现有的学习LTL公式的算法之上。粗略地说，我们的算法减少了学习任务的命题逻辑中的约束满足问题，然后使用SAT求解器搜索一个解决方案，在一个增量的方式。我们已经实现了我们的算法，并进行了比较研究所提出的方法和现有的LTL学习算法。我们的研究结果说明了所提出的方法的有效性，从例子中提供简洁的人类可解释的描述。
2020-02-10 cs.LG cs.LO stat.ML
Secure Control in Partially Observable Environments to Satisfy LTL Specifications
本文研究了在部分可观察环境中，在对手存在的情况下，必须满足时序逻辑规范的智能体的控制策略的合成。代理（防御者）与对手的相互作用被建模为部分可观察的随机博弈。我们的目标是生成一个防御者的政策，以最大限度地满足给定的时间逻辑规范下的任何对手的政策。搜索策略仅限于有限状态控制器的空间，这导致了一个易于处理的方法来确定策略。我们的规范达到（子集）经常性状态的马尔可夫链的满意度。我们提出了一个算法来确定一组防守者和对手的有限状态控制器的固定大小，将满足时序逻辑规范，并证明它是健全的。然后，我们提出了一个值迭代算法，以最大限度地满足时间逻辑规范下的有限状态控制器的固定大小的概率。最后，我们将此设置扩展到防御者的有限状态控制器的大小可以增加以提高满意度概率的情况。我们用一个例子来说明我们的方法。
2020-11-05 cs.CR cs.GT cs.LO
Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+
本研究提出首个从LTL到LTLf+的线性转换方法，将LTL归一化为Manna-Pnueli层次的反应片段，保留LTLf+的优势且无渐近代价，可将LTLf+技术应用于更多AI问题。
2026-08-04 cs.AI cs.FL cs.LO
Learning Optimal Strategies for Temporal Tasks in Stochastic Games
Duke University（杜克大学）；University of Florida（佛罗里达大学）
本文提出一种无需环境模型的强化学习方法，通过确定性奇数自动机构建产品博弈，利用折扣奖励优化策略以满足LTL规范，解决大规模颜色问题并验证方法有效性。
2023-08-31 cs.AI cs.LG 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
Learning GR(1) Specifications from Traces
Yale University（耶鲁大学）；Columbia University（哥伦比亚大学）；Barnard College, Columbia University（巴纳德学院，哥伦比亚大学）
本文提出基于SAT的工具GR1MINE，利用GR(1)时序骨架与学习子句提升效率，在GR(1)及非GR(1)规范基准上，其学习可实现公式的速度与性能均优于现有基线工具。
2026-08-10 cs.FL cs.LO cs.SE
Iterative Circuit Repair Against Formal Specifications
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）；Stanford University（斯坦福大学）
我们提出了一种深度学习方法，用于根据线性时间时序逻辑（LTL）中给出的形式规范修复时序电路。给定一个有缺陷的电路及其正式规范，我们对Transformer模型进行训练，以输出满足相应规范的电路。我们提出了一个分离的分层Transformer的形式规格说明和电路的多模态表示学习。我们引入了一个数据生成算法，使泛化到更复杂的规格和分布数据集。此外，我们提出的修复机制显着提高了自动合成的电路从LTL规格与Transformers。它提高了最先进的$6.8$百分点上举行的实例和$11.8$百分点上的分布数据集从年度反应合成竞争。
2023-03-02 cs.LG cs.LO
Reactive Synthesis Modulo Theories Using Abstraction Refinement
反应式合成从作为时序逻辑公式给出的规范构建系统。传统上，无功综合定义为具有布尔输入和输出变量的系统。最近，新的理论和技术已经被提出来扩展反应合成的数据域，这是需要更复杂的程序。特别是，时间流逻辑（TSL）（Finkbeiner et al. 2019）通过状态变量、更新和未解释的函数扩展了LTL，并被创建用于合成。本文给出了TSL（T）的一个综合方法，它是TSL的理论推广。使用反例引导合成循环和LTL合成程序进行合成。我们的方法翻译TSL（T）规格LTL和提取系统，如果合成成功。另外，分析了与理论不一致的对策。如果反策略是理论一致的，则证明该规范是不可实现的。否则，我们将时间假设和布尔谓词添加到TSL（T）规范中，并开始循环的下一次迭代。我们证明了TSL（T）的综合问题是不可判定的。然而，我们的方法可以成功地合成或显示几个非布尔的例子的不可实现性。
2021-07-30 cs.LO
Distributed PROMPT-LTL Synthesis
我们认为，在提示线性时序逻辑（PROMPT-LTL），它扩展了LTL的时间运营商配备了参数，约束其范围的规范的分布式实现的合成。对于单过程综合，这是公认的，这样的参数扩展不会增加最坏情况下的复杂性。对于同步系统，我们表明，尽管是更强大的，分布式的可实现性问题的PROMPT-LTL并不比它的LTL对应。对于异步系统，我们必须考虑一个假设保证合成问题，因为我们必须表达调度假设。由于异步分布式综合对于LTL已经是不可判定的，我们给出了基于有界综合的PROMPT-LTL假设保证综合问题的半判定过程。
2016-09-14 cs.GT cs.LO
Learning Probabilistic Temporal Logic Specifications for Stochastic Systems
University of Oxford（牛津大学）；National University of Singapore（国立新加坡大学）
针对现有形式化规范推断方法无法刻画随机系统行为的问题，提出结合文法枚举、启发式搜索等技术的PLTL规范学习算法，可从马尔可夫链中高效提取能刻画策略或模型变体时序差异的简洁规范。
2025-05-17 cs.AI cs.FL cs.LO
LTL Reactive Synthesis with a Few Hints
我们研究了一个变种的问题，合成Mealy机，执行LTL规格对所有可能的行为的环境，包括敌对的。在这里研究的变体中，用户提供了系统的高级LTL规范，以设计，以及解决方案必须产生的一组执行示例E。我们的合成算法分为两个阶段。首先，它使用自动机学习算法的定制扩展来概括沿着示例E采取的决策。这个阶段概括了E中用户提供的示例，同时保留了可实现性。其次，该算法将学习阶段得到的（通常）不完全Mealy机转化为完全Mealy机，从而实现了并行学习。这些例子被用来指导合成过程。我们提供了一个完整的结果，表明我们的程序可以学习任何Mealy机M，实现了一个小的（多项式）集的例子。我们还表明，我们的问题，推广经典的LTL合成问题（即当E = { \emptyset }），匹配其最坏情况下的复杂性。从E学习的额外成本在E的大小和实现可扩展性的解决方案的符号表示的大小上是偶数多项式。该符号表示是由在Acacia-Bonzai中实现的合成算法在解决普通LTL合成问题时计算的。我们说明了我们的方法的一组例子的实际利益。
2023-01-25 cs.FL cs.GT cs.LO
Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)
DEIB, Politecnico di Milano（博洛尼亚工程学院，米兰理工大学）；Politecnico di Milano（米兰理工大学）；INESC-ID/Instituto Superior Técnico Universidade de Lisboa（里斯本大学超级学院/葡萄牙信息科学与技术研究所）；Dipartimento di Informatica Università degli Studi di Milano（米兰大学信息学院）
本文提出了一种基于LTLfMT的一阶时间逻辑奖励规范框架，结合奖励机和HER解决奖励稀疏性问题，适用于连续控制任务。
2026-02-05 cs.AI 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
High-Quality Synthesis Against Stochastic Environments
在经典的综合问题中，我们给出了一个LTL公式psi的输入和输出信号的集合，我们合成了一个传感器，实现psi。自动综合在实际应用中的一个缺点是没有考虑综合系统的质量。实际上，经典的设置是布尔型的：一个计算满足或不满足一个规范。因此，虽然合成的系统是正确的，但它的质量没有保证。近年来，研究人员考虑将经典布尔设置扩展到定量设置。逻辑LTL [F]是一个多值逻辑，它用质量算子扩充了LTL。LTL [F]公式的满意值是[0，1]中的实值，其中该值越高，计算满足规范的质量越高。LTL的决策问题变成了LFL的搜索或优化问题[F]。特别是，在合成问题中，目标是生成满足最高质量规格的换能器。以前的工作考虑了最坏情况的设置，目标是以最小的质量最大化计算的质量。我们引入并解决了随机设置，其中的目标是生成一个换能器，最大限度地提高预期的计算质量，受到给定的输入信号分布。因此，环境不是敌对的，而是被假设为概率性的，这对应于许多现实的设置。我们发现，这个问题是2EXPTIME完全的，像经典的LTL合成，仍然是这样，在两个扩展，我们认为：一个最大限度地提高预期的质量，同时保证最低的质量是，概率$1$，在给定的阈值以上，和一个允许对环境的假设。
2016-08-23 cs.LO
Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL
我们继续调查的参数化扩展的线性时序逻辑（LTL），保留有吸引力的算法特性的LTL：多项式空间模型检验算法和双指数时间算法求解游戏。Alfrer等人和Kupferman等人分别证明了参数LTL（PLTL）和PROMPT-LTL的情况，它们的时态算子配备了在时间上限制其范围的变量。后来，这也被证明是正确的参数LDL（PLDL），它扩展PLTL能够表达所有的Ω正则属性。在这里，我们将PLTL推广到有成本的系统，即，我们不是以时间来界定经营者的范围，而是以时间累积的成本来界定经营者的范围。再次，我们表明，模型检验和解决游戏的规格PLTL成本并不比相应的问题LTL。最后，我们讨论了PLDL的成本和扩展到多个成本函数。
2015-09-24 cs.LO
Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages
提供适当的工具来解决不一致的合规规则的问题是一个重要的研究课题。这个问题对于实现对早期声明式设计的自动支持以及支持基于契约或基于服务的系统中规则的演化至关重要。在本文中，我们研究的问题，提取时间不可满足的核心，以检测不一致的部分规范。我们扩展了冲突驱动的SAT求解器，为时序逻辑提供了一个新的冲突驱动的深度优先搜索求解器。我们使用此求解器来计算LTL不可满足的核心，而无需重新探索求解器的历史。
2011-09-13 cs.LO
Safeguarding Learning-based Control for Smart Energy Systems with Sampling Specifications
Fraunhofer IKS（弗劳恩霍夫智能感知系统研究所）
本文针对强化学习控制能源系统时的安全问题，将实时时序安全要求离散化为 LTL 规范，以支持安全强化学习的 shields 综合与形式化验证，并为原始安全要求提供概率下界。
2023-08-11 cs.LG cs.LO cs.SE
