LTL Verification of Memoryful Neural Agents
Imperial College London（帝国理工学院）
提出针对有记忆神经多智能体系统的LTL验证框架，支持有界与无界规范，通过边界模型检测与约束求解技术，首次实现无界规范验证并大幅提升有界验证效率。
2025-03-04 cs.AI cs.LG 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
Automatic Generation of Safety-compliant Linear Temporal Logic via Large Language Model: A Self-supervised Framework
Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））
本文提出AutoSafeLTL框架，利用大语言模型自动生成符合安全限制的LTL规范，通过语言包含检查与自动反例引导修改机制确保逻辑一致性和语义准确性。
2026-04-27 cs.FL cs.LO
Discounting in LTL
近年来，越来越多的需求和兴趣，形式化和推理的软件和硬件系统的质量。与传统的验证不同，传统的验证处理的是系统是否满足给定规范的问题，关于质量的推理处理的是系统满足规范的\emph{how well}问题。这种努力的一个方向是将时态逻辑的“最终”运算符细化为{ \em折扣运算符}：规范的满意值是$[0,1]$中的值，其中满足可能性需求所花费的时间越长，满意值就越小。本文介绍了线性时态逻辑的一种折扣增广，并对其进行了研究，同时也研究了它与命题质量算子的结合。我们表明，可以增加LTL与任意一组贴现函数，同时保持模型检查问题的可判定性。用一元命题质量算子进一步扩充逻辑保持了可判定性，而增加平均算子使一些问题不可判定。我们还讨论了问题的复杂性，以及各种扩展。
2014-11-19 cs.FL cs.LO
A Complete Fragment of LTL(EB)
本文研究基于状态的严格化方法中的活性条件验证问题，在LTL(EB)的□LTL片段中提出一套可靠且在温和限制下对Event-B机器完全的推导规则。
2024-01-30 cs.LO
Platform Dependent Verification: On Engineering Verification Tools for 21st Century
本文综述了与平台相关的显式状态LTL模型检验的最新进展。
2011-11-02 cs.LO cs.SE
Semantics for Linear-time Temporal Logic with Finite Observations
本文通过确定性前缀集族为运行时验证逻辑 LTL3 建立完整的基于模型的归纳语义，证明其与传统 LTL 语义直接对应，并在 Isabelle/HOL 中形式化了公式进展求值技术及其在有限迹上的可靠性与完备性。
2024-11-21 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
Rational Verification for Probabilistic Systems
Monash University（莫纳什大学）；University of Oxford（牛津大学）；University of Kaiserslautern（凯泽斯劳滕大学）
理性验证是确定在多智能体系统中，在系统中的智能体理性行动的假设下，通过选择共同形成博弈论均衡的策略，将持有哪些时间逻辑属性的问题。以前在这方面的工作主要集中在确定性系统。在本文中，我们发展的理论和算法的合理性验证概率系统。我们专注于并发随机游戏（CSG），它可以用来模拟复杂的多智能体环境中的不确定性和随机性。在定性概率环境下，研究了非合作博弈和合作博弈的理性验证问题。在前一种情况下，我们认为LTL性质满足的纳什均衡的游戏，在后一种情况下，LTL性质满足的核心。在这两种情况下，我们表明，问题是2 EXPTIME-完全的，因此不困难比简单得多的验证问题的模型检验LTL性能的系统建模为马尔可夫决策过程（MDPs）。
2021-07-26 cs.AI cs.GT cs.LO
Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
路径检查是模型检验问题的一种特殊情况，其中所考虑的模型是单个路径，在监视、测试和验证中起着重要的作用。我们证明了线性时间时序逻辑（LTL），路径检查可以有效地并行化。除了核心逻辑，我们考虑扩展的LTL与有界未来（BLTL）和过去的时间（LTL+过去）运营商。尽管这两个扩展都以指数方式提高了逻辑的简洁性，但路径检查仍然可以有效地并行化：我们对LTL、LTL+Past和BLTL+Past的算法是在AC ^1（logDCFL）\subseteq NC中。
2012-10-19 cs.LO
The Infinite, in Finite Time
University of Edinburgh（爱丁堡大学）；University of New South Wales（新南威尔士大学）；Australian National University（澳大利亚国立大学）
该研究针对运行时验证场景，通过引入确定性前缀丰富LTL语义，证明LTL与LTL₃语义同构，形式化公式演进技术并证明其可靠性与完备性，重构安全-活性分解定理等，所有内容均在Isabelle/HOL中机械化实现。
2026-08-25 cs.LO
Temporal logic with predicate abstraction
考虑了一个没有量词但具有谓词抽象机制和等式的谓词线性时态逻辑LTL_{λ,=}。LTL_{λ,=}的模型可以很自然地看作是在某些（可能是无限的）域的元素上移动的卵石（柔性常数）系统。这允许使用LTL_{λ,=}的规范的动态系统使用一些资源，如使用内存位置，移动代理占用一些网站等的进程。另一方面，我们表明，LTL_{λ,=}是不是递归axiomatizable，因此，LTL_{λ,=}规范的全自动验证是不，一般来说，可能的。
2004-10-27 cs.CL cs.LO
Team Semantics for the Specification and Verification of Hyperproperties
我们开发团队语义的线性时序逻辑（LTL）来表达hyperproperties，这是最近被确定为一个关键的概念，在信息流属性的验证。从概念上讲，我们认为一个异步和同步的团队语义的变体。我们研究了这种新逻辑的基本性质，并对其可满足性、路径和模型检验问题的计算复杂性进行了分类。此外，我们将研究这些基本逻辑的扩展如何对添加其他原子运算符做出反应。最后，我们比较它的表现力的HyperLTL，另一个最近推出的逻辑hyperproperties。我们的研究结果表明，团队语义下的LTL是一个可行的替代HyperLTL，它补充了HyperLTL的表达能力，并具有部分更好的算法性能。
2018-06-25 cs.CC cs.LO
Rational Verification in Iterated Electric Boolean Games
电布尔博弈是博弈的紧凑表示，其中参与者具有由LTL公式描述的定性目标并且具有有限的资源。我们研究了几个决策问题的复杂性与分析的合理性，在电动布尔游戏与LTL目标。特别是，我们报告的问题，决定是否配置文件是一个纳什均衡在一个迭代的电动布尔游戏并不比在迭代的布尔游戏没有资源界限。我们证明这是一个PSPACE完全问题。作为推论，我们得到了监管当局合理消除和合理构建纳什均衡都是PSPACE完全问题。
2016-07-12 cs.GT cs.LO
Automata-less Monitoring via Trace-Checking (Extended Version)
Department of Mathematics, Computer Science and Physics University of Udine（乌迪内大学数学、计算机与物理系）
针对运行时验证中DFA监控器双指数爆炸问题，提出基于内蕴安全/共安全公式的迹检查监控方法，复杂度为多项式级，并明确了LTL和LTLf中识别这类公式的复杂度。
2025-11-14 cs.FL cs.LO
Asynchronous Composition of LTL Properties over Infinite and Finite Traces
Fondazione Bruno Kessler（布鲁诺·克斯特勒基金会）；University of Trento（特伦托大学）
本文提出了一种新的LTL重写方法，用于验证异步软件组件在无限和有限轨迹上的LTL属性，通过优化公式大小并保持时间属性不变，以提高验证效率。
2026-02-13 cs.LO
On the Complexity of Rational Verification
Monash University（莫纳什大学）；University of Kaiserslautern（凯泽斯劳滕大学）；Sapienza University of Rome（罗马第一大学）；University of Oxford（牛津大学）
理性验证是指检查并发多智能体系统的时间逻辑属性的问题，假设系统中的代理选择形成博弈论均衡的策略。理性验证可以被理解为多智能体系统的模型检验的对应物，但是虽然经典的模型检验可以在多项式时间内完成一些时态逻辑规约语言，如CTL，多项式空间与LTL规范，理性验证要困难得多：理性验证的关键决策问题是2 EXPTIME-完全与LTL规范，即使使用显式状态系统表示。在此背景下，我们在本文中的贡献是三方面的。首先，我们表明，合理验证的复杂性可以大大降低限制规格GR（1），一个片段的LTL，可以代表一个广泛的和实际有用的一类反应系统的响应特性。特别是，我们表明，对于一些相关的设置，合理的验证可以在多项式空间，甚至在多项式时间。其次，我们提供了改进的复杂性结果，合理的验证时，考虑球员的目标给出的平均回报效用函数，可以说是最广泛使用的方法，在并发和多智能体系统的定量目标。最后，我们考虑了满足社会福利约束的计算结果的问题。为此，我们考虑功利主义和平等主义的社会福利，并表明计算这样的结果是PSPACE完全或NP完全。
2022-07-06 cs.AI cs.LO cs.MA
Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)
Free University of Bozen-Bolzano（博尔扎诺自由大学）；University of Toronto（多伦多大学）
本文针对有限迹LTL的预期监控，提出基于递进与LTLf可满足性检查的替代方法，实验表明其在算术设置下优于自动机方法，结合两者在命题设置下权衡良好。
2026-09-29 cs.AI cs.LO
Monitoring Bounded LTL Properties Using Interval Analysis
Tokyo Institute of Technology（东京工业大学）；CNRS, IRCCyN（法国国家科学研究中心，IRCCyN）
本文提出一种区间方法用于验证由有界线性时序逻辑描述的属性，通过前向模拟混合自动机并传播时间区间来验证属性，证明了问题的可判定性。
2015-07-14 cs.LO cs.NA cs.SY
NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
Baylor University（贝勒大学）
提出NeuroNL2LTL神经符号框架，通过验证器在环训练和最小编辑修复机制，实现自然语言到线性时序逻辑的高可靠性翻译，在20万+需求上达到86%的可满足性输出。
2026-05-20 cs.AI cs.LO
On Relaxing Metric Information in Linear Temporal Logic
度量LTL公式依赖于next运算符来编码时间距离，而定性LTL公式仅使用until运算符。本文展示了如何将任何度量LTL公式M转换为定性公式Q，使得Q是可满足的当且仅当M在关于M中使用的最大距离的可变性有界的词上是可满足的（即，下一个的出现），但是Q的大小与这样的距离无关。除了理论上的兴趣，这一结果可以帮助简化验证系统的时间粒度的异质性，需要大的距离来表达粗粒度的动态细粒度的时间单位。
2011-06-17 cs.LO
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
我们提出RVHyper，一个运行时验证工具的hyperproperties。超性质，如非干涉性和观察决定论，将多个计算轨迹相互关联。规范在时态逻辑HyperLTL中以公式的形式给出，它扩展了线性时间时态逻辑（LTL）的跟踪量词和跟踪变量。RVHyper按顺序处理执行跟踪，直到检测到违反规范。在这种情况下，将返回一组跟踪形式的反例。作为一个示例应用程序，我们展示了如何RVHyper可以用来检测虚假的依赖关系，在硬件设计。
2019-05-31 cs.LO
A Temporal Logic of Security
提出了一种新的安全策略验证逻辑。该逻辑HyperLTL扩展了线性时间时态逻辑（LTL），并在多个执行路径上使用连接词进行显式和同时量化，从而使HyperLTL能够表达LTL无法表达的信息流安全策略。给出了一个HyperLTL片段的模型检测算法，并在原型模型检测器中实现了该算法。在HyperLTL中可表达的安全策略类的特征在于超属性的算术层次结构。
2013-07-09 cs.CR cs.LO
Efficient Offline Monitoring of Linear Temporal Logic with Bit Vectors
位图是一种数据结构，用于压缩表示整数集合;它提供了非常快速的查询和操作这些集合的操作，利用位级并行性。在本文中，我们描述了一种技术，离线验证的任意表达式的线性时序逻辑使用位图操作。首先对事件跟踪进行预处理并将其转换为一组位图。然后通过操作这些位图的递归过程来计算LTL表达式。实验结果表明，复杂的LTL公式包含近20个操作符，事件跟踪可以评估在每秒数百万个事件的吞吐量。
2020-05-24 cs.LO
Temporal Logics for Hyperproperties
提出了两种新的超性质验证逻辑。超属性将安全策略（如不干涉）表征为计算路径集的属性。标准的时态逻辑，如LTL、CTL和CTL*，一次只能引用一条路径，因此不能表达许多感兴趣的超性质。这里提出的逻辑，HyperLTL和HyperCTL*，在多个路径上向LTL和CTL* 添加显式和同时量化。这种量化使得能够表达超性质。给出了该逻辑的模型检验算法。针对HyperLTL的一个片段，实现了一个原型模型检测器。
2014-01-21 cs.LO
HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications
University of Colorado Boulder（科罗拉多大学博尔德分校）
本文提出一种归纳框架，通过超证书概念验证离散时间动态系统 against 超LTL规范。方法结合前瞻函数与屏障函数，利用闭包证书和SOS/SMT技术实现自动验证。
2026-05-01 cs.LO cs.SY eess.SY
CTL* Verification and Synthesis using Existential Horn Clauses
Technion - Israel Institute of Technology（以色列理工学院）
本文提出基于存在性Horn子句（EHCs）的自动验证与合成方法，用于无限状态反应程序对CTL*规格的验证，展示了其在复杂系统中的应用。
2024-08-21 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
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
Verification of Switched Stochastic Systems via Barrier Certificates
提出了一种连续时间切换随机系统的时序逻辑验证方法。我们的目标是找到一个复杂的时间属性满足在有限的时间范围内的概率的下限。所需的时间属性的系统表示使用一个片段的线性时序逻辑，称为安全的LTL相对于有限的痕迹。我们的方法结合了基于自动机的验证和屏障证书的使用。它依赖于分解的自动机与规范的否定成一系列更简单的可达性任务和计算这些可达性概率的上限，通过共同的或多个障碍证书。通过应用反例引导归纳合成框架来寻找障碍证书，说明了理论结果。
2021-09-25 cs.LO cs.SY eess.SY
Verifying nondeterministic probabilistic channel systems against $ω$-regular linear-time properties
有耗信道系统（Lossy Channel Systems，LCS）是一种通过不可靠的无界FIFO信道进行通信的有限状态自动机系统。为了规避不确定LCS的模型检验的不确定性，引入了概率模型，其中可以确定线性时间属性是否几乎肯定成立。然而，这样的完全概率系统不是非确定性协议的忠实模型。我们研究了一个混合模型的LCS的消息丢失被视为故障发生的一些给定的概率，系统的内部行为仍然是不确定的。因此，语义是在无限状态马尔可夫决策过程。本文的目的是讨论由线性时态逻辑（LTL）公式形式化的线性时间性质的可判定性。我们的重点是定性设置，其中一个问，例如，LTL公式几乎肯定成立还是零概率成立（如果公式描述了不良行为）。令人惊讶的是，事实证明，-在有限状态马尔可夫决策过程-LTL公式的满意度关系取决于所选择的类型的决策者，解决了不确定性。虽然所有的变量的定性LTL模型检验问题的完整类的历史相关的调度器是不可判定的，同样的问题，有限内存调度器可以解决算法。然而，可达性属性和特殊种类的经常性可达性属性的限制产生可判定的验证问题的完整类的验证，其中-这类限制的属性-是强大的有限内存的验证，甚至是他们的子类。
2006-04-11 cs.LO
From Specifications to Behavior: Maneuver Verification in a Semantic State Space
fortiss GmbH（福蒂斯有限公司）；Technische Universität München（慕尼黑工业大学）
为了在可预见的未来实现自动驾驶汽车的市场进入，行为规划系统将需要遵守与人类相同的规则。如果不妥善解决审批陷阱，就无法强制执行产品责任。在本文中，我们定义了一个语义抽象的连续空间和形式化的交通规则的线性时序逻辑（LTL）。语义状态空间中的序列表示高级规划者可以选择执行的策略。我们检查这些演习对正式的交通规则，使用运行时验证。通过使用标准的模型检查器NuSMV，我们证明了我们的方法的有效性，并提供运行时属性的机动验证。我们表明，高层次的行为可以在语义状态空间中进行验证，以满足一组形式化的规则，这可以作为一个步骤，实现预期的功能安全。
2019-11-29 cs.LO cs.RO
Synthesis of Sequential Extended Regular Expressions for Verification
综合技术采用可实现的线性时序逻辑规范，并产生实现规范的正确电路。生成的电路可以直接使用，也可以用作检查逻辑设计正确性的斜接。通常，这些技术生成非确定性有限状态自动机，其可以以可能的指数代价确定。最近的研究结果表明，使用确定性自动机的符号和有界模型检验的LTL安全性能的多个优点。在本文中，我们提出了一种技术与支持工具，采取一个顺序扩展的正则表达式规范Φ，和一个逻辑设计实现S，并生成一个时序电路C，表示为一个与反转图，检查是否S满足Φ。该技术将生成的电路C传递给有界模型检查器ABC，以验证正确性。我们用自由输入变量对Φ中的不确定性进行编码，得到了许多状态，它们与Φ的大小成斜接线性关系。我们的技术成功地生成了模型检查器的输入，而其他技术由于指数爆破而失败，并且在大多数情况下，ABC成功地找到了设计中的缺陷，否则无法检查，或者验证了设计。我们评估了我们的技术对几个工业基准，包括IBM仲裁器，负载平衡器，和交通灯系统，并比较我们的结果与NuSMV框架。我们的方法发现了缺陷，并且验证了NuSMV无法验证的系统。
2014-01-14 cs.FL cs.LO
Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers
本文提出将非嵌套离散时间 STL 公式编码为 Lustre 同步观察器，提供三值在线语义以支持性质验证与反例搜索，并通过仪表化证明确保实现正确性，实验使用 Kind2 和 Z3 自动化完成。
2023-11-16 cs.LO
Debugging of Web Applications with Web-TLR
Web-TLR是一个Web验证引擎，它基于成熟的重写逻辑--Maude/LTLR串联，用于Web系统规范和模型检查。在Web-TLR中，Web应用程序被表示为重写理论，可以通过使用Maude内置的LTLR模型检查器进行形式化验证。每当一个属性被反驳时，就会传递一个反例跟踪，揭示一个不希望的错误导航序列。不幸的是，分析（或甚至简单的检查）这样的反例可能是不可行的，因为在检查的痕迹的大小和复杂性。在本文中，我们赋予Web-TLR一个新的Web调试设施，支持有效的操作反例的痕迹。这个设施是基于一个向后跟踪切片技术重写逻辑理论，允许我们感兴趣的信息片段，通过反向重写序列追溯。切片过程通过丢弃不影响最终结果的无用数据，大大简化了计算跟踪。通过使用这个工具，Web工程师可以专注于失败应用程序的相关片段，这大大减少了手动调试工作，也减少了迭代验证的数量。
2011-08-11 cs.LO cs.SE
Contract-based Design and Verification of Multi-Agent Systems with Quantitative Temporal Requirements
本文提出定量假设-保证契约，实现多智能体系统在定量时间逻辑LTL[$\mathcal{F}$]规范下的组合式设计与验证，提高可扩展性和模块化。
2024-12-17 cs.LO
A Verified Approach for Checking Real-Time Specification Patterns
我们提出了一个验证方法的形式化验证的时间属性使用模型检查技术。我们专注于使用实时的【形】规范模式，它可以被看作是一个子集的定时时序逻辑，包括反应系统的分析过程中常见的属性表示的属性。我们的模型检测方法是基于使用观察员，以转换到验证更简单的LTL公式的验证定时模式。虽然使用观察员的模型检查是很常见的，我们的贡献是原始的几个方面。首先，我们定义了一个正式的框架来验证我们的观察者是正确的和非侵入性的。其次，我们为每个模式定义不同的观察者类别，并使用务实的方法，以选择最有效的候选人在实践中。这种方法是实现在一个集成的验证工具链的Fiacre语言。
2013-01-31 cs.LO
Model checking memoryful linear-time logics over one-counter automata
我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。
2010-01-18 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
Temporal Hyperproperties for Population Protocols
本文研究无限状态系统群体协议的时序超性质，证明一般群体协议的HyperLTL验证不可判定，并指出即时观察子类在不包含next算子时验证可判定（2-EXPSPACE），任何扩展均导致不可判定。
2024-10-15 cs.LO
AgentLTL: A Trace-Verification Framework for Measuring, Enforcing, and Training Procedural Compliance in Tool-Using LLM Agents
EPITA；Bpifrance
介绍基于一阶线性时态逻辑的AgentLTL语言，用于表达代理跟踪的程序规则，产生确定性无评判的合规分数，此框架可用于约束和微调，提升模型合规性与准确性。
2026-07-07 cs.AI cs.LO cs.SE
A Simplification of a Real-Time Verification Problem
我们重新审视了使用超时和日历模型的密集动态实时的【形】验证问题，并将其简化为有限状态验证问题。为了克服具有密集动态的实时的【形】系统验证的复杂性，Dutertre和Sorea提出了基于超时和超时的转换系统来建模实时的【形】系统的行为，并使用k-归纳法与有界模型检验相结合来验证安全属性。在这项工作中，我们介绍了这些模型的规范形式主义的时间转换图和捕捉他们的行为的语义方面的时间转换系统。此外，我们讨论了一种技术，它减少了问题的验证定性的时间属性的无限状态空间的（一个大的片段）这些超时和基于转换系统到无时钟的有限状态模型，通过一个两步的过程，包括数字化和规范的有限减少。这种技术使我们能够验证安全不变量的实时的【形】系统使用有限状态模型检查，避免了复杂的无限状态（有界）模型检验和规模的模型，而无需应用技术从基于归纳的证明方法。此外，我们可以验证实时的【形】系统的活性属性，这是不可能通过使用无限状态模型检查器的归纳法。我们提出的例子菲舍尔的协议，列车门控制器，和TTA启动算法，以说明这种方法可以有效地用于验证安全性，活性，并在LTL使用有限状态模型检查器，如SAL-SMC和自旋的时间属性。我们还演示了如何先进的建模概念，如间进程调度，优先级，中断，紧急和承诺的位置可以指定为扩展所提出的规范形式主义。
2010-08-08 cs.LO cs.SE
