Satisfiability Games for Branching-Time Logics
分支时间时态逻辑如CTL*、CTL和CTL+的可满足性问题在程序规范和验证中有重要的应用。它们的计算复杂性是已知的：CTL* 和CTL+对于双指数时间是完全的，CTL对于单指数时间是完全的.这些逻辑的一些决策程序是已知的;它们使用树自动机，tableaux或公理系统。在本文中，我们提出了一个统一的博弈论框架，这些分支时间时序逻辑的可满足性问题。我们定义可满足性游戏的完整的分支时间时序逻辑CTL* 使用高层次的定义获胜的条件，抓住了最少不动点展开的本质的良好基础。这些获胜条件构成了ω-词的形式语言。我们分析了在何种情况下需要哪种确定性ω-自动机来识别这些语言。然后，我们得到一个减少的问题，解决奇偶校验或Büchi游戏。所获得的算法的最坏情况下的复杂性匹配这些逻辑的已知下界。这种方法提供了一个统一的，但复杂性理论上的最佳处理分支时间时序逻辑的可满足性。它将时序逻辑机器的使用与自动机的使用分开，从而保留了输入公式和表示可满足性的对象之间的语法关系，即奇偶或Büchi游戏中的获胜策略。这里介绍的游戏只在输入公式的Fischer-Ladner闭包上工作。最后但并非最不重要的是，这里提出的游戏来尝试提供工具支持复杂的分支时间逻辑，如CTL* 和CTL+的可满足性问题。
2013-10-15 cs.LO
Alternating Automata on Data Trees and XPath Satisfiability
数据树是一个无序的有序树，它的每个节点都由一个来自有限字母表的字母和一个来自无限集合的元素（“数据”）标记，其中后者只能比较相等。本文考虑了数据树上的交替自动机，它可以向下移动和向下移动，并且有一个寄存器用于存储数据。主要结果是：有限数据树上的非空性是可判定的，但不是原始递归的;安全自动机的非空性是可判定的，但不是初等的。证明使用不确定树自动机与故障计数器。允许向上移动、向下移动或两个寄存器，每一个都会导致不可判定性。作为推论，可判定性获得两个数据敏感片段的XML查询语言。
2010-06-14 cs.DB cs.FL cs.LO
Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures
本文提出树约束自动机，证明CTL(Z)与CTL*(Z)可满足性分别为ExpTime和2ExpTime完全，解决长期开放问题。
2025-06-18 cs.LO
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。
2023-11-09 cs.FL cs.LO
Revisiting MITL to Fix Decision Procedures
度量区间时态逻辑（Metric Interval Temporal Logic，MITL）是一种具有可判定可满足性和模型检验问题的实时时态逻辑。MITL的决策过程依赖于自动机理论方法，其中逻辑公式被转换为等效的时间自动机。由于时间自动机在互补下不封闭，MITL的决策过程首先将公式转换为否定的范式，然后再转换为时间自动机。我们发现，不幸的是，这些20岁的程序是不正确的，因为它们依赖于一个不正确的语义的R运算符。我们提出了正确的语义R，并给出了新的，正确的决策程序MITL。我们表明，可满足性和模型检验的MITL是EXPSPACE完全的，如前所述。我们还确定了一个片段的MITL，我们称之为MITL_{WI}是丰富的比MITL_{0,\infty}，我们表明，可满足性和模型检验是PSPACE完成。我们的许多结果已经在PVS中得到了形式化的证明。
2019-10-09 cs.LO
The complexity of linear-time temporal logic over the class of ordinals
我们考虑的时间逻辑与因为和直到模态。这种时态逻辑在表达上等价于一阶逻辑的坎普定理。我们证明了它有一个PSPACE-完全可满足性问题的序数类。在我们的证明的后果，我们表明，给定的代码的一些可数序数α和一个公式，我们可以在PSPACE中决定是否有一个模型的α公式。为了证明这些结果，我们引入了一类简单的序数自动机，作为表达Büchi序数自动机。通过将时态逻辑的可满足性问题归结为简单有序自动机的非空性问题，得到了时态逻辑可满足性问题的PSPACE上界。
2010-12-21 cs.LO
From $μ$-Calculus to Alternating Tree Automata using Parity Games
$μ$ -无限树上的微积分和自动机是描述无限树语言的互补方式。利用$μ$ -Calculus与交替树自动机之间的对应关系，将模式$μ$ -Calculus公式编译成交替树自动机，解决了可满足性和模型检验问题.因此提倡一个自动机模型，专门为工作模式$μ$ -微积分。与Janin和Walukiewicz提出的自动机模型相比，自动机模型的优点是能够以更简单的方式处理任意分支。这两个问题（即，模型检验和可满足性）分别通过约简到交替树自动机的相应问题，即接受问题和非空问题来解决。这些问题，反过来，解决使用奇偶性游戏的语义交替树自动机被翻译成一个获胜的战略，在一个适当的奇偶性游戏。
2016-02-02 cs.FL cs.LO
Alternating Nonzero Automata
我们引入了一类新的无限树上的自动机，称为\emph{alternating nonzero automata}，它扩展了非确定非零自动机。我们减少交替非零自动机的空性问题为非确定性的，这意味着可判定性相同的问题。作为推论，我们得到的概率时序逻辑扩展CTL* 和定性片段的pCTL* 的可满足性算法。
2018-02-12 cs.FL cs.LO
Satisfiability and Model Checking of CTL* with Graded Path Modalities
分次路径模态计算满足一个性质的路径的数量，并推广了CTL* 的存在（E）和泛（A）路径模态。生成的逻辑称为GCTL*。我们解决了GCTL* 可满足性的复杂性，即，2 ExpTime-Complete，以及GCTL* 的模型检验问题的复杂性，即，PSpace-Complete。对于CTL*，下限已经成立，因此，使用自动机理论方法，我们提供上限。这项工作的意义是双重的：GCTL* 比CTL* 更有表达力，而在计算复杂性方面没有额外的成本，并且GCTL* 具有CTL* 优于CTL的所有优点，例如，表达公平的能力。
2014-10-28 cs.LO
Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
本文提出带极值约束的寄存器自动机模型，证明其空性问题可判定，并应用于二变量逻辑，在树序和线性序存在时证明其可数可满足性及可满足性问题可判定。
2022-03-21 cs.FL cs.LO
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete
IIT Bombay（印度理工学院孟买分校）；MPI-SWS（马克斯·普朗克软件系统研究所）
本文证明多变量单侧区间TPTL的可满足性检验为PSPACE完全，且其表达力严格强于MITL，但检验复杂度更低，通过归约到新的非点式交替定时自动机子类实现。
2023-09-01 cs.CL cs.FL 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
The Complexity of Enriched Mu-Calculi
Università di Napoli “Federico II”（那不勒斯费德里科二世大学）；TU Dresden（德累斯顿工业大学）；Microsoft Research（微软研究院）；Rice University（莱斯大学）
完全丰富演算是命题演算的逆程序、分次模态和名值的推广.虽然满足性在几个表达片段的充分丰富的演算被称为是可判定的和ExpTime完全的，它最近被证明，完整的演算是不可判定的。在本文中，我们研究的片段的充分丰富的演算，通过删除至少一个额外的结构。我们表明，在以这种方式获得的所有片段中，可满足性是可判定的和ExpTime完全的。因此，我们确定了一个家庭的可判定的逻辑是最大的（和无与伦比的）的表达能力。我们的结果是通过引入两个新的自动机模型，表明他们的空性问题是ExpTime-完全的，然后减少这些问题的相关逻辑的可满足性。我们介绍的自动机模型是双向分级交替奇偶自动机在无限树（2GAPTs）和完全丰富的自动机在无限森林（FEAs）。前者是文献中两个不可比自动机模型的常见推广。后者扩展交替自动机以类似的方式完全丰富的演算扩展标准演算。
2008-09-22 cs.CL cs.LO
Extending Büchi Automata with Constraints on Data Values
最近，数据树和数据字在XML推理和系统验证方面受到了相当大的关注。这些是树或词，除了来自有限字母表的标签之外，还携带来自无限字母表的数据值（数据）。一般来说，很难获得足够表达的数据字和树的逻辑，但对于可满足性问题仍然具有合理的复杂性。在本文中，我们扩展和研究的概念，Büchi自动机的欧米茄字的数据。我们证明了这种扩张的空性问题在初等复杂性下是可判定的。然后，我们应用我们的结果来显示两种逻辑的可判定性的欧米茄字的数据：一阶逻辑的两个变量的片段和一些经典的线性时序逻辑的欧米茄字的数据的扩展。
2012-06-23 cs.LO
Grammatical Inference as a Satisfiability Modulo Theories Problem
Institute for Computing；Information Sciences Radboud University Nijmegen, The Netherlands Email
从可满足性模理论的角度研究了从一组标记符号序列中学习最小一致模型的问题。我们提出了两种编码确定性有限自动机和扩展这些Moore和Mealy机之一。我们的实验结果表明，这些编码提高了国家的最先进的，是有用的，在实践中学习小模型。
2017-05-30 cs.FL cs.LG 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
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
Model checking memoryful linear-time logics over one-counter automata
我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。
2010-01-18 cs.LO
Logics Meet 2-Way 1-Clock Alternating Timed Automata
本文研究了单时钟交替时间自动机（1-ATA）的扩展，即双向单时钟交替时间自动机（2-Way 1-ATA）。我们证明了具有重置自由循环的2-Way 1-ATA的子类（2-Way 1-ATA-rfl）在表达上等价于用保护度量量词（GQMSO）扩展的MSO[<]。2路1-ATA-rfl（以及因此GQMSO）的空性检查问题通常是不可判定的。我们提出了一个“非准时性”的限制，称为非邻接，2路1-ATA-rfl，也为GQMSO，其中的空（分别满足性）检查成为可判定的。非相邻2路1-ATA是第一类具有交替和2路性的时间自动机，其空性检查是可判定的（并且也具有初等复杂性）。我们还表明，2路1-ATA-rfl，即使与非相邻的限制，可以表达属性是不可识别的使用1-ATA。
2022-02-26 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
Model Checking Regular Language Constraints
即使是最快的SMT求解器在处理来自真实程序的正则表达式时也会遇到性能问题。由于这些性能问题通常来自问题表示（例如，非确定性有限自动机得到确定和正则表达式得到展开），我们重新审视布尔有限自动机，它允许直接和自然的表示任何正则语言的布尔组合。将IC3模型检验算法应用于布尔有限自动机，不仅可以有效地回答空性和普适性问题，而且通过扩展，可以判定多变量串成员问题的可满足性。我们证明了所产生的系统的有效性，一些流行的基准和正则表达式。
2017-08-30 cs.FL cs.LO cs.SC
Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach
可满足性模理论（SMT）求解器已经成功地应用于解决形式化验证中的许多问题，例如从集成电路到信息物理系统的许多类系统的有界模型检验（BMC）。通常，BMC是通过检查一个可能很长但没有量词的公式的可满足性来执行的。然而，BMC问题可以自然地编码为BMC步骤数量的量化公式。在这种方法中，我们然后使用决策程序支持量词来检查这些量化公式的可满足性。该方法先前已被应用于使用量化布尔公式（QBF）编码来执行用于纯离散系统的BMC，然后使用QBF求解器来释放QBF检查。在本文中，我们提出了一个新的量化编码的BMC矩形混合自动机（RHA），这需要使用更一般的逻辑，由于实（密集）时间和实值状态变量建模连续状态。我们已经实现了一个初步的实验原型的方法，使用HyST模型转换工具生成量化BMC（QBMC）查询的Z3 SMT求解器。我们描述了几个时间和混合自动机的基准，如费舍尔和林奇-斯考特互斥算法的实验结果。我们将我们的方法与无量化器的BMC方法进行比较，例如使用dReal SMT求解器的dReach工具中的方法，以及使用MathSAT SMT求解器构建在nuXmv之上的HyComp工具。基于我们有前途的实验结果，QBMC可能在未来是一个有效的和可扩展的分析方法RHA和其他类的混合自动机的进一步改进，在SMT求解器，如Z3的量词处理。
2022-07-14 cs.FL cs.LO cs.SC
Satisfiability Bounds for $ω$-Regular Properties in Bounded-Parameter Markov Decision Processes
本文考虑有界参数马尔可夫决策过程满足$ω$ -正则性的最小和最大概率的计算问题。BMDP由马尔可夫决策过程（MDP）产生，允许以实际概率未知的间隔形式的转移概率上的不确定性。$ω$ -正则语言形成了一大类属性，例如，拉宾或奇偶自动机，包含丰富的规范，如线性时序逻辑。在BMDP中，满足该属性的概率取决于未知的转移概率以及策略。在本文中，我们计算极值。这解决了Dutreix和Coogan在CDC 2018中特别提出的问题，扩展了他们在没有对手的区间马尔可夫链上的结果。其主要思想是重新解释他们的工作作为分析的区间MDP和相应的BMDP问题的分析的$ω$定期随机游戏，其中提供了一个解决方案。该方法进一步平滑地扩展到有界参数随机博弈。
2022-07-27 cs.LO cs.SY eess.SY
Arbitrary-arity Tree Automata and QCTL
IRISA -- Inria, CNRS, Univ. Rennes（IRISA - 法国国家信息与自动化研究所，法国国家科学研究中心，雷恩大学）
本文提出 EU-自动机，并利用其为 QCTL 和 MSO 提供了最优复杂度的决策算法及量词交替转换方法。
2026-02-26 cs.FL cs.LO
Guarded Negation Transitive Closure Logic
Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800（波尔多大学）；University of Buenos Aires（布宜诺斯艾利斯大学）；CONICET（阿根廷国家科学研究委员会）；Chiba University（千叶大学）
本文研究了guarded negation fragment of transitive closure logic (GNTC) 的可满足性问题，证明其为2ExpTime-完全，并展示了该逻辑的模型检查问题在组合复杂度下为P^NP[O(log^2 n)]-完全。
2026-07-21 cs.DB 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
Buchi automata augmented with spatial constraints: simulating an alternating with a nondeterministic and deciding the emptiness problem for the latter
这项工作的目的是彻底调查Buchi自动机增强空间约束。这种自动机的输入树是无限k元西格玛树，节点代表时间点，西格玛除了在经典的k元西格玛树中使用外，还包括对感兴趣的n对象空间场景的快照的描述。来自RCC8类空间关系代数（RA）x的约束用于对空间场景的对象施加空间约束，最终在输入树的不同节点处。我们表明，一个布奇交替增强空间约束的自动机可以模拟与经典的布奇不确定自动机相同类型，增强空间约束。然后，我们提供了一个非确定性的双深度优先多项式空间算法的空问题，后者自动机。我们的主要动机来自另一项工作，也提交给这次会议，它定义了一个时空化的著名家庭ALC（D）的描述逻辑与一个具体的域：一起，这两个作品提供了一个有效的解决方案的可满足性问题的概念的时空化的弱循环TBox。
2020-02-22 cs.FL cs.LO
FO logic on cellular automata orbits equals MSO logic
本文将经典元胞自动机扩展至任意标记图，证明其轨道上的 FO 逻辑等价于 MSO 逻辑，并据此推导出模型检测与可满足性的不可判定性结论及具体公式实例。
2024-04-25 cs.DM cs.LO math.DS
Model-checking real-time systems: revisiting the alternating automaton route
Chennai Mathematical Institute（金奈数学研究所）；CNRS, ReLaX, IRL 2000（法国国家科学研究中心、ReLaX实验室、IRL 2000）
本文提出了一种基于区域方法的1-ATA空性算法，改进了MTL到1-ATA的转换，并研究了在特定条件下模型检验实时系统的方法。
2026-01-06 cs.FL cs.LO
Symmetry Breaking Predicates for SAT-based DFA Identification
ITMO University（圣彼得堡国立信息技术机械与光学大学）
以往的研究表明，确定性有限自动机（DFA）识别的NP难问题可以有效地转化为布尔可满足性（SAT）问题。现代SAT求解器可以有效地处理困难的DFA识别实例。我们提出了一种技术，以减少问题的搜索空间，通过执行深度优先搜索（DFS）或广度优先搜索（BFS）顺序的DFA状态的枚举。我们提出对称破缺谓词，它可以被添加到布尔公式代表各种DFA识别问题。我们将展示如何将这种技术应用于DFA识别无噪声和噪声数据。此外，我们提出了一种方法来确定所需的大小的所有自动机。所提出的方法优于当前国家的最先进的DFASAT方法DFA识别无噪声数据。所提出的方法的一个很大的优点是，它允许准确地确定存在或不存在的解决方案的噪声DFA识别问题不同于元启发式方法，如遗传算法。
2016-02-17 cs.AI cs.FL cs.LO
