Model checking strategy-controlled systems in rewriting logic
本文针对 Maude 内置 LTL 模型检测器无法验证策略控制规约的问题，提出策略感知扩展，并结合表达力分析、应用示例和性能比较验证其有效性。
2024-01-15 cs.LO
Converting Reconfigurable Petri Nets to Maude
模型检验是理论计算机科学的一个重要研究方向。它可以验证具有一组属性（如活性，死锁或安全性）的模型。典型的建模技术之一是Petri网，它们被很好地理解并且可以用于模型检验。可重构Petri网是基于一组规则的Petri网。这些规则可以动态地用于改变网络。缺少的是验证可重构网络和死锁或活性等属性的可能性。本文介绍了一个转换可重构Petri网Maude，使我们能够填补空白。提出了一种基于Maude方程-重写逻辑和LTLR模型检验器的网变换方法。
2014-11-12 cs.FL cs.LO
Variable and clause elimination for LTL satisfiability checking
研究了LTL公式子句范式的预处理技术。应用标记子句的机制，使我们能够重新解释LTL可满足性作为一组纯粹的命题问题，从而转移简化思想从SAT到LTL。我们证明了这一点，适应变量和子句消除，现代SAT求解器使用的一个非常有效的预处理技术。我们的实验证实，即使在时间设置的公式大小和随后的求解器运行时间的减少，可以实现大幅减少。
2013-09-30 cs.LO
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
LIPN CNRS UMR 7030 Université Sorbonne Paris Nord（巴黎北大学国家科学研究中心联合研究实验室）；Pohang University of Science and Technology（韩国科学技术院）；University of Oslo（奥斯陆大学）
本文提出了一种用于参数时间Petri网的形式化分析与参数综合框架，利用重写逻辑与SMT求解器实现精确语义分析，通过符号可达性方法实现参数综合，实验表明方法在多个方面优于现有工具。
2024-09-12 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
Model Checking Constraint LTL over Trees
约束自动机是Büchi自动机的一种改进，它处理来自某种关系结构S的数据字。这样一个自动机的每一个转换都带有S的关系的约束。只有当当前和下一个数据值满足转换的所有约束时，才能触发转换。这些自动机已被用于设置，其中S是一个线性顺序，以确定约束LTL的约束S。在本文中，S是无限分枝的无限阶树T。给出了T-约束自动机空性的PSPACE算法。这一结果暗示了T上约束LTL的可满足性和模型检验问题的PSPACE完备性。
2015-04-23 cs.LO
Truly On-The-Fly LTL Model Checking
我们提出了一种新的算法，基于自动机的LTL模型检验，交错的公式的否定和空检查的广义Büchi自动机的建设。我们的算法首先将LTL公式转换成线性弱交替自动机;交替自动机的配置对应于广义Büchi自动机的位置，并且Tarjan算法的变体用于确定过渡系统和自动机的产品的接受运行的存在。因为我们避免了一个明确的建设的Büchi自动机，我们的方法可以产生显着的改善，在运行时间和内存中，大型LTL公式。该算法已在SPIN模型检查器中实现，并给出了一些基准示例的实验结果。
2005-11-16 cs.LO
Algorithmic metatheorems for decidable LTL model checking over infinite systems
通过算法元定理的模型检验问题P在无限状态系统，我们的意思是通用的结果，可以用来推断的可判定性（可能的复杂性）的P不仅在一个特定的类的无限系统，但在一个大家庭的类的无限系统。这样的结果通常开始于一个强大的形式主义的无限状态系统，其中P是不可判定的，并断言可判定时，通过一个额外的“语义条件”C的限制。我们证明了各种算法的元定理的问题的模型检验LTL和它的两个共同的片段LTL（Fs，Gs）和LTLdet的表达类的字/树自动转换系统，这是由有限的字和树上操作的同步有限状态转换器。我们提出了许多应用程序，在那里我们得到（以统一的方式）模型检验LTL及其片段在特定类别的无限状态系统上的许多已知和先前未知的可判定性和复杂性结果，包括下推系统;前缀可识别系统;具有离散时钟和自由计数器的反向有界计数器系统;具有有界数目的上下文切换的并发下推系统; Petri网的各种子类;弱扩展PA过程;和弱扩展地树重写系统。在所有情况下，我们都能够得到最优（或接近最优）的复杂度。最后，我们查明的确切位置在算法和分析层次的问题，检查相关的语义条件和LTL模型检验问题在所有字/树自动系统。
2009-10-26 cs.LO
On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems
考虑由方阵$M \in \mathbb{Q}^{d \times d}$和起点$s \in \mathbb{Q}^d$给出的离散动力系统。这种系统的轨道是无限轨道$\langle s, Ms, M^2s, \ldots\rangle$。给定一个半代数集合的集合$T_1, T_2, \ldots, T_m \subseteq \mathbb{R}^d$，我们可以将每个$T_i$与一个原子命题$P_i$相关联，该命题在时间$n$处评估为真，当且仅当$M^ns \in T_i$。这就产生了离散线性动力系统的LTL模型检验问题：给定这样一个系统$(M,s)$和这样一个原子命题上的LTL公式，确定轨道是否满足公式。本文的主要贡献是证明了离散线性动力系统的LTL模型检验问题在3维或更小维上是可判定的。
2020-07-09 cs.LO
LTL Model Checking of Self Modifying Code
自修改代码是可以在程序执行期间修改其自身指令的代码。它被恶意软件编写者广泛用于混淆其恶意代码。因此，分析自修改代码现在是一个很大的挑战。本文研究了自修改代码的LTL模型检测问题。我们使用自修改下推系统（SM-PDS），下推系统的扩展，可以修改自己的一套过渡在执行过程中，这样的程序建模。我们把LTL模型检测问题归结为自修改Büchi下推系统（SM-BPDS）的空性问题。我们在一个工具中实现了我们的技术，我们成功地应用于检测几个自我修改的恶意软件。我们的工具还能够检测几个恶意软件，知名的反病毒软件，如BitDefender，Kinsoft，Avira，eScan，卡巴斯基，奇虎360，百度，Avast和赛门铁克未能检测到。
2019-09-27 cs.LO
Constraint LTL Satisfiability Checking without Automata
本文提出了一种新的方法来判定用线性时态逻辑语言写的带有将来和过去算子的公式和属于约束系统D的原子公式的可满足性（简称CLTLB（D））。该技术基于有界可满足性的概念，并将CLTLB（D）公式编码为QF-EUD，结合了无量词等式理论和D.类似于标准LTL，其中有界模型检查和SAT求解器可以用作自动机理论方法的模型检查的替代方案，我们的方法允许用户通过SMT求解技术来解决CLTLB（D）公式的可满足性问题，而不是通过检查合适的自动机A_A的语言的空性。该技术是有效的，并已在我们的Zot形式化验证工具中实现。
2014-02-11 cs.LO
Fast LTL Satisfiability Checking by SAT Solvers
线性时态逻辑（LTL）的可满足性检查是检查LTL断言中可能错误的基本步骤。现存的LTL可满足性检查器使用各种不同的搜索过程。唯一的例外是基于有界模型检验的LTL可满足性检验，它没有提供一个完整的决策过程，LTL可满足性检验器没有利用过去20年在布尔可满足性求解方面取得的显著进展。在本文中，我们提出了一个新的LTL可满足性检查框架，加速使用布尔SAT求解器。我们的方法是基于变体的\emph{obligation-set method}，我们提出了在早期的工作。我们在这里描述了允许使用布尔SAT求解器来分析给定LTL公式的义务的算法。实验评估表明，新的方法提供了一个显着的性能优势。
2014-04-29 cs.DS cs.LO
Verifying LTL for Infinite State Systems via Termination Analysis
RWTH Aachen University（亚琛工业大学）
提出框架MoAT，将无限状态系统的LTL模型检验归约为公平终止问题，并利用终止分析工具KoAT和LoAT进行验证，实验表明与现有工具性能相当。
2026-06-17 cs.LO
Linear Encodings of Bounded LTL Model Checking
研究线性时序逻辑的有界模型检验问题。我们提出了几个有效的编码，具有大小线性的界限。此外，我们展示了如何编码可以扩展到LTL与过去的运营商（PLTL）。广义编码仍然是线性的大小，但不能检测最小长度的反例。通过使用虚拟展开技术可以捕获最小长度的反例，然而，在规范中编码的大小是二次的。我们还扩展虚拟展开的Buchi自动机，使他们能够接受最小长度的反例。我们的BMC编码可以是增量的，以便从增量SAT技术中受益。通过相当小的修改，增量编码可以通过终止检查进一步增强，允许我们使用BMC证明属性。实验清楚地表明，我们的新编码大大提高了BMC的性能，特别是在增量编码的情况下，并且它们在发现错误方面非常有竞争力。对活性到安全性转换的分析揭示了本文中BMC编码的许多相似之处。使用基于BDD的不变式检查的活性到安全性的转换结果在一个有效的方法来找到最短的反例，补充基于BMC的方法。
2006-11-16 cs.LO
Model Checking Branching Properties on Petri Nets with Transits (Full Version)
为了对并发系统进行模型检验，区分数据流和控制流是很方便的。正确性是在数据流级别上指定的，而系统是在控制级别上配置的。带变迁的Petri网和Flow-LTL是相应的形式体系。在Flow-LTL中，数据流的正确性以及控制的公平性和最大性的假设都以线性时间表示。到目前为止，分支行为不能指定的Petri网与过境。在本文中，我们引入Flow-CTL* 来表达数据流的预期分支行为，同时保持LTL的公平性和最大化假设的控制。我们编码的物理访问控制与策略更新的Petri网与过境，并给出标准的要求在流CTL *。在模型检验方面，我们通过构造自动机将Flow-CTL* 的带变迁Petri网的模型检验问题归结为LTL的Petri网的模型检验问题。因此，可以验证在无限数量的人的公平性假设下具有策略更新的物理访问控制。
2020-07-14 cs.LO
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
概率系统的模型检测问题主要依赖于将LTL转换为确定性Rabin自动机（DRW）。我们最近的Safraless翻译的LTL（F，G）片段产生较小的自动机相比，传统的方法。在这项工作中，而不是DRW，我们认为确定性自动机的接受条件作为广义拉宾对（DGRW）的析取。与DRW相比，LTL（F，G）公式到DGRW的Safraless翻译导致更小的自动机。我们提出了概率模型检测算法以及DGRW条件下的博弈求解。我们的新算法在理论界和实际评价方面都有所改进。我们比较PRISM与我们的新的翻译，并表明，新的翻译导致显着的改善。
2013-04-18 cs.FL cs.LO
Model Checking Flat Freeze LTL on One-Counter Automata
本文解决了单计数器自动机上平坦冻结线性时序逻辑模型检测的可判定性开放问题，通过归约到带参数化相等性测试的可达性问题并转化为Presburger算术证明其可判定。
2018-12-06 cs.FL cs.LO
Predicting the Results of LTL Model Checking using Multiple Machine Learning Algorithms
School of Information Engineering, Zhengzhou University（郑州大学信息工程学院）
本文研究了如何利用一些机器学习算法预测LTL模型检验的结果。将Kripke结构和LTL公式及其模型检验结果组成数据集。采用基于随机森林（RF）、K-最近邻（KNN）、决策树（DT）和逻辑回归（LR）的方法进行训练和预测。实验结果表明，基于RF、KNN、DT和LR的方法的预测准确率分别为97.9%、98.2%、97.1%和98.2%，平均计算效率分别是现有方法的7102500、598、4132364和5543415倍，如果每个LTL公式的长度为500，则分别为。
2019-02-21 cs.LG cs.LO
Equational and Inductive Reasoning for Maude in Athena
Universidad de los Andes（安第斯大学）；Rensselaer Polytechnic Institute（伦斯勒理工学院）；Pontificia Universidad Javeriana（哈维里亚纳天主教大学）
本文提出maude2athena框架，将Maude的等式理论转换为Athena，支持归纳推理和演绎推理，保持语义并确保简洁性，促进模型检查与定理证明的结合。
2026-04-21 cs.LO
A CEGAR-like Approach for Cost LTL Bounds
定性的形式化验证，即寻找关于系统行为的布尔答案，通常不足以满足实际目的。观察定量信息是感兴趣的，例如，用于电池或实时调度器的适当校准。从历史上看，重点一直是在一个连续的领域的数量，但近年来显示了离散的定量域的新的兴趣。代价线性时序逻辑是经典线性时序逻辑的一种定量扩展。它集成到一个很好的理论，在过去几年中，扩展了定性设置，与同行的逻辑，自动机和代数结构。我们提出了一个实际使用的逻辑模型检查的目的。CLTL公式定义了一个从无限单词到整数的函数。在给定的一组单词上找到这样一个函数的边界可以被看作是LTL通用和存在模型检查的扩展。我们提出了一个基于经典LTL模型检验的类CEGAR算法，并使用带计数器的Büchi自动机实现了该算法，为离散定量逻辑的实际应用迈出了第一步.
2015-06-18 cs.LO
The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments
在1985年的一篇开创性论文中，Sistla和Clarke证明了线性时态逻辑（LTL）的模型检验问题是NP完全的或PSPACE完全的，这取决于所使用的时态运算符的集合。相反，如果命题算子的集合是有限的，复杂性可能会降低。本文系统地研究了命题算子和时态算子限制集上LTL公式的模型检验问题。对于几乎所有的时间和命题运算符的组合，我们确定是否模型检验问题是易处理的（在P）或难处理的（NP难）。然后，我们专注于易处理的情况下，表明他们都是NL-完全的，甚至对数空间可解。这导致了一个令人惊讶的差距之间的复杂性和棘手的案件。值得注意的是，我们的分析涵盖了无限的问题集，因为有无限多组命题算子。
2008-05-05 cs.CC cs.LO
Simplifying LTL Model Checking Given Prior Knowledge
本文提出利用先验知识自动机简化LTL模型检测中的否定性质自动机，从而提升检测效率；实验表明在MCC'22基准上可显著简化或直接解决一半问题。
2025-03-28 cs.FL 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
Fairness and promptness in Muller formulas
本文研究了线性时序逻辑（LTL）的通用与公平模型检验问题，发现pLTL的Muller片段在复杂度比较上不具备相同算法特性，并识别出一个公平模型检验快于通用检验的新表达性片段。
2024-09-27 cs.LO
Counterexample-Preserving Reduction for Symbolic Model Checking
LTL模型检验的成本对验证公式的长度高度敏感。我们观察到，在某些特定的条件下，输入LTL公式可以减少到一个制造商到处理之前的模型检验。在我们的约简中，这两个公式不需要在逻辑上等价，但它们在模型中共享相同的反例集。在模型被象征性地表示的情况下，能够以轻量级的努力（例如，解决问题）。在本文中，我们尝试将这种技术命名为“反例保持约简”（简称CePRe），最后通过采用NuSMV对所提出的技术进行了实验评估。
2013-01-15 cs.LO
OCTAL: Graph Representation Learning for LTL Model Checking
Purdue University（普渡大学）
针对传统符号模型检测的状态空间爆炸问题，提出基于图表示学习的OCTAL框架，将LTL模型检测转化为二分类任务，实现了显著的准确率与最高11倍的整体加速。
2023-08-19 cs.AI cs.LO cs.SE
LTL Model-Checking for Dynamic Pushdown Networks Communicating via Locks
动态下推网络（Dynamic Pushdown Network，DPN）是一组下推系统（Pushdown Systems，PDS），其中每个进程都可以动态地创建新的PDS实例。DPN是具有（可能是递归的）过程调用和线程创建的多线程程序的自然模型。使用锁扩展DPN允许进程彼此同步。因此，带锁的DPN是一种很好的形式主义，可以对通过锁进行同步的多线程程序进行建模。因此，为带锁的DPN提供模型检验算法是很重要的。在这项工作中，我们认为模型检验的DPN与锁对单索引的LTL属性的形式V fi s. t。fi是在PDS i上解释的LTL公式。我们考虑模型检验问题w.r.t.简单赋值（即，配置是否满足原子命题仅取决于其控制位置和持有的锁）和w.r.t.定期评估（即，满足原子命题的配置集合是配置的规则集合）。我们证明了这些模型检验问题是可判定的。
2016-10-11 cs.LO cs.PL cs.SE
Bounded LTL Model Checking with Stable Models
本文介绍了异步并发系统的有界模型检验，作为回答集编程的一个很有前途的应用领域。作为异步系统的通信自动机，1-安全Petri网的推广模型，使用。它示出了如何1-安全的Petri网和对网络的行为的要求可以被翻译成一个逻辑程序，这样的有界模型检验问题的网可以通过计算相应的程序的稳定模型来解决。稳定模型语义的使用导致有界可达性和死锁检测任务的紧凑编码，以及线性时序逻辑的有界模型检验的更一般的问题。给出了所设计的翻译的正确性证明，并给出了使用该翻译和Smodels系统的一些实验结果。
2003-05-23 cs.AI cs.LO
Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic
本文提出了一种近似方法来验证计数器系统相对于线性时态逻辑的表达计数扩展中制定的属性。它可以表达，例如，通过对运行中的特定位置进行计数并施加算术约束，确保应答的数量永远不会超过对服务的请求的数量。所解决的问题是不可判定的，因此解决了平坦的下近似的系统。这提供了一个灵活的可调整的穷举和计算工作量之间的权衡，类似于有界模型检验。最近的技术和结果的平坦Kripke结构的模型检查频率特性的解除和构造一个参数化编码的（近似）问题的量化器免费Presburger算法。基于z3 SMT求解器的原型实现证明了基于RERS挑战赛问题的方法的有效性。
2019-01-17 cs.LO cs.SE
Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking
我们提出了两种新的混合技术，取代同步产品中使用的自动机理论方法的LTL模型检验。建议的产品是明确的图形的聚集（符号集的状态），可以解释为Büchi自动机。这些混合方法一方面允许使用经典的空检查算法并在运行中构建图，另一方面，由于聚集体的符号表示，具有状态空间的紧凑编码。符号观测产品假设全局断续属性（例如，LTL \ X）来聚合状态。自循环聚合产品}不要求属性是全局断续的（即，它可以处理完整的LTL），但在可能的情况下动态地检测和利用一种形式的口吃。我们的实验表明，这两个变种，而彼此无法比拟的，可以优于其他现有的方法。
2011-06-28 cs.FL cs.LO
Polsat: A Portfolio LTL Satisfiability Solver
在本文中，我们提出了一个投资组合LTL可满足性求解器，称为Polsat。为了实现LTL公式的快速可满足性检查，该工具集成了四个代表性的LTL求解器：pltl，TRP++，NuSMV和Aalta。Polsat的思想是并行运行组件求解器以获得最佳的整体性能;一旦其中一个求解器终止，它将停止所有其他求解器。值得注意的是，Polsat求解器利用了现代多核计算集群的强大功能。实验结果表明，Polsat充分利用了LTL求解器的优势，同时也是所有LTL求解器的测试平台。
2013-11-07 cs.LO
Second-Order Hyperproperties
本文提出支持对迹集合进行二阶量化的时间逻辑Hyper$^2$LTL，以表达公共知识等复杂超性质，并针对受限片段设计了基于不动点迭代和自动机学习的近似模型检测算法，在工具HySO中验证有效。
2023-05-29 cs.LO
Model checking memoryful linear-time logics over one-counter automata
我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。
2010-01-18 cs.LO
Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
近年来，基于区间时态逻辑的模型检验作为基于标准点时态逻辑（如LTL、CTL、CTL* 等）的模型检验的可行替代方案而出现。像往常一样，系统的行为通过（有限）Kripke结构来建模。然而，虽然被解释为“逐点”的时间逻辑描述了系统如何逐状态地演变，以及系统状态的谓词属性，但那些被解释为“逐区间”的时间逻辑表达了计算延伸的属性，跨越了一系列状态。假设一个命题字母在一个计算延伸（间隔）上保持不变，当且仅当它在每个分量状态上保持不变（同质性假设）。一个自然的问题出现了：用间隔代替点作为主要的时间实体有什么好处，或者这只是一个品味问题？本文研究了Halpern和Shoham的区间时态逻辑（HS）在模型检验中的表达能力，并与LTL、CTL和CTL* 进行了比较。为此，我们考虑HS的三种语义变体：基于状态的变体，由Montanari等人引入，它允许时间在过去和将来都分支，基于计算树的一个，它只允许时间在将来分支，基于轨迹的变体，它不允许时间分支。这些变体相互比较，并与上述标准逻辑进行比较，得到一个完整的画面。特别是，我们表明，HS与跟踪为基础的语义是相当于LTL（但至少指数更简洁），HS与计算树为基础的语义是相当于有限的CTL*，和HS与基于状态的语义是无法比拟的所有这些（LTL，CTL和CTL*）。
2018-09-24 cs.LO
Improved Bounded Model Checking of Timed Automata
时间自动机（TA）是一个非常流行的建模形式主义的时间敏感的属性。一个常见的任务是验证TA的网络是否满足给定的属性，通常用线性时态逻辑（LTL）或时间计算树逻辑（TCTL）的子集表示。在本文中，我们建立在TACK有界模型检查TA，它支持基于信号的语义TA和更丰富的度量区间时态逻辑（MITL）。TACK将TA网络和属性编码为LTL的变体，即时钟约束LTL（CLTLoc）。产生的CLTLoc公式然后可以通过诸如Zot的工具求解，该工具将CLTLoc属性转换为可满足性模理论（SMT）求解器的输入逻辑。我们提出了一种新的方法，保留TACK的MITL属性的编码，同时直接到SMT求解器语言编码的TA网络，利用BitVector逻辑和逻辑的实算术。我们还介绍了几个优化，使我们能够显着优于CLTLoc编码在许多实际情况下。
2021-04-26 cs.LO
Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking
下推系统（PDS）是递归程序的一种抽象模型，下推系统的模型检验方法已得到研究。寄存器PDS（RPDS）是由寄存器扩展的PDS，以有限的方式处理来自无限域的数据值。一个线性时序逻辑（LTL）模型检验方法已被提出的RPDS与定期估值，但该方法要求用于表示一个定期估值的寄存器自动机（RA）是向后确定的。本文提出了另一种方法来解决同样的问题，其中的模型检验问题的RPDS归结为PDS的问题，通过构造一个PDS互模拟等价于一个给定的RPDS。所提出的方法的结构比以前的模型检验方法更简单，不需要RA确定性或后向确定性，互模拟等价性清楚地保证了这种减少的正确性。另一方面，所提出的方法要求每个RPDS（和RA）具有新鲜度属性，其中每当RPDS用未存储在任何寄存器或栈顶中的数据值更新寄存器时，该值应该是新鲜的。本文还表明，这种模型检验问题的定期评估定义的一般RA是不可判定的，因此新鲜度约束是必要的，在所提出的方法。
2022-03-22 cs.FL cs.LO
Traversing automata with current state uncertainty under LTL$_f$ constraints
本文研究路径上的LTL$_f$模型检测问题，识别出多项式空间可解的一般条件，并针对零件定向问题中的特定约束给出PSPACE完全和NP完全情形，同时证明同步性约束不改变复杂度。
2023-11-29 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
Formal Visual Modeling of Real-Time Systems in e-Motions: Two Case Studies
e-Motions是一个基于时间的可视化模型转换框架，具有实时的【形】Maude语义，支持通常的Maude形式化分析方法，包括模拟，可达性分析和LTL模型检验。e-Motions的特点是一套新颖而强大的结构，用于表达定时行为。在本文中，我们说明了使用这些结构-从而隐含地调查其适用性，以直观的方式定义实时的【形】系统-定义和正式分析两个原型和非常不同的实时的【形】系统：（一）一个简单的往返时间协议计算的时间，它需要一个消息从一个节点到另一个节点，并返回;（二）EDF调度算法。
2011-06-30 cs.LO cs.SE
Parametric Linear Dynamic Logic (full version)
我们介绍参数线性动态逻辑（PLDL），它扩展了线性动态逻辑（LDL）的时间运营商配备参数，约束其范围。LDL本身是作为线性时序逻辑（LTL）的扩展而提出的，它能够表达所有的ω-正则规范，同时仍然保持LTL的许多理想属性，如直观的语法和语义，并转换为指数大小的非确定性Büchi自动机。但是LDL缺乏表达时间约束的能力。通过添加参数化的运营商LDL，我们得到一个逻辑，能够表达所有的ω-正则性质，并包含参数化LTL和PROMPT-LTL LTL的参数化扩展。我们的主要技术贡献是翻译PLDL公式到不确定的Büchi自动机的指数大小通过交替自动机。这就产生了多项式空间算法的模型检验和假设保证模型检验和可实现算法的双指数运行时间。所有这三个问题也被证明是完整的这些复杂性类。此外，我们给出了严格的上限和下限的最佳参数值的模型检验和可实现性。利用这些界，我们提出了一个多项式空间过程的模型检验优化和一个算法的三次指数运行时间的可实现性优化。我们的研究结果表明，PLDL模型检验和可实现性并不比它们各自的（参数）LTL对应。
2015-12-07 cs.FL 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
LTL Fragments are Hard for Standard Parameterisations
我们分类的LTL可满足性和模型检验问题的几个标准参数化的复杂性。所考察的参数分别是时间深度、命题变量数和公式树宽，路径宽度我们发现，所有的运营商片段的LTL下的参数化是棘手的参数化的复杂性的意义上。
2015-09-22 cs.CC 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
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
Inquisitive Team Semantics of LTL
本文提出受探究逻辑启发的InqLTL团队语义，证明其带布尔否定时高度不可判定且表达力弱于带布尔否定的TeamLTL，同时找到一个可判定模型检验、可表达超性质的有意义片段。
2026-11-10 cs.FL 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
On-the-fly Unfolding with Optimal Exploration for Linear Temporal Logic Model Checking of Concurrent Software and Systems
针对并发系统LTL模型检测中的状态爆炸与即时展开难题，本文基于PDNet提出带延迟变迁探索树的最优即时展开算法，实现工具并在基准上优于SPIN与DiVine。
2024-06-12 cs.FL cs.LO
The Complexity of Flat Freeze LTL
本文研究单计数器自动机上平坦冻结LTL的模型检验问题，证明其NEXPTIME完全，并通过交替双向自动机模拟实现NP可达性算法，同时为参数定时自动机可达性提供新证明。
2019-10-15 cs.FL cs.LO
Synchronous Team Semantics for Temporal Logics
University of Tübingen（蒂宾根大学）；Institut für Theoretische Informatik, Leibniz Universität Hannover（汉诺威莱布尼茨大学理论计算机科学研究所）；School of Computing Science, University of Glasgow（格拉斯哥大学计算科学学院）；Department of Computer Science, Aalborg University（奥尔堡大学计算机系）
本文为LTL和CTL提出团队语义，使其能表达超性质，研究其计算复杂度并证明带有团队语义的LTL是HyperLTL的可行替代方案。
2026-10-06 cs.LO
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
Measuring Progress of Probabilistic LTL Model Checking
最近，Zhang和Van Breugel引入了概率模型检查器的进度度量的概念。给定线性时间属性P和已经检查过的系统部分的描述，进度度量返回单位间隔内的实数。实数捕获模型检查器在验证P方面取得了多少进展。如果进展为零，则没有取得任何进展。如果是，模型检查器就完成了。他们证明了进度度量为满足P的执行路径集合的度量提供了一个下界。他们还提出了一个算法来计算P是不变量时的进度度量。本文给出了当P是线性时序逻辑正片段公式时计算进度测度的一个算法。在这个片段中，我们可以表达不变量，也可以表达许多其他有趣的性质。该算法在P的大小上是指数的，而在已经检查过的系统部分的大小上是多项式的。我们还提出了一个算法来计算一个下限的进度措施在多项式时间。
2012-07-04 cs.LO cs.SE
PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude
分布式信息物理系统（DCPS）在航空和地面交通系统等领域非常普遍，包括分布式混合系统。DCPS的设计和验证是相当具有挑战性的，因为异步通信，网络延迟和时钟偏差。此外，它们的模型检验验证通常变得不可行，由于巨大的状态空间爆炸所造成的系统的并发性。PALS（“物理异步，逻辑同步”）的方法已被提出来减少DCPS的设计和验证，以设计和验证其底层同步版本的任务要简单得多。最初的PALS方法假设单个逻辑周期，但多速率PALS将其扩展以处理多速率DCPS，其中组件可以以不同的逻辑周期操作。本文展示了如何多速率PALS可以应用于正式验证一个非平凡的多速率DCPS。我们使用实时的【形】Maude正式指定一个多速率分布式混合动力系统由一个飞行员谁把飞机根据指定的角度通过分布式控制系统的飞机。我们的正式分析表明，原来的设计是无效的，在实现一个平稳的转弯机动，并导致重新设计的系统，满足所需的正确性。这表明，多速率PALS方法不仅是有效的正式DCPS验证，但也可以有效地用于DCPS的设计过程中，甚至在属性进行验证。
2013-01-01 cs.LO cs.SE
On complexity of propositional Linear-time Temporal Logic with finitely many variables
众所周知[DemriSchnoebelen 02]，命题线性时间时态逻辑LTL的可满足性和模型检查问题，在语言中只有一个命题变量，都是PSPACE完全的，这与LTL的这些问题的复杂性相一致，具有任意数量的命题变量[SislaClarke 85]。在本文中，我们表明，通过修改[SislaClarke 85]中LTL的空间硬度的原始证明，可以得到相同的结果;即，我们展示了如何修改来自[SislaClarke 85]的构造，以仅使用一个变量的公式来模拟多项式空间约束的图灵机的计算。我们相信，我们对[DemriSchnoebelen 02]结果的替代证明提供了对LTL的语义和计算特性的额外见解。
2018-11-25 cs.LO
Model Checking for Fragments of Halpern and Shoham's Interval Temporal Logic Based on Track Representatives
模型检验允许人们根据系统行为的形式模型（通常是Kripke结构）自动验证系统预期属性的规范。基于点的时态逻辑，如LTL、CTL和CTL*，描述了系统如何逐状态演化，通常用作规约语言。他们证明自己在各种应用领域相当成功。然而，属性约束的时间顺序的时间扩展的事件，以及涉及时间聚合，这是固有的间隔为基础的属性，不能正确地处理它们。区间时态逻辑（ITLs），以间隔作为其原始的时间实体，原来是非常适合的规范和验证的间隔计算属性（我们解释的所有轨道的Kripke结构作为计算间隔）。研究了Halpern和Shoham的时间区间模态逻辑（HS）的部分片段的模型检验问题。HS的特点是每对区间之间的每种可能的排序关系（所谓的艾伦关系）都有一种模态。首先，我们描述了一个EXPSPACE模型检验算法的HS片段的艾伦的关系满足，满足，开始，开始，和完成，它利用的可能性找到，为每个轨道（无限长），一个等效的有界长度的轨道代表。在检查属性时，它只需要考虑长度不超过给定界限的轨迹。我们证明了这样一个片段的模型检验问题是PSPACE困难的。最后，我们确定了其他表现良好的HS片段，这些片段的表达能力足以捕捉系统的有意义的区间特性，如互斥，状态可达性和非饥饿，其复杂性小于或等于LTL。
2017-09-06 cs.LO
