Computation Tree Logic for Synchronization Properties
我们提出了一个逻辑，扩展CTL（计算树逻辑）与运营商表示同步属性。如果一个属性在所有具有一定长度的路径中都成立，则该属性在系统中是同步的。新的逻辑是通过使用与CTL相同的路径量词和时态运算符来获得的，但允许量词的顺序不同。这个小的语法变化导致一个逻辑，可以表达非正规的属性，其中已知的扩展MSO路径长度相等是不可判定的。我们证明了我们的变体CTL是可判定的，模型检测问题是在Delta_3 ^P = P ^{NP ^NP}中，并且是DP-困难的。我们类似地考虑量词交换CTL的扩展，我们提出的运营商定义使用的基本运营商的CTL * 表示发生无限多个同步点。证明了模型检验问题仍然存在于Delta_3 ^P中，如果允许Next算子，则CTL和新逻辑的区分能力一致，从而可以在模型检验之前使用经典的互模拟商进行状态空间约简。
2016-05-24 cs.FL cs.LO
Experimental Study on CTL model checking using Machine Learning
Zhengzhou University（郑州大学）
目前流行的CTL模型检验工具所采用的核心方法都面临着著名的状态爆炸问题。在我们以前的研究中，提出了一种基于机器学习（ML）算法的方法来解决这个问题。然而，准确度并不令人满意。首先，我们在Graph Lab上进行综合实验，使用五种机器学习算法寻求最佳准确率。其次，在给定最优精度的情况下，求平均时间。结果表明，基于逻辑回归（LR）的方法模拟CTL模型检验的准确率为98.8%，平均效率是现有方法的459倍;基于提升树（BT）的方法模拟CTL模型检验的准确率为98.7%，平均效率是现有方法的639倍.
2019-02-23 cs.AI cs.LO
An Experiment on Parallel Model Checking of a CTL Fragment
我们提出了一个并行算法，本地，在飞，模型检验的CTL的片段，非常适合于现代，多核架构。这种模型检查算法得益于我们在以前的工作中描述的并行状态空间构造算法，并且共享相同的基本原则集：对可以分析的模型没有假设;对状态分布的方式没有限制;对处理器之间共享工作的方式没有限制。我们评估我们的算法的不同版本的性能，并将我们的结果与使用其他并行模型检验工具获得的结果进行比较。这项工作的最新贡献之一是研究CTL模型检查，不需要存储整个转换图，但操作上的反向生成树的空间效率的变体。
2013-01-31 cs.DC cs.LO
CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems (Technical Report)
Carl von Ossietzky University of Oldenburg（奥尔登堡卡尔·冯·奥西茨基大学）；DTU Compute（丹麦技术大学计算学院）
本文提出了一种基于上下文自由图文法的无限族有限状态标记转换系统CTL*模型检查方法，并通过实验验证了其有效性。
2026-01-22 cs.LO
Branching-time model checking of one-counter processes
单计数器进程（OCP）是下推进程，只对一元堆栈字母表进行操作。研究了基于OCP的模型检验计算树逻辑（CTL）的计算复杂性。一个PSPACE上界是继承自该问题的模态μ演算。首先，我们分析的周期性行为的CTL在OCP和推导出一个模型检验算法，其运行时间是指数的控制位置和语法概念的公式，我们称之为直到深度。因此，模型检验固定OCP对CTL公式与一个固定的深度，直到在P。这概括了第一作者，Mayr，和到CTL的片段EF的表达复杂性的结果。其次，我们证明了在一定的OCP上，CTL模型检验是PSPACE困难的。第三，我们表明，已经存在一个固定的CTL公式，模型检验的OCP是PSPACE困难的。对于后者，我们使用了复杂性理论的两个结果：（i）将中国余数表示中的自然数转换为二进制表示是在对数空间一致的NC ^1中;（ii）PSPACE是AC ^0-可串行化的。我们证明，我们的方法可以用来回答进一步的开放性问题。
2010-02-03 cs.CC cs.LO
CTL* model checking for data-aware dynamic systems with arithmetic
复杂动态系统的分析是形式化方法和人工智能的核心研究课题，系统与数据的组合建模在业务流程管理等应用中越来越重要。此外，流程挖掘技术现在被用来自动地从事件数据中挖掘流程模型，通常没有正确性保证。因此，需要验证技术的线性和分支时间属性，以确保所需的行为。在这里，我们考虑数据感知的动态系统与算术（DDSAs），这构成了一个简洁的，但表达形式主义的过渡系统与线性算术后卫。我们提出了一个CTL* 模型检验程序DDSAs依赖于一个有限状态的抽象，通过一组公式，捕捉变量配置。线性时间验证被证明是可判定的，在特定类别的DDSAs的约束语言或控制流被适当地限制。我们调查了几个这些限制的情况下，CTL*，积极和消极的结果：CTL* 验证被证明是可判定的单调性和整数周期性约束系统，但不可判定的反馈自由和有界回看系统。为了证明我们的方法的可行性，我们实现了它在基于SMT的原型ADA，显示出许多实际的业务流程模型可以有效地分析。
2022-05-18 cs.LO
New results on pushdown module checking with imperfect information
开放下推系统的模型检验标准分支时态逻辑（下推模块检查或PMC）最近在文献中被研究，在具有关于系统的完美和不完美信息的环境的上下文中（在最后一种情况下，环境仅具有系统的控制状态和栈内容的部分视图）。对于标准CTL，不完全信息下的PMC是不可判定的。如果堆栈内容被假设为可见的，那么问题是可判定的，并且是2EXPTIME完全的（将PMC的复杂性与CTL的完美信息相匹配）。限制在堆栈内容的深度可见的情况下，具有针对CTL的不完全信息的PMC的可判定性状态是开放的。在本文中，我们表明，与此限制，PMC与不完美的信息对CTL仍然不可判定。另一方面，我们个性化一个有趣的子类OPDS与可见的堆栈内容深度，使PMC与不完善的信息对CTL的存在片段是可判定的，并在2EXPTIME。此外，我们表明，PMC的程序复杂性与不完美的信息和可见的堆栈内容对CTL是2EXPTIME完全的（因此，指数比PMC的程序复杂性与完美的信息，这是已知的EXPTIME完全）。
2011-06-07 cs.LO
Temporal Logics with Language Parameters
计算树逻辑（CTL）及其扩展CTL* 和CTL+作为通用模型检验工具的基础广泛应用于自动验证。但是，虽然它们可以表达许多感兴趣的属性，如可达性，但即使是简单的常规属性，如“每隔一个索引标记为a”，也不能在这些逻辑中表达。虽然开发了许多扩展以包括常规或甚至非常规（例如可见下推）语言，但Axelsson等人给出了用于具有任意语言类的CTL的第一个通用框架Extended CTL。并应用于常规的，可见的下推和（确定性）上下文无关的语言。我们将这个框架扩展到CTL* 和CTL+，并分析它的可判定性，复杂性，表达性和可满足性。
2019-10-25 cs.FL cs.LO
Model Checking for a Class of Weighted Automata
在过去的十年中，已经提出了大量不同的模型检验方法。不同的方法适用于不同的模型类型，包括不定时，定时，概率和随机模型。本文提出了一种新的模型检验技术框架，其中包括一些已知的方法，但扩大了可将模型检验应用于一般加权自动机类的模型类别。该方法允许一个简单的适应模型检验的模型，尚未考虑为此目的。可以应用模型检验的那些新模型类型的例子是max/plus或min/plus自动机，它们是描述不同形式的动态系统和优化问题的良好建立的模型。在这种情况下，模型检验可用于验证系统的时间或定量属性。本文首先简要介绍了我们的类加权自动机，作为一个非常一般的模型类型。然后给出了值计算树逻辑（CTL）的$) is introduced as a natural extension of the well known branching time logic CTL. Afterwards, algorithms to check a weighted automaton according to a CTL$公式。最后，给出了加权自动机和CTL$的互模拟。
2003-04-15 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
Branching-time model checking of one-counter processes
单计数器进程（OCP）是下推进程，只对一元堆栈字母表进行操作。研究了基于OCP的模型检验计算树逻辑（CTL）的计算复杂性。一个PSPACE上界是继承自该问题的模态μ演算。首先，我们分析了OCP上CTL的周期性行为，并推导出一种模型检验算法，其运行时间仅在控制位置数量方面呈指数级，以及我们称之为向左直到深度的公式的语法概念。因此，模型检验固定OCP对CTL公式与一个固定的深度，直到在P。这概括了第一作者，Mayr，和到CTL的片段EF的表达复杂性的结果。其次，我们证明了在一定的OCP上，CTL模型检验是PSPACE困难的。第三，我们表明，已经存在一个固定的CTL公式，模型检验的OCP是PSPACE困难的。为了得到后一个结果，我们使用了复杂性理论中的两个结果：（i）将中国余数表示中的自然数转换为二进制表示是在对数空间一致的NC ^1中;（ii）PSPACE是AC ^0-可串行化的。我们证明，我们的方法可以用来获得进一步的结果。我们证明了在OCP上对CTL的片段EF进行模型检验对于P^NP是困难的，从而建立了一个匹配的下界，并回答了第一作者Mayr和To的一个公开问题。我们还证明了以下问题对于PSPACE是困难的：给定一个计数器马尔可夫决策过程，一组计数器值为零的目标状态和一个初始状态，以决定初始状态最终到达目标状态之一的概率是否任意接近1。这提高了以前已知的下界的每一个层次的布尔Bra…
2009-09-06 cs.CC cs.LO
Abstract Family-based Model Checking using Modal Featured Transition Systems: Preservation of CTL* (Extended Version)
变量系统允许通过使用特征（配置选项）标记变量功能来有效地构建许多自定义变量。在许多应用中，其质量保证和形式化验证至关重要。基于族的模型检验通过利用变量之间的共性，允许在单次运行中同时验证变分系统的所有变量。然而，它的计算成本仍然在很大程度上取决于变体的数量（通常是巨大的）。在这项工作中，我们将展示如何实现有效的基于家庭的模型检验的CTL* 的时间属性，使用可变性抽象和现成的（单系统）工具。我们使用变异抽象派生抽象的基于族的模型检验，其中的变异模型的变分系统被替换为一个抽象的（更小的）版本，称为模态特征的过渡系统，它保留了普遍的和存在的时间属性的满意度，在CTL* 表示。模态特征变迁系统包含两类变迁，分别称为may变迁和must变迁，它们分别由保守（过近似）抽象和它们的对偶（欠近似）抽象定义。可变性抽象可以与变量集合的不同划分相结合，以推断用于变分系统的合适的分而治之验证计划。我们说明了几个变分系统的这种方法的实用性。
2018-03-05 cs.LO cs.PL cs.SE
Enriched MU-Calculi Module Checking
开放系统的模型检验问题已经在文献中得到了深入的研究，对于有限状态（模块检验）和无限状态（下推模块检验）系统，关于Ctl和Ctl*。在本文中，我们进一步研究了这个问题的μ演算丰富的名义和分次模态（混合分次μ演算），在有限状态和无限状态设置。使用自动机理论方法，我们证明了混合分级μ-演算模块检验在指数时间内是可解的，而混合分级μ-演算下推模块检验在双指数时间内是可解的.这些结果也是紧密的，因为它们匹配Ctl的已知下限。我们还研究了关于混合分级μ-演算的模块检查问题，通过展示多米诺问题的简化，我们展示了它的不可判定性。最后，我们简要概述了完全丰富的Mu演算的模型检验问题，以及通过删除至少一个额外的构造而获得的片段。
2008-07-29 cs.LO
Distributed CTL Model Checking in the Cloud
最近广泛使用的“大数据”平台要求形式化验证社区更广泛地采用。事实上，形式化验证需要高性能的数据处理软件，用于从来自被分析系统的空前数量的数据中提取知识。由于基于云的计算资源已经变得易于访问，因此验证技术和工具有机会经历深刻的技术转型，以利用新的可用架构。这使得人们对并行化和分布式验证技术越来越感兴趣。在本文中，我们介绍了一种分布式的方法，利用通常使用的技术，由“大数据”社区，使验证的计算树逻辑（CTL）公式非常大的状态空间，使用分布式系统和云计算设施。基准规范上进行的几个测试的结果，从而显示所提出的方法的方便。
2013-10-24 cs.DC cs.LO cs.SE
A Team Based Variant of CTL
我们介绍了两个变种的计算树逻辑CTL的基础上的团队语义：一个异步的和同步的。对于这两个变种，我们调查的计算复杂性的可满足性以及模型检验问题。可满足性问题被证明是EXPTIME-完全的。在这里，考虑两种语义中的哪一种并不重要。对于模型检验，我们证明了同步情况下的PSPACE-完全性，异步情况下的P-完全性。此外，我们证明了这两种语义的几个有趣的基本属性。
2015-07-14 cs.CC cs.LO
Cycle Detection in Computation Tree Logic
时态逻辑是一种非常强大的形式主义，在形式系统的设计和验证中得到了深入的研究和应用。它的应用通常简化为解决特定的决策问题，如模型检验和可满足性。在这类问题中，解决方案通常需要在循环中检测一些特定的属性。例如，当使用基于自动机、博弈论、SCC分解等的经典技术时，就会发生这种情况。令人惊讶的是，迄今为止，还没有一个时态逻辑被认为具有讨论循环的明确能力。在本文中，我们介绍周期-CTL *，经典的分支时间时序逻辑CTL* 的扩展，随着周期量化，以便在周期上的谓词。这个逻辑非常有表现力。事实上，我们证明，它严格扩展CTL*，是正交的μ演算。我们还提供了一些涉及非正则性质的例子，证明了它的有用性。我们研究了Cycle-CTL* 的模型检验问题，并证明了它和CTL* 一样是PSPACE完备的.我们还研究了逻辑的存在循环片段的可满足性问题，并证明了它在2 ExpTime中是可解的。这一结果利用了自动机理论的方法，以及新的ad-hoc定义的互模拟和树状展开。
2016-09-14 cs.FL cs.LO
A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking
概率计算树逻辑（PCTL）和连续随机逻辑（CSL）通常分别用于描述离散时间和连续时间的概率属性规范。在PCTL和CSL中，执行满足某些时态性质的可能性可以通过其基本计算树逻辑（CTL）中路径量词的概率扩展来定量表示，但它们的路径公式在CTL中是通过相同的运算符来表示的。由于这个原因，它们都不能表示具有定量时间属性的公式，例如“某些属性在路径上超过80%的时间点（在某个有界区间内）保持不变”的形式。本文引入了一个新的时态算子来表达事件频率的概念，并在CTL \star的基础上定义了概率频率时态逻辑（PFTL）。因此，我们可以很容易地表示概率系统中的行为的时间属性。然而，它是很难开发一个完整的PFTL模型检查，由于丰富的表现力。相应地，我们开发了一个模型检测算法的CTL类片段的PFTL对有限状态马尔可夫链，和一个近似的模型检测算法的有界线性时序逻辑（LTL）类片段的PFTL对可数状态马尔可夫链。
2011-11-14 cs.LO
Parameterized Model Checking of Token-Passing Systems
我们重新访问的参数化模型检验问题的令牌传递系统和规格的索引$\textsf{CTL}^\ast \backslash \textsf{X}$。Emerson和Namjoshi（1995，2003）已经表明，单向令牌环中索引$\textsf{CTL}^\ast \backslash \textsf{X}$的参数化模型检验可以简化为检查高达某个\emph{cutoff}大小的环。Clarke et al.（2004）对于一般拓扑和索引$\textsf{LTL} \backslash \textsf{X}$给出了类似的结果，前提是进程不能选择发送或接收令牌的方向。我们统一和大大扩展这些结果，系统地探索片段的索引$\textsf{CTL}^\ast \backslash \textsf{X}$一般拓扑结构。对于每个片段，我们确定是否存在一个截止点，对于一些具体的拓扑结构，如环，集团和星，我们推断小截止点。最后，我们表明，问题变得不可判定，因此没有截止存在，如果进程被允许选择的方向，他们发送或从他们收到的令牌。
2013-11-25 cs.LO
QCTL model-checking with QBF solvers
量化CTL（QCTL）是对时态逻辑CTL的扩展，在原子命题上引入了量化。这个扩展被认为是非常有表现力的：QCTL允许我们在Kripke结构上表达复杂的属性（它和MSO一样有表现力）。量化存在几种语义：这里，我们使用结构语义，其中额外的命题标记Kripke结构（而不是其执行树），并且模型检验问题在这个框架中已知是PSPACE完备的。提出了一种基于QBF约简的QCTL模型检验算法。我们考虑几个减少策略，我们比较它们与原型（基于几个QBF求解器）在不同的例子。
2020-10-06 cs.LO
SAT-Based ATL Satisfiability Checking
模型与策略的综合是软件工程中一个非常重要的问题。这里的主要内容是检查表达要实现的系统规范的公式的可满足性。提出了一种新的判定交替时序逻辑（ATL）公式可满足性的方法。该方法扩展了CTL利用SAT模单调理论求解器的方法。类似于CTL的情况下，我们的方法似乎是非常有效的。实验结果表明，我们可以快速测试的大型ATL公式，已经达到了现有的方法。
2020-02-08 cs.LO cs.MA
Counting CTL
本文提出了一系列的定量扩展的时序逻辑CTL。我们增强了时间模态的能力，以约束满足某些子公式沿路径的状态的数量。通过选择约束中允许的布尔运算和算术运算的组合，可以得到几个不同的推广CTL的逻辑。我们提供了一个彻底的分析，他们的表现力和简洁性，以及他们的模型检查和可满足性问题的复杂性（范围从P-完全不可判定）。最后，我们提出了两种具有相似特征的替代逻辑，并对这两种变体的性质进行了比较研究。
2013-02-15 cs.LO
Learning Branching-Time Properties in CTL and ATL via Constraint Solving
本文研究从Kripke结构和并发博弈结构样本中学习CTL与ATL公式的问题，通过将学习问题编码为可满足性问题并结合不动点模型检测算法进行符号化求解，并在Python原型中验证了方法的有效性。
2024-06-28 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
Rich Counter-Examples for Temporal-Epistemic Logic Model Checking
模型检验验证系统的模型是否满足给定的属性，否则会产生一个反例来解释违规。验证的性质正式表示在时间逻辑。一些时态逻辑，如CTL，是分支的：它们允许表达关于模型的整个计算树的事实，而不是每个线性计算。当处理多模态逻辑时，这个分支方面甚至更加关键，即用几个转移关系表达系统事实的逻辑。一个突出的例子是CTLK，一个逻辑，原因的时间和认知属性的多智能体系统。一般来说，模型检查器为失败的属性生成线性反例，由模型的单个计算路径组成。但是一些分支性质只能通过一个线性反例来很好地和部分地解释。本文提出了更丰富的反例结构，称为树型注释反例（TLACE），属性的限制性CTL（ARCTL），CTL量化路径的扩展限制在动作标记的模型过渡。这些反例有一个分支结构，支持更完整地描述违反属性。这些反例的元素都注释了部分属性，以便更好地理解它们的结构。这些更丰富的反例的可视化和浏览成为一个关键问题，因为对于深度嵌套的属性，分支和状态的数量可以呈指数级增长。本文形式化地定义了TLACE的结构，刻画了TLACE的充分反例。模型和失效属性，并给出了ARCTL属性的生成算法。它还用CTLK中的例子说明了这种方法，使用CTLK到ARCTL的简化。所提出的方法已经实施，首先通过扩展NuSMV模型检查器来生成和导出分支反例，其次通过提供交互式图形界面来可视化和浏览它们。
2012-02-21 cs.LO cs.MA
Branching Bisimulation Learning
提出一种针对非确定性系统的分支互模拟学习算法，通过决策树和SMT求解生成有限商，实现CTL*模型检测，在大型或无限状态空间上优于现有技术。
2025-05-22 cs.LO
Symbolic Model Checking using Intervals of Vectors
Computer Science Department Faculty of Science University of Geneva（日内瓦大学理学院计算机科学系）
本文提出了一种基于向量区间的新方法，用于高效进行Petri网的CTL模型检查，通过同态操作和标准形式提升性能。
2026-09-16 cs.LO
Changing Observations in Epistemic Temporal Logic
ENS Rennes（雷恩高等师范学院）；University of Naples “Federico II”（那不勒斯费德里科二世大学）
我们研究了知识和时间逻辑中主体观察力的动态变化。我们认为CTL*K，扩展CTL* 与知识运营商，并丰富它与一个新的运营商，模拟一个代理的方式观察系统的变化。我们扩展了经典的语义知识的完美召回代理占观察的变化，我们表明，这个新的运营商严格增加了CTL*K的表达能力。我们减少模型检查问题，我们的逻辑CTL*K，这是已知的可判定的。这为我们的逻辑提供了模型检查问题的解决方案，但其复杂性不是最佳的。事实上，我们提供了一个更好的复杂性直接决策过程。
2018-09-03 cs.AI cs.LO cs.MA
Inferring Properties in Computation Tree Logic
针对分支时间逻辑规范推断研究不足的问题，提出一种基于反例引导的算法，通过生成不可取模型从有限状态模型中推断出简洁且语言极小的CTL公式，并首次开发了基于SAT编码的被动学习算法。
2023-10-20 cs.FL cs.LO
Reducing Validity in Epistemic ATL to Validity in Epistemic CTL
Institute of Mathematics；Informatics Bulgarian Academy of Sciences Sofia, Bulgaria
我们提出了一个有效性保持翻译的一个子集的认知交替时间时序逻辑（ATL）的认知计算树逻辑（CTL）。已知所考虑的认知ATL子集具有有限模型性质和可判定的模型检验。这需要有效性的可判定性，但隐含的算法是不可行的。将有效性问题减少到相应的CTL系统中，使得该逻辑的自动演绎技术可用于处理明显更复杂的ATL系统。
2013-03-04 cs.AI cs.LO cs.MA
Quantified CTL with imperfect information
量化CTL（QCTL）是一个研究得很好的时态逻辑，它扩展了原子命题上的量化CTL。最近，它已经成为一个强大的中介框架，研究逻辑的战略推理。我们将其扩展到包括不完美的信息，通过参数化量化器来定义它们观察模型的程度，从而约束它们的行为。我们考虑两种不同的语义，一个与没有记忆的概念有关，另一个与完美回忆有关。我们研究了我们的逻辑的表达性，并表明，它符合MSO的第一语义和MSO具有同等水平的第二个。我们建立的模型检查问题是Pspace完全的第一语义。虽然它是不可判定的第二个，我们确定了一个语法片段，定义的概念，分层公式，我们证明是可判定的自动机理论的方法。
2018-09-03 cs.LO
Temporal Logics for Hyperproperties
提出了两种新的超性质验证逻辑。超属性将安全策略（如不干涉）表征为计算路径集的属性。标准的时态逻辑，如LTL、CTL和CTL*，一次只能引用一条路径，因此不能表达许多感兴趣的超性质。这里提出的逻辑，HyperLTL和HyperCTL*，在多个路径上向LTL和CTL* 添加显式和同时量化。这种量化使得能够表达超性质。给出了该逻辑的模型检验算法。针对HyperLTL的一个片段，实现了一个原型模型检测器。
2014-01-21 cs.LO
Model checking: the interval way
[...]最著名的模型检验（MC）技术是从80年代后期发展起来的，记住著名的“基于点”的时序逻辑LTL和CTL。然而，虽然这种逻辑的表达能力是毋庸置疑的，但我们可能希望检查系统模型的一些属性，这些属性本质上是“基于区间的”，因此不能用基于点的时间逻辑来表达，例如，“命题P必须在给定计算扇区中至少保持平均数量的系统状态”。在这里，时间间隔逻辑（ITLs）开始发挥作用，为时间推理提供了另一种设置。这样的逻辑处理间隔，而不是点，作为它们的原始实体：这一特征使它们能够表达时间属性，例如持续时间的动作，成就和时间聚合，这在标准的基于点的逻辑中无法处理。Halpern和Shoham的时间间隔模态逻辑（HS）是最著名的ITL之一：除了相等之外，它为间隔对之间的13种可能的排序关系中的每一种提供了一种模态。在这篇论文中，我们的注意力集中在基于HS的MC，在属性规约语言的角色，这是一个小的工作已经做了比较MC基于点的时态逻辑。我们研究了这种问题的复杂性，考虑不同的系统模型，我们也比较了HS的表达能力，在MC的LTL，CTL和CTL*。[...]
2019-02-11 cs.CC cs.LO
An Algebraic Method to Fidelity-based Model Checking over Quantum Markov Chains
本文提出QCTL逻辑在量子马尔可夫链上进行基于保真度的模型检测，通过归约到实数存在理论的量词消去实现精确计算，证明QCTL公式指数时间可判定，并以量子IPv4协议验证有效性。
2021-01-13 cs.LO
Compositional Reasoning for Interval Markov Decision Processes
Puggelli等人最近研究了具有凸不确定性的Markov决策过程的模型检验概率CTL性质，这类模型检验算法通常存在状态空间爆炸问题.在本文中，我们解决概率互模拟，以减少这样的MDP的大小，同时保持概率CTL属性，它满足。特别是，我们讨论的关键成分，建立在运行时组成间隔MDP组件的并行组合操作。更确切地说，我们研究如何并行组合操作的区间MDP可以定义，以便达到一个同余闭包。其结果是，我们表明，概率互模拟区间MDPs是一致的两个方面的并行性，即同步产品和交织。
2016-07-28 cs.LO
A Constructive Equivalence between Computation Tree Logic and Failure Trace Testing
形式化验证的两个主要系统是模型检验和基于代数模型的测试。模型检验基于某种形式的时态逻辑，例如线性时态逻辑（LTL）或计算树逻辑（CTL）。CTL是一种强大而现实的逻辑，它能够表达进程的最有趣的属性，如活性和安全性。基于模型的测试基于进程的某些操作语义（例如跟踪、故障或两者）及其关联的前序。除了互模拟之外，最细粒度的前序（主要是理论上的重要性）是基于故障跟踪的。我们表明，这两个最强大的变种是等价的，也就是说，我们表明，对于任何故障跟踪测试存在一个CTL公式相当于它，反之亦然。我们所有的证明都是构造性的和算法性的。我们的结果允许一个大系统的部分被指定为逻辑，而其他部分被指定为代数，从而结合了最好的两个（逻辑和代数）的世界。
2019-01-30 cs.LO
Extended Computation Tree Logic
我们介绍了一个通用的扩展流行的分支时间逻辑CTL细化的时间，直到和释放操作符与形式语言。例如，语言可以确定沿着路径的时刻，直到属性可以被满足。我们考虑几类语言导致逻辑具有不同的表达能力和复杂性，其重要性是出于他们的使用模型检验，合成，抽象解释等，我们表明，即使上下文无关的语言，直到操作逻辑仍然允许多项式时间模型检查，尽管显着增加的表达能力。这使得该逻辑在验证中的应用成为一个有希望的候选者。此外，我们分析了可满足性的复杂性，并比较了这些逻辑的表达能力CTL* 和PDL的扩展。
2010-06-18 cs.LO
Robust Computation Tree Logic
针对分支时间逻辑缺乏鲁棒语义的问题，提出采用多值语义的 rCTL 与 rCTL*，在保持或增强表达能力的同时，使模型检测、可满足性和综合复杂度不增加。
2023-10-24 cs.LO
Propositional Dynamic Logic for Hyperproperties
反应式系统的信息安全属性（如非干扰性）通常需要将系统的不同执行相互关联并同时遵循它们。这样的超性质在其他上下文中也可以是有用的，例如，当分析分布式系统的属性时，如线性化。由于LTL、CTL或模态μ演算等常见逻辑无法表达超性质，因此开发了超逻辑HyperLTL和HyperCTL* 来解决这个缺陷。然而，这些逻辑不能表达任意的Ω-正则性质。在本文中，我们介绍HyperPDL-三角洲，一个适应的命题动态逻辑的Fischer和Ladner的hyperproperties，为了消除这一限制。使用一个优雅的自动机理论框架，我们表明，HyperPDL-三角洲模型检验是渐近不更昂贵的HyperCTL* 模型检验，尽管它大大增加了表达能力。我们进一步研究片段的HyperPDL-三角洲方面的可满足性检查。
2020-07-17 cs.FL 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
Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems
资源受限的多智能体系统的验证一般是不可判定的。在许多这样的设置中，资源对于代理是私有的。本文研究了基于交替时序逻辑（ATL）的资源逻辑在共享资源下的模型检验问题。资源可以被消耗和生产到任何数量。我们表明，模型检验问题是不可判定的，如果两个或两个以上的这样的无界资源。我们的主要技术成果是，在一个单一的共享资源的情况下，问题变得可判定。虽然直观，可判定性的证明是不平凡的。我们减少模型检验的问题交替Büchi下推系统。一个中间结果连接到一般的基于自动机的验证：我们表明，模型检验计算树逻辑（CTL）（紧凑）交替Büchi下推系统是可判定的。
2015-08-14 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 and model synthesisfrom partial models: a logic-based perspective
我考虑以下一般情况：一个抽象的模型M的一些“真正的”系统只是部分介绍，或部分已知的，我们必须确保实际的系统满足给定的规范，形式化的一些逻辑语言。这种情况至少有两个本质上不同的解释，导致两个本质上不同的形式逻辑和算法问题：“部分模型的模型合成”，其中M到完整模型的一些“可接受”扩展必须满足规范，和“部分模型的模型检验”，其中M到完整模型的所有“可接受”扩展必须满足规范。这些问题自然地扩展了经典的可满足性、有效性和模型检验的逻辑决策问题。在这里，我简要地讨论这两个问题的背景下，经典，模态和时间逻辑。我做了一些观察，状态一些开放的问题，并概述了一个一般的表格式的程序，解决了几个著名的模态和时序逻辑，包括有限的部分模型的无约束模型合成的问题。K、LTL、CTL、ATL。
2020-12-22 cs.LO
Reasoning about Games via a First-order Modal Model Checking Approach
在这项工作中，我们提出了一个逻辑的基础上，一阶CTL，即游戏分析逻辑（GAL），以原因的游戏。我们将博弈论的模型和解的概念分别作为GAL的模型和公式。准确地说，我们将具有完美信息的广泛博弈表示为GAL模型，并通过GAL公式将纳什均衡和子博弈完美均衡表示出来。从实用的角度来看，我们提供了一个GAL模型检查器，以自动分析游戏。我们至少在两个方向上使用我们的模型检查器：找到博弈论的解决方案概念;以及分析基于AI社区标准算法的玩家，例如极大极小过程。
2014-04-14 cs.LO
A Complete Mental Temporal Logic for Intelligent Agents
该研究提出融合心智模态的时态逻辑 BPICTL，建立可靠完备推理系统、证明有限模型性质并给出模型检测算法。
2026-10-30 cs.LO
Model Checking One-clock Priced Timed Automata
我们考虑定价模型（a.k.a.加权）时间自动机，它是时间自动机的扩展，具有位置和转换的成本信息，我们基于对模态具有成本约束的经典时态逻辑的扩展来研究该模型的各种模型检查问题。我们证明，在假设模型只有一个时钟，模型检查这类模型对逻辑WCTL，CTL成本约束的方式，是PSPACE完全的（虽然它已被证明是不可判定的，只要模型有三个时钟）。我们还证明了模型检查WMTL，具有成本约束模态的LTL，只有当模型中有一个时钟和一个秒表成本变量（即，其斜率位于{0，1}中）。
2008-06-20 cs.CC cs.GT cs.LO
Checking Temporal Properties of Presburger Counter Systems using Reachability Analysis
计数器系统是一个众所周知的和强大的建模符号，用于指定无限状态系统。在本文中，我们的目标是检查计数器系统的时间性质的问题。我们首先专注于检查活性的属性，并提出了两个半决策技术，这些属性。这两种技术都返回一个公式，该公式对满足给定活性属性的给定系统的可达状态集进行编码。我们的技术的一个新颖的方面是，他们使用的可达性分析技术，这是很好的研究，在文献中，作为黑盒，因此能够计算精确的答案，更广泛的一类系统比以前的方法相同的问题。其次，他们计算他们的结果，迭代膨胀或收缩，因此允许一个近似的解决方案，以获得在任何一点。我们的技术状态的正式属性，并提供使用标准基准的实验结果，以显示我们的方法的实用性。最后，我们提供了一种技术，检查任意CTL的时间属性，它使用上述的活性属性检查技术作为黑盒。
2017-12-15 cs.LO
TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets
本文提出了一种针对Petri网的HyperLTL模型检查器，用于验证超属性，该工具集成于TAPAAL框架并展示了其在计算机网络领域的应用性能。
2026-01-09 cs.LO
L2C2: Logic-based LSC Consistency Checking
实时序列图（LSC）已被提出作为一个基于对象间的规范和反应式系统的可视化程序设计语言。在本文中，我们引入了一个基于逻辑的框架来检查LSC规范的一致性。一个LSC模拟器已经在逻辑编程中实现，利用记忆化的深度优先搜索策略，以显示LSC中的反应系统将如何响应一组外部事件序列。定义了一个正式的符号来指定外部事件序列，用并行运算符和测试控件扩展了正则表达式。并行运算符允许在LSC中同时测试交织的并行外部事件;而测试控件为用户提供了一种新的方法来指定和测试某些时间属性（例如，CTL公式）。我们的框架还提供了一个状态转换图或故障跟踪证明一致性检查结果。
2010-02-16 cs.LO
Extended Graded Modalities in Strategy Logic
Technische Universitat Wien（维也纳工业大学）；Università degli Studi di Napoli Federico II（那不勒斯费德里科二世大学）
策略逻辑（SL）是多智能体系统中策略推理的逻辑形式。它的主要特点是，它具有与特定代理相关联的策略变量，这些变量具有绑定运算符。我们引入了分级策略逻辑（GradedSL），这是SL在策略变量元组上的分级量词的扩展，即，“存在至少g个不同的元组（x_1，...，其中g是集合N的并集{aleph_0，aleph_1，2 ^aleph_0}中的基数。我们证明了GradedSL的模型检测问题是可判定的。然后，我们转向GradedSL片段的复杂性。当g被限制为有限基数时，写为GradedNSL，模型检查的复杂性并不比SL更难，即，它在量词等级中是非初等的。我们说明了我们的形式主义，显示如何计算的数量不同的策略配置文件是纳什均衡（NE），或子博弈完美均衡（SPE）。通过对具体公式结构的分析，我们得出结论：检验唯一NE或SPE存在性的重要问题都可以在2 ExpTime中解决，这并不比仅仅检验此类平衡点的存在性困难。
2016-07-12 cs.AI cs.GT cs.LO
Strategic (Timed) Computation Tree Logic
本文定义了带战略算子的 CTL 和 TCTL 扩展（SCTL 和 STCTL），证明其表达力优于 ATL，并分析了不同信息与回忆语义下的模型检测复杂度，最终利用 IMITATOR 工具支持 STCTL[ir] 的实际应用。
2023-10-19 cs.LO cs.MA
Strategies, model checking and branching-time properties in Maude
本文扩展Maude模型检验能力，使其支持策略控制系统上的CTL*和μ-演算分支时间性质验证，并通过通用高效连接集成外部模型检验器并比较其性能。
2024-01-15 cs.LO
Reactive Synthesis: Branching Logics and Parameterized Systems
反应合成是一种自动的方法，可以将人类在某种逻辑中表达的意图转化为某种系统。本文分为逻辑和系统两部分。在第一部分中，我们开发了两种新的CTL* 合成方法。第一种方法由两个扩展的SMT为基础的有界综合：一个遵循自底向上的CTL* 模型检验，另一个遵循自动机框架。第二种方法将CTL* 合成减少为LTL合成。这种减少将任何LTL合成器变成CTL* 合成器。这两种方法已经实施，并可在网上查阅。在第二部分中，我们研究了两个系统架构的参数化综合。第一种体系结构是受缓存一致性协议启发的保护系统。在防护系统中，进程转换的启用或禁用取决于某些局部状态中是否存在其他进程。已有的关于保护协议的截断结果仅限于封闭系统，并且对于活性性质的应用有限。我们关闭这些差距，并证明了严格的截止与活性的开放系统，也截止检测死锁。第二种架构是令牌环系统，其中单个令牌循环布置在环中的进程。现有的参数化综合方法的实验表明，它不能扩展到大规格。首先，我们优化的方法，细化截止约简，使用模块化和抽象。评估显示了几个数量级的加速。其次，对工业仲裁协议AMBA进行了参数化综合案例研究。我们描述了新的技巧-一个新的截止扩展和分解合成-，再加上前面描述的优化，使我们能够合成AMBA在一个参数化的设置，第一次。
2018-08-28 cs.LO
Modelling and Verification of Multiple UAV Mission Using SMV
Cranfield University（克兰菲尔德大学）
模型检验可以用来验证数字电路、安全协议、通信协议的正确性，因为它们可以用有限状态转移模型来建模。然而，在Kripke模型中模拟无人机等混合系统的行为是具有挑战性的。这项工作的目的是捕捉到一个Kripke模型的无人机执行合作搜索任务的行为，从而验证它对时间属性表示的计算树逻辑（CTL）。SMV模型检验器用于模型检验。
2010-03-01 cs.LO cs.MA cs.RO
Qualitative Logics and Equivalences for Probabilistic Systems
我们调查的逻辑和等价关系，捕捉定性行为的马尔可夫决策过程（MDP）。我们提出了定性随机CTL（QRCTL）：这种逻辑公式可以表达这样一个事实，即某些时间属性持有所有路径，或概率为0或1，但它们不区分中间概率值。我们提出了一个符号的，多项式时间模型检测算法的QRCTL MDP。逻辑QRCTL在MDP的状态上导出了一个等价关系，我们称之为定性等价：非正式地说，如果两个状态下概率为0或1的公式集相同，则两个状态是定性等价的。我们表明，对于有限的交替MDP，其中不确定性和概率的选择发生在不同的状态，定性等价与交替互模拟相吻合，因此可以通过有效的分区细化算法计算。另一方面，在非交替MDP中，等价关系不能通过划分细化算法来计算，而是需要非局部计算。最后，我们考虑QRCTL*，它以与CTL* 扩展CTL相同的方式用嵌套的时态运算符扩展QRCTL。我们表明，QRCTL和QRCTL* 诱导交替MDP相同的定性等价，而在非交替MDP，从QRCTL* 产生的等价可以严格更精细。我们还提供了一个完整的定性等价，互模拟，交替互模拟之间的关系的表征，根据是否MDP是有限的，以及他们的过渡关系是否是有限分支。
2009-05-04 cs.LO
