Temporal logic with predicate abstraction
考虑了一个没有量词但具有谓词抽象机制和等式的谓词线性时态逻辑LTL_{λ,=}。LTL_{λ,=}的模型可以很自然地看作是在某些（可能是无限的）域的元素上移动的卵石（柔性常数）系统。这允许使用LTL_{λ,=}的规范的动态系统使用一些资源，如使用内存位置，移动代理占用一些网站等的进程。另一方面，我们表明，LTL_{λ,=}是不是递归axiomatizable，因此，LTL_{λ,=}规范的全自动验证是不，一般来说，可能的。
2004-10-27 cs.CL cs.LO
The Complexity of Flat Freeze LTL
本文研究单计数器自动机上平坦冻结LTL的模型检验问题，证明其NEXPTIME完全，并通过交替双向自动机模拟实现NP可达性算法，同时为参数定时自动机可达性提供新证明。
2019-10-15 cs.FL cs.LO
A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)
本研究提出将线性时序逻辑模理论LTL-MT规约为符号数据字自动机SDWAs的新方法，可转化为约束霍恩子句求解，适用于模型检测等场景，实验表现不逊于现有定制方案。
2024-08-16 cs.LO
A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Buchi Register Automata
本文将析取 μ↓-演算从有限字重新定义到无限字，并证明其与 Büchi 寄存器自动机表达能力等价。
2024-06-17 cs.FL 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
A Linear Temporal Logic of Frequencies on Series of Events
Universität Tübingen（蒂宾根大学）；University School for Advanced Studies IUSS Pavia（帕维亚高等研究学院）；University of Milan（米兰大学）
本文提出LTLF，一种通过引入测度敏感算子表达事件序列频率属性的时序逻辑，用于形式化监控和控制系统（如机器学习分类器）。
2026-11-03 cs.LO math.LO
Model Checking Flat Freeze LTL on One-Counter Automata
本文解决了单计数器自动机上平坦冻结线性时序逻辑模型检测的可判定性开放问题，通过归约到带参数化相等性测试的可达性问题并转化为Presburger算术证明其可判定。
2018-12-06 cs.FL cs.LO
Model checking memoryful linear-time logics over one-counter automata
我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。
2010-01-18 cs.LO
Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers
度量时态逻辑（MTL）和时间命题时态逻辑（TPTL）是线性时态逻辑（LTL）的重要实时扩展。在一般情况下，这些扩展的可满足性检查问题是不可判定的，当未来的U和过去的S模态使用。在一个经典的结果中，证明了MTL [U，S]的非准时片段MITL[U，S]的可满足性检验是可判定的，具有EXPSPACE完全复杂性。鉴于这种非准时性的概念在TPTL[U，S]的情况下不能恢复可判定性，我们提出了TPTL[U，S]的非准时性的一个推广，称为\emph{non adjacency}，并专注于它的1-变量片段1-TPTL[U，S].虽然非相邻的1-TPTL[U，S]似乎是一个非常小的片段，但它比MITL更严格地表达。作为我们的主要结果，我们证明了非相邻1-TPTL[U，S]的可满足性检验问题是可判定的，具有EXPSPACE完全复杂性。
2021-09-05 cs.LO
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
我们研究了一个扩展了模块和分数时钟约束的时间下推自动机的表达模型。我们表明，二进制可达性关系是有效的混合线性算术与合理的整数排序表示。这包含了类似的可表达性结果，以前已知的有限和下推定时自动机与不定时堆栈。作为关键的技术工具，我们使用量词消去的混合线性算术的一个片段和循环顺序原子，并减少注册下推自动机循环顺序原子。
2018-04-28 cs.FL cs.LO
Logics for Context-free Hyperproperties
Technische Universität Ilmenau（伊尔梅瑙工业大学）；Université Paris Cité, CNRS, IRIF（巴黎西岱大学，法国国家科学研究中心，信息研究与研究所）；Aalborg University（奥尔堡大学）
提出一种用于指定上下文无关超性质的逻辑，通过迹量化扩展可视下推自动机，并证明单量词交替下的模型检测可判定性及不可判定性边界。
2026-10-04 cs.FL cs.LO
Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words
University of Warwick（华威大学）
本文提出带作用域的MSO逻辑和数据正则表达式，证明其与NRA在数据域上的等价性，为寄存器自动机提供新的理论基础。
2026-02-13 cs.LO
Automata-Based Software Model Checking of Hyperproperties
我们开发了时态流逻辑（TSL）和超时态流逻辑（HyperTSL）模理论的模型检验算法。TSL扩展了线性时序逻辑（LTL）的存储单元，功能和谓词，使其成为一个方便的和表达的逻辑推理软件和其他系统的无限数据域。HyperTSL进一步将TSL扩展到hyperproperties的规范-与多个系统执行相关的属性。因此，HyperTSL可以在软件系统中表达信息流策略，如不干涉。我们用理论扩充了HyperTSL，得到了HyperTSL（T），并建立在LTL软件验证的方法上，得到了TSL和HyperTSL（T）的模型检验算法。这导致了一个合理但不一定完整的算法，用于HyperTSL（T）的forall*exists* 片段中包含的规范。我们的方法构成了第一个软件模型检验算法的时间hyperproperties与量词交替，不依赖于有限状态的抽象。
2023-03-26 cs.FL cs.LO
Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
研究了具有团队语义的模型检验线性时态逻辑（TeamLTL）的表达性和复杂性。TeamLTL，尽管是一个纯粹的模态逻辑，但能够定义超属性，即，与多个执行跟踪相关的属性。TeamLTL最近才被引入，关于它的表达能力和模型检验问题，只有很少的结果是已知的。我们将TeamLTL的表达性与通过用迹和命题量词（HyperLTL和HyperQPTL）扩展LTL获得的超性质的逻辑联系起来。通过这样做，我们得到了一些模型检验的TeamLTL结果，并确定其不可判定性边界。特别是，我们证明了任何向下封闭的TeamLTL扩展的所谓的左平坦片段的模型检验的可判定性。此外，我们建立了具有布尔析取和包含原子的TeamLTL的模型检验问题是不可判定的。
2021-11-23 cs.CC cs.LO
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
Technische Universität Dresden（德累斯顿工业大学）
对于关系一元公式（Löwenheim类），二阶量词消去，这是密切相关的计算一致插值，投影和遗忘-操作，目前受到关注的知识处理-总是成功的。Heinrich Behmann从1922年开始对这个类的可判定性证明是通过等价保持公式重写的消元法进行的。在这里，我们重建的结果从Behmann的出版物的详细和讨论相关的问题，在现代方法的背景下，二阶量词消去在计算逻辑。此外，广泛的文件的信件和手稿在贝曼的遗赠，关注二阶量词消去，包括一个评论登记册和英文摘要的德语来源，重点是技术材料。在20世纪20年代后期，Behmann试图为谓词的元数大于1的公式开发一种基于消除的决策方法。他的手稿和与威廉·阿克曼的通信显示了今天仍然感兴趣的技术方面，并深入了解了阿克曼1935年的里程碑式论文“Untersuchungen über das Eliminationsproblem der mathematischen Logik”的起源，该论文奠定了两种流行的现代二阶量词消去方法的基础。
2017-12-19 cs.AI cs.LO
Alternating register automata on finite words and trees
我们研究交替寄存器自动机的数据字和数据树的逻辑。数据字（或数据树）是一个字（或树），其每个位置携带来自有限字母表的标签和来自无限域的数据值。我们研究单向自动机与交替控制数据字或树，一个寄存器存储数据和比较它们的平等。这是Demri，Lazic和Jurdzinski开始的研究的延续。从寄存器自动机模型的角度出发，本文的工作有两个目的：（1）简化已有的交替寄存器自动机空性问题的可判定性证明;（2）展示这些模型的可判定扩展。从逻辑的角度来看，我们表明，（a）在数据字的情况下，满足性的LTL与一个寄存器和量化的数据值是可判定的;和（b）满足性的问题，所谓的前向片段的XML文档是可判定的，即使在存在的DTD，甚至是关键的约束。可判定性是通过减少自动机模型介绍。这个片段包含子轴、后代轴、下一个兄弟轴和下一个兄弟轴，以及数据相等和不相等测试。
2012-03-07 cs.DB cs.FL cs.LO
A Linear-Time Nominal $μ$-Calculus with Name Allocation
无限字母表语言的逻辑和自动机模型，如Freeze LTL和寄存器自动机，用于验证过程或带有数据的文档。它们与名义集上的形式主义密切相关，例如非确定性轨道有限自动机（NOFA），其中名称扮演数据的角色。在这种形式主义中的推理问题在计算上往往是困难的。名字绑定的名义自动机模型，如规则的非确定性名义自动机（RNAs）已被证明是计算上更容易处理。在本文中，我们介绍了一个线性时间不动点逻辑Bar-muTL有限字在一个无限的字母表，它的特点是完全否定和冻结量化通过名称绑定。我们通过对扩展的正则非确定性名义自动机的非平凡约简表明，尽管Bar-muTL允许无限制的非确定性和无限多的寄存器，但RNAs上的模型检验Bar-muTL和可满足性检验都具有基本的复杂性.例如，模型检验在2 ExpSpace中，更准确地说是在参数化的ExpSpace中，有效地将寄存器的数量作为参数。
2021-08-20 cs.FL cs.LO
Decidability of Timed Communicating Automata
研究了时间通信网络的可达性问题。每个进程都是一个时间自动机，通过在无界FIFO通道上交换消息与其他进程进行通信。消息携带时钟，该时钟在发送和接收时以适当的定时约束进行检查。每个自动机只能访问它的本地时钟和发送/接收消息的消息时钟集。时间是密集的，所有的时钟都以相同的速度进化。我们的主要贡献是一个完整的特征的可判定和不可判定的通信拓扑结构概括和统一以前的工作。从技术的角度来看，我们使用量词消去和减少计数器自动机与寄存器。
2018-04-20 cs.DC 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
Feasible Automata for Two-Variable Logic with Successor on Data Words
我们介绍了一个自动机模型的数据字，这是在每个位置进行一个符号从一个有限的字母表和一个值从一个无界的数据域的话。该模型是（语义）的数据自动机，介绍了Bojanczyk，等的限制。在2006年，它被称为弱数据自动机。它的表达能力比数据自动机差，而表达能力又是寄存器自动机无法比拟的。弱数据自动机的表达能力与后继为+1且数据值相等\sim，EMSO 2（+1，\sim）的存在一元二阶逻辑完全对应。它遵循从以前的工作，大卫，等。等人在2010年提出了弱数据自动机的非空性问题可以在2-NEXPTIME中判定。此外，我们还研究了数据ω-串上的弱Büchi自动机。它们可以用EMSO 2（+1，\sim）的扩展来刻画，其中存在量词用于无限集合.最后，通过对弱数据自动机的非空性问题进行非确定性多项式时间约简，得到了其非空性问题的复杂性界。
2011-10-06 cs.FL cs.LO
