The Complexity of Satisfiability Checking for Symbolic Finite Automata
本文研究符号有限自动机的可满足性问题，通过将其分解为输入字符理论与接受单词索引的单子二阶理论，获得了该自动机类及其线性算术约束扩展的紧计算复杂度界限。
2023-06-30 cs.LO
Complexity of the Model Checking problem for inquisitive propositional and modal logic
本文研究了探究命题逻辑 InqB 和探究模态逻辑 InqM 的模型检测问题复杂性，基于 Yang 的思想证明了这两个问题均为 AP-完全。
2024-03-28 cs.LO math.LO
On the complexity of the model checking problem
在过去的二十年里，一阶逻辑的各种片段的模型检验问题引起了人们的广泛关注：特别是对于原始正片段和正Horn片段，它们分别被称为约束满足问题和量化的约束满足问题。事实上，这两个片段是目前唯一没有已知复杂性分类的片段。所有其他的句法片段可以很容易地分类，无论是直接或使用Schaefer的二分法定理SAT和QSAT，除了积极平等自由片段。这个突出的片段也可以被分类，并享有四分法：根据模型，相应的模型检验问题是易于处理的，NP完全的，co-NP-complete或Pspace-complete。此外，复杂度下降总是见证了一个通用的解决算法，使用量词相对化。此外，它的复杂性的特点是代数手段：存在或不存在特定的满射超运算之间的那些保持模型的复杂性。
2012-10-25 cs.CC cs.LO
Path Checking for MTL and TPTL over Data Words
本文研究了数据词上MTL与TPTL的路径检查问题，依据寄存器数量和约束编码方式给出完整复杂度分析，证明MTL为P完全、TPTL为PSPACE完全，并得出单计数器机器模型检查的精确复杂度。
2017-09-01 cs.LO
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。
2023-11-09 cs.FL cs.LO
A Note on the Complexity of Model-Checking Bounded Multi-Pushdown Systems
本文给出了模型检验多下推系统的复杂性刻画。多下推系统对递归并发程序进行建模，其中任何顺序进程都具有有限控制。我们认为有界性的三个标准概念：上下文有界性，相位有界性和堆栈排序。逻辑形式主义是一个线性时间时态逻辑，扩展了著名的逻辑CaRet，但专用于多下推系统，其中抽象运算符（与调用和返回有关），例如下一次和直到被堆栈参数化。我们表明，这个问题是EXPTIME-完全的上下文有界的运行和一元编码的上下文开关的数量，我们还证明了这个问题是2 EXPTIME-完全的相位有界的运行和一元编码的相位开关的数量。在这两种情况下，值k都作为输入给出（因此它不是模型检验问题的常数），这在复杂性上产生了实质性的差异。在某些情况下，我们的结果改善了以前的复杂性结果。
2012-12-06 cs.FL cs.LO
Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
Ong证明了由n阶递归方案生成的可能无限排序树的模态μ演算模型检验问题（等价于交替奇偶树自动机（APT）接受问题）是n-EXPTIME完全的。我们认为两个子类的APT和调查各自的验收问题的复杂性。主要结果是，对于APT与一个单一的优先级，问题仍然是n-EXPTIME完全的，而对于APT与一个析取转移函数，问题是（n-1）-EXPTIME完全的。Kobayashi最近的工作表明，函数式程序的资源使用验证可以简化为递归模式的模型检验。作为一个应用，我们证明了资源使用验证问题是（n-1）-EXPTIME完全的。
2011-12-20 cs.LO cs.PL
The parameterized space complexity of model-checking bounded variable first-order logic
本文研究有界变量一阶查询模型检测的参数化空间复杂度，建立树层次结构完备性，提出高空间效率检测器，并探讨其最优性。
2019-09-19 cs.LO
Dichotomies and Duality in First-order Model Checking Problems
我们研究的复杂性的模型检验问题，固定的模型A，在一定的片段L的一阶逻辑。这些有时被称为L的表达式复杂性。我们得到各种复杂性分类定理，这些逻辑L的范围在模型A，在二分法猜想的约束满足问题的精神-这本身可以被看作是模型检验问题的存在合取正一阶逻辑。
2006-11-28 cs.CC cs.LO
Model Checking Existential Logic on Partially Ordered Sets
我们研究了在有限偏序集（简称偏序集）中检验存在句（即使用存在量词和所有布尔连接词构建的前缀形式的一阶句）是否为真的问题。偏序集是一个自反的、反对称的、传递的有向图。这个问题包括基本的嵌入问题，找到一个同构的副本偏序集作为诱导子结构的另一个偏序集。模型检验存在逻辑已经是NP-困难的固定偏序集，因此，我们研究的结构性质的偏序集产生条件的固定参数易处理的问题时，参数化的句子。我们确定宽度作为一个中心的结构属性（偏序集的宽度是成对的不可比元素的子集的最大大小），我们的主要算法的结果是，模型检验存在逻辑类的有限偏序集的有界宽度是固定参数听话。我们观察到一个类似的现象，在经典的复杂性，我们证明了同构问题是多项式时间有界宽度的偏序集类听话，这解决了一个开放的问题，为了理论。我们围绕我们的主要算法结果的复杂性结果限制较少，自然相邻类的有限偏序集，在这个意义上建立其紧密性。我们还将我们的工作与（并证明其独立性）的基本固定参数的有界度和有界宽度的有向图的模型检验的易处理性结果。
2014-04-15 cs.DS 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
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
A Parameterized View on the Complexity of Dependence Logic
本文研究了团队语义学领域中一种成熟的逻辑--依赖逻辑的模型检验的参数化复杂性。我们从这个问题的九个直接参数化的列表开始，即：分裂）/（自由）变量/全称量词，公式大小，输入结构的Gaifman图的树宽度，宇宙/团队的大小，以及依赖原子的arity。我们提出了一个全面的图片参数化的复杂性的模型检验，并获得了一个划分的问题，分为易处理和各种棘手的程度。此外，我们还考虑了复杂性的最重要的变量（数据和表达式的复杂性）的模型检验问题，通过固定部分的输入。
2021-09-20 cs.LO
ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking
我们给出了第一个ExpTime（复杂性最优）的Tableau决策过程，用于检查描述逻辑SHIQ中的知识库的可满足性，当数字以一元编码时。我们的程序是基于全局状态缓存和整数线性可行性检查。
2013-12-31 cs.LO
Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
CISPA Helmholtz Center for Information Security（CISPA 赫尔姆霍兹信息安全中心）；Bar Ilan University（巴伊兰大学）；Saarland University（萨尔兰大学）
本文研究了超2LTL在有限结构上的模型检查问题，证明其在树状和无环结构上的可判定性，并探讨了不同片段的复杂性。
2026-01-28 cs.FL cs.LO
The Complexity of Model Checking Higher-Order Fixpoint Logic
高阶不动点逻辑（Higher-Order Fixpoint Logic，HFL）是简单类型λ演算和模态λ演算的混合。这使得它成为一个高度表达的时态逻辑，能够表达模态λ演算中无法表达的程序的各种有趣的正确性属性。本文给出了其模型检验问题的复杂性结果。特别是，我们认为这些片段的HFL只使用类型的有界阶k和arity m。我们建立k倍指数时间完备性的模型检验每个这样的片段。对于上界，我们使用不动点消除，以获得可达性游戏，是单指数的大小的公式和k倍指数的大小的底层过渡系统。这些博弈可以在确定性线性时间内求解。作为一个简单的结果，我们得到一个指数时间上界的表达复杂性的每个这样的片段。下界是由交替（k-1）重指数空间有界图灵机的字问题的一个简化而建立的。由于有固定的机器的类型，其字的问题已经很难相对于k倍指数时间，我们得到，作为一个推论，k倍指数时间完整性的数据复杂性的片段的HFL，提供m超过3。这也产生了表达能力的层次结构。
2007-06-29 cs.LO
On the Complexity of Verifying Regular Properties on Flat Counter Systems
在计数器系统验证的近似方法中，其中之一是模型检验其平坦展开。不幸的是，除了可达性查询或过去的LTL模型检查问题的复杂性表征，这种业务模型并不总是很好地研究。在本文中，我们描述的复杂性的模型检测问题的平面计数器系统的规约语言，包括一阶逻辑，线性μ演算，无限自动机，和相关的形式主义。我们的研究结果跨越不同的复杂性类（主要是从PTime到PSpace），它们适用于计数器值的算术约束系统允许的语言。就证明技术而言，我们提供了一种集中于主要问题的统一方法。
2013-04-23 cs.LO
The Complexity of Generalized HyperLTL with Stuttering and Contexts
ENS Rennes（雷恩高等师范学院）；Aalborg University（奥尔堡大学）
本文研究了包含停滞和上下文的广义超LTL的可满足性、有限状态可满足性和模型检查问题的复杂性，证明了可满足性为Σ₁¹-完全，而模型检查和有限状态可满足性则等价于二阶算术中的真值，远比可决定的超LTL模型检查问题复杂。
2026-11-02 cs.LO
The Model Checking Problem for Distributed Knowing How is $Δ^p_2$-Complete
University of Amsterdam（阿姆斯特丹大学）
研究了分布式知道如何的模型检测问题的复杂性，证明该问题是 $\Delta^p_2$-完全的。
2026-06-26 cs.LO
Complexity of Model Checking for Modal Dependence Logic
模态依赖逻辑（Modal Dependence Logic，MDL）是由Väänänen最近提出的。它通过操作符=（）增强了基本模态语言。对于命题变量p_1，.，p_n原子式=（p_1，...，p_（n-1），p_n）直观地说明p_n的值仅由p_1，.，p_（n-1）。我们证明了Kripke结构上MDL公式的模型检验是NP完全的，并进一步考虑了通过限制允许的命题和模态连接词的集合而得到的MDL片段。事实证明，几个片段，例如，没有情态动词或没有命题连接词的句子仍然是NP完全的。我们还考虑了MDL的限制，其中每个单个依赖原子的长度由整个逻辑固定的数字限制。我们表明，这个有界MDL的模型检验问题仍然是NP完全的。我们还通过允许经典析取（由Sevenster引入）来扩展MDL，除了依赖析取之外，并表明经典析取总是至少与有界元依赖原子一样糟糕，在某些情况下甚至更糟，例如，只有两个析取的片段是NP完全的。此外，我们几乎完全分类的计算复杂性的模型检验问题的所有限制的命题和模态算子的无界以及有界MDL。
2012-01-27 cs.CC 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
Parametrised Complexity of Model Checking and Satisfiability in Propositional Dependence Logic
在本文中，我们开始在依赖逻辑领域的参数化复杂性的系统研究，发现它的起源于依赖逻辑的Väänänen从2007年。我们研究这个逻辑（PDL）的命题变体，并调查各种参数化相对于中央决策问题。PDL的模型检验问题是NP完全问题。本研究的主题是确定一个参数列表（公式大小，树宽，树深，团队规模，变量数）下MC成为固定参数易处理。此外，我们表明，析取的数量或依赖原子的arity（dep-arity）作为一个参数都产生paraNP-完全性的结果。然后，我们考虑的可满足性问题（SAT）显示出不同的图片：在团队规模，或deparity SAT是paraNP-完全的，而在所有其他提到的参数的问题是FPT。最后，我们介绍了一个变种的可满足性问题，要求一个给定的规模的团队，并显示这个问题的一个几乎完整的图片。
2020-06-13 cs.CC 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
Computational Complexity of Model-Checking Quantum Pushdown Systems
本文研究了量子栈系统模型检查的计算复杂性，证明了量子栈系统在特定逻辑下的可判定性，并展示了其NP难性。
2026-08-10 cs.CC cs.LO
Model-Checking Problems as a Basis for Parameterized Intractability
大多数参数化复杂性类都是根据布尔可满足性问题（所谓的加权可满足性问题）的参数化版本来定义的。例如，Downey和Fellow的W-层次结构就是这种形式。但是也有一些类，例如A-层次，它们更自然地以一阶逻辑的某些片段的模型检验问题来表征。唐尼、费罗斯和里根是第一个在两种形式主义之间建立联系的人，他们用一阶模型检验问题来描述W-层次。我们改进了他们的结果，然后证明了A-层次和W^*-层次的加权可满足性和模型检验问题之间类似的对应关系。因此，我们获得了非常统一的许多最重要的参数化复杂性类的特征，在这两种形式主义。我们的结果可以用来给一些结构参数化复杂性理论的核心结果的新的，简单的证明。
2005-06-22 cs.CC cs.LO
On the Computational Complexity of Model Checking for Dynamic Epistemic Logic with S5 Models
Institute for Logic, Language and Computation University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）
动态认知逻辑（DEL）是一个逻辑框架，用于表示和推理多个代理的知识变化。在这个框架中的一个重要的计算任务是模型检验问题，这已被证明是PSPACE硬，即使是S5模型和两个代理-在其他功能的存在下，如多点模型。我们回答开放的问题，在文献中这个问题的复杂性，在更受限制的设置。我们提供了一个详细的复杂性分析的模型检验问题的DEL，在那里我们考虑各种组合的限制，如代理的数量，无论是单点或多点的模型，以及是否后置条件允许在更新。特别是，我们证明了这个问题已经是PSPACE困难的（1）一个代理的情况下，多点S5模型，没有后置条件，和（2）两个代理的情况下，只有单点S5模型，没有后置条件。此外，我们还研究了只允许半私有公告作为更新的设置。我们表明，在这种情况下，问题已经是PSPACE-硬时，限制到两个代理和三个命题变量。我们在本文中获得的结果有助于勾勒出确切的边界的限制设置的模型检验问题的DEL是计算上易于处理的。
2020-09-18 cs.AI cs.CC cs.LO
On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions
本文研究了Halpern和Shoham的区间时序逻辑HS的模型检验问题。在过去的几年里，间隔时态逻辑MC作为传统（基于点）时态逻辑MC的可行替代方案越来越受到关注，传统时态逻辑MC可以被恢复为特殊情况。大多数结果都是在同质性假设下得到的，即约束一个命题字母在一个区间上成立当且仅当它在每个分量状态上成立。最近，Lomuscio和Michaliszyn提出了一种放松这种假设的方法，利用正则表达式来定义命题字母在其组成状态方面的行为。当同质性假设，MC的确切复杂性是一个困难的公开问题，充分HS和它的两个句法最大片段AA'BB' E '和AA' EB 'E'。在本文中，我们提供了一个渐近最优的约束下，这两个片段的复杂性更有表现力的语义变体的基础上，正则表达式的MC问题是AEXP_pol-完成，其中AEXP_pol表示的复杂性类的问题，由指数时间有界的交替图灵机，使一个多项式有界的交替。
2017-09-07 cs.CC cs.LO
The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum
本文研究了在 van Glabbeek 分支时间谱中，判定有限无环过程特征公式的复杂度，给出了可满足性与素性问题的复杂度结果，并探讨了多项式时间可解与计算困难的逻辑边界及公式构造的复杂度。
2024-11-13 cs.LO
Tractability Frontier of Data Complexity in Team Semantics
研究了具有团队语义的逻辑模型检测的数据复杂性。我们专注于严格和宽松的团队语义下的依赖，包含和独立逻辑公式。我们的研究结果描绘了一个清晰的易处理性/难处理性边界的数据复杂性的量化器的自由和量化的公式为每个逻辑。对于松散语义下的包含逻辑，我们将模型检测问题归结为所谓的双Horn布尔公式的可满足性问题。通过这种约简，我们给出了包含逻辑的数据复杂性在PTIME内的已知结果的另一种证明。
2021-08-12 cs.LO
The Complexity of Generalized HyperLTL with Stuttering and Contexts
本文确定了带 stuttering 和 contexts 的广义 HyperLTL 的可满足性与模型检测复杂度，证明可满足性为 $Σ_1^1$-完全，而模型检测等价于二阶算术真值且远难于 HyperLTL。
2025-09-17 cs.FL cs.LO
Agent-Alternation-Free Epistemic Metric Temporal Logic with Past: Model Checking and Complexity
Université Paris-Saclay（巴黎萨克雷大学）；CNRS（法国国家科学研究中心）；ENS Paris-Saclay（巴黎萨克雷高等师范学校）；LMF（拉格兰日数学实验室）；Institut Universitaire de France（法兰西学院）；Direction Générale de l’Armement（法国国防总局）
研究带过去时态的无主体交替认知度量时态逻辑的模型检查，通过结合时态测试自动机与完美回忆观察者进行分析，证明其模型检查为EXPSPACE完全，给出了该逻辑在特定条件下的复杂性结论。
2026-07-16 cs.FL 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
The Complexity of Bisimilarity and Model Checking in Finitary Diagrams
Max Planck Institute for Informatics（马克斯·普朗克Informatics研究所）；Saarland University（萨尔兰大学）
本文通过改进ETIM问题的随机算法，将有限图的互模拟判定上界降至NEXP，图路径逻辑模型检验上界降至NP，并证明后者是NP难的。
2026-06-16 cs.LO
Quantitative Computation Tree Logic Model Checking Based on Generalized Possibility Measures
本文研究了广义可能性计算树逻辑模型检验，它是Y.Li，Y.Li and Z.Ma（2014）提出的可能性计算逻辑模型检验的扩展.该系统采用广义可能性Kripke结构（GPKS，简称）建模，验证性质由广义可能性计算树逻辑（GPoCTL，简称）公式描述.基于广义可能性测度和广义必要性测度，讨论了广义可能性计算树逻辑模型检验的方法，并详细说明了相应的算法及其复杂性。此外，给出了（2013）中引入的PoCTL与GPoCTL的比较。最后以恒温器为例说明了GPoCTL模型检测方法。
2014-09-23 cs.LO
Model Checking Lower Bounds for Simple Graphs
Frick和Grohe的一个著名结果表明，在树上决定FO逻辑涉及一个参数依赖，这是一个指数塔。虽然这个下界对于Courcelle定理来说是紧的，但它已经被最近的一系列其他图类的元定理所回避。在这里，我们提供了一些额外的非初等下界结果，这在某种意义上更强。我们的目标是解释这些最近的元定理的共同特征，并确定进一步进展的障碍。更具体地说，首先，我们表明，在类的阈值图，因此也对任何工会和互补封闭类，没有模型检查算法，即使是FO逻辑与基本参数的依赖。第二，我们表明，有没有模型检查算法与MSO逻辑的基本参数依赖，甚至限制到路径（或相当于一元字符串），除非E=NE。作为一个推论，我们解决了一个开放的问题上的复杂性的MSO模型检测的图有界的最大叶数。最后，我们看看深度为d的有色树类上的MSO。我们证明了，假设ETH，对于每个固定的d>=1，至少d+1级的指数是必要的这个问题，从而表明（d+1）倍指数算法最近给出的Gajarsky和Hlinobryny是本质上最优的。
2014-03-24 cs.CC cs.LO
The Complexity of HyperQPTL
ENS Rennes（法国高等师范学院雷恩分校）；Aalborg University（奥尔堡大学）
本文研究了超QPTL和超QPTL$^+$的复杂性，发现超QPTL的可满足性为$Σ^2_1$-完全，而超QPTL$^+$的相关问题等价于第三阶算术中的真理，均为不可判定。
2026-02-23 cs.LO
Complexity of the Description Logic ALCM
University of Leicester（莱斯特大学）
本文证明了描述逻辑ALCM中知识库的一致性检验问题是ExpTime完全的。M代表Motz，Rohrer和Severi定义的元建模。为了展示我们的主要结果，我们定义了ExpTime Tableau算法作为Nguyen和Szalas在ALC中检查知识库一致性的算法的扩展。
2015-11-12 cs.AI cs.LO
Property Checking By Logic Relaxation
本文介绍了一种新的时序电路的性质检测框架。它基于一种称为逻辑松弛（LoR）的方法。给定一个安全属性，LoR方法放松了手头的转换系统，这导致扩展了可达状态的集合。对于第j个时间帧，LoR方法计算仅由松弛系统在j个转变中可达到的坏状态集合的超集A_j。集合A_j是由一种称为部分量词消去的技术构造的。如果A_j不包含坏的状态，并且这个状态在松弛系统中的j个转换中是可达的，那么它在原始系统中也是可达的。因此，所述财产不成立。检察官办公室对PC的上诉如下。由LoR生成的归纳不变量（或反例）是计算仅在松弛系统中可达的状态的结果。因此，PC的复杂性可以通过找到一个接近原始系统的“错误”松弛来大大降低。这类似于等价性检查，其复杂性很大程度上取决于要比较的设计的相似程度。
2016-01-12 cs.LO
Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard
我们解决了多下推系统的共享内存并发程序的模型检验问题。我们认为在这里布尔程序与有限数量的线程和递归过程。众所周知，这类程序的模型检验问题是不可判定的。在本文中，我们调查的可判定性和这个问题的复杂性的假设下，有界的上下文切换定义的Qadeer和Zeroof，和相位有界的La Torre等人提出的。对时间逻辑，特别是分支时间逻辑，如模态$μ$ -演算或CTL的模型检验这样的系统很少受到关注。众所周知，与模态$μ$ -演算密切相关的奇偶博弈对于有界相位系统类是可判定的（因此对于有界上下文切换也是如此），但具有非初等复杂性（赛斯）。一个自然的问题是，这种高复杂性是否是不可避免的，有什么方法来绕过它。本文解决这些问题，不幸的是，有点令人惊讶的是，它表明，分支模型检验的MPDS本质上是一个很难的问题，没有简单的解决方案。我们证明了在相位限制下的MPDS上的奇偶博弈是非初等的。我们的主要结果表明，模型检验的$k$上下文有界MPDS对一个简单的CTL片段，由公式，其时间运营商来自集合${\EF, \EX}$，有一个非初等的下界。
2012-05-31 cs.FL cs.GT cs.LO
Model Checking Parse Trees
分析树是计算语言学和编译器构造中的基本句法结构。我们认为，在本文中，在这两个领域中，有很好的激励模型检查集的解析树的一些字根据上下文无关文法。我们提出了充分的命题动态逻辑（PDL）树在这些应用程序中，并研究作为一个健全的检查相应的模型检查问题的复杂性：虽然在一般情况下完成指数时间，我们发现自然的限制，语法为我们的应用程序，并建立复杂性范围从非确定性的多项式时间多项式空间的相关情况。
2013-03-25 cs.LO
On the Complexity of Dynamic Epistemic Logic
尽管动态认知逻辑（DEL）是一个很有影响力的逻辑框架，用于表示和推理信息变化，但很少有人知道其相关决策问题的计算复杂性。事实上，我们只知道，对于公告逻辑，一个片段的DEL，可满足性问题和模型检查问题分别是PSPACE-完全的，并在P.我们有助于填补这一空白，证明了事件模型的DEL语言，模型检查问题，令人惊讶的是，PSPACE-完全的。此外，我们证明了可满足性问题是NEXPTIME-完全的。在此基础上，我们给出了一个可靠的、完备的判定可满足性问题的表方法。
2013-10-23 cs.LO
Twin-width and Limits of Tractability of FO Model Checking on Geometric Graphs
在图上决定可在FO逻辑中表达的属性的问题的复杂性--FO模型检验问题（由相应的FO公式参数化），在所谓的稀疏图类上被很好地理解，但在遗传密集图类上理解得少得多。关于后者，最近的双宽度概念[Bonnet等人，FOCS 2020]似乎非常有用。例如，这些作者[CGTA 2019]关于置换图上FO模型检验的固定参数易处理性的确切极限在哪里的问题已经由Bonnet等人在2020年使用新引入的twin-width很容易地回答。我们证明了遗传子类的这种精确刻画与易处理的FO模型检验自然地从置换扩展到圆图（圆中弦的相交图）。也就是说，我们证明了在通常的复杂性假设下，一个遗传的圆图类的FO模型检验是在FPT当且仅当类排除一些置换图。我们还证明了FPT中具有FO模型检验的区间图的遗传类的类似的排除子图特征，这总结了[Ganian et al.，ICALP 2013年]。数学方面提出的特征-关于当子类的类的圆和置换图有界双宽度，而且扩展到所谓的有界扰动这些类。
2022-06-28 cs.DM cs.LO
Optimal Satisfiability Checking for Arithmetic $μ$-Calculi
共代数$μ$演算为不动点逻辑提供了一个通用的语义框架，其分支类型超出了标准的关系设置，例如概率，加权或基于博弈。以前的工作的coalgebraic $μ$ -演算包括指数时间上界的可满足性检查，但需要一个良好的表规则的下一步模态。这样的规则并不是在所有感兴趣的情况下都可用，特别是那些涉及整数权重的情况，如分级$μ$ -演算，或者实值权重与非线性算术的组合。在本文中，我们证明了相同的复杂性上限更一般的假设下，特别是关于（更简单）的可满足性问题的复杂性的基本所谓的一步逻辑，大致描述为嵌套的下一个步骤片段的逻辑。我们还提出了一个通用的全局缓存算法，是适合于实际使用，并支持对飞行可满足性检查。示例应用包括在具有Presburger算术的分级$μ$ -演算的扩展中用于可满足性检查的新指数时间上界，以及（二值）概率$μ$ -演算的扩展与多项式不等式。作为一个副结果，我们还得到了一个新的上限$\mathcal{O}(((nk)!)^2)$的最小模型大小的可满足的公式，所有的共代数$μ$ -演算，其中$n$是大小的公式和$k$的交替深度。
2019-01-15 cs.LO
ExpTime Tableaux with Global Caching for the Description Logic SHOQ
我们给出了第一个ExpTime（复杂性最优）的tableau决策过程，用于检查描述逻辑SHOQ中知识库的可满足性，它扩展了基本描述逻辑ALC，具有传递角色，角色层次，名词和量化数量限制。复杂度是用一元数表示来衡量的。我们的程序是基于全局缓存和整数线性可行性检查。
2014-07-21 cs.LO
The Complexity of Verifying Strategic Abilities in Succinct Multiagent Systems
Griffith University（格里菲斯大学）；CNRS, LIPN, Sorbonne Paris North University（法国国家科学研究中心，LIPN，索邦巴黎北大学）；University of Naples Federico II（那不勒斯费德里科二世大学）；University of New South Wales（新南威尔士大学）
本文研究不完全信息下多智能体系统策略能力验证的复杂性，证明SLK_P和SLK的简洁模型检验为AEXP(poly)完全，目标ATL和ATL*为P^{NEXP}完全，修正了相关旧结果并明确了主观语义下的复杂度性质。
2026-10-13 cs.LO
Equivalence Checking and Simulation By Computing Range Reduction
我们介绍了新的方法的等价性检查和模拟的基础上计算范围减少（CRR）。给定一个组合电路$N$，CRR问题是计算如果不考虑$N$的一组输入，则从$N$的范围中消失的一组输出。重要的是，在许多情况下，即使计算$N$的整个范围是不可行的，也可以有效地找到范围缩减。通过CRR解决等价性检查有助于生成模仿“切割传播”方法的等价性证明。商业工具已经成功地使用了这种方法的有限版本。通过仿真对电路$N$进行功能验证可以被视为降低计算$N$范围的复杂性的一种方式。不是查找$N$的整个范围并检查它是否包含错误输出，而是仅针对一个输入计算这样的范围。CRR仿真提供了一种处理复杂距离计算的替代方法。其思想是排除$N$的输入子集，并计算由这种排除引起的范围减小。如果消失的输出集包含错误输出，则$N$存在错误。
2015-08-11 cs.LO
Optimal Reads-From Consistency Checking for C11-Style Memory Models
本研究针对C11风格内存模型变体（如RC20、RA及其强弱变体）的读自一致性检查问题，提出了近线性时间算法并刻画了复杂性，包括最优性结果和NP难度边界，在TruSt和C11Tester中实现并显著提升性能。
2023-05-12 cs.LO cs.PL
Computation Tree Logic Model Checking Based on Possibility Measures
为了解决可能性理论中不确定信息的系统验证问题，Li和\cite{li12}引入了线性时间特性的模型检验，其中不确定性用可能性测度来建模。Xue，Lei和Li \cite{Xue09}定义了基于可能性测度的计算树逻辑（CTL），称之为可能性CTL（PoCTL）。本文是上述工作的继续。首先，我们研究了PoCTL的表现力。不同于概率CTL，它表明，PoCTL（特别是，定性PoCTL）是更强大的CTL就其表现力。详细给出了基本CTL公式与定性PoCTL公式的等价表达式。给出了一些不能用任何CTL公式表示的PoCTL公式。特别地，用PoCTL公式表示了重复可达性和持久性的一些定性性质.接着，采用CTL模型检测算法，详细讨论了PoCTL模型检测问题的解决方法及其时间复杂度。最后，通过一个实例说明了PoCTL模型检验方法。
2014-01-19 cs.LO
Linear-Time Model Checking Branching Processes
（多类型）分支过程是生成随机无限树的自然和充分研究的模型。分支过程具有非确定性和概率性分支，推广了转移系统和马尔可夫链（但不是一般的马尔可夫决策过程）。我们研究了模型检验分支过程对线性时间ω-正则规范的复杂性：它是几乎肯定的情况下，由分支过程随机生成的树的每个分支满足ω-正则规范？主要结果是，对于LTL规格这个问题是在PSPACE，包含经典的结果，分别为过渡系统和马尔可夫链。底层的一般模型检查算法是基于自动机理论的方法，使用明确的Büchi自动机。
2021-07-04 cs.FL cs.LO
Model Checking Parameterized Asynchronous Shared-Memory Systems
我们描述了参数化系统的活性验证的复杂性，由一个领导者进程和任意多个匿名和相同的贡献者进程。进程通过共享的有界值寄存器进行通信。虽然寄存器上的每个操作都是原子的，但是没有同步原语来原子地执行操作序列。我们分析的情况下，过程中建模的有限状态机或下推机和属性是由一个Büchi自动机的字母表的读取和写入行动的领导者。我们证明了这个问题是可判定的，并且具有令人惊讶的低复杂性：当所有进程都是有限状态机时，它是NP完全的，并且当它们是下推机时，它是PSPACE-hard和NEXPTIME。这种复杂性低于非参数化的情况：多个有限状态机的活性验证是PSPACE完全的，并且对于两个下推机是不可判定的。对于有限状态机，我们的证明使用存在性抽象和半线性约束来表征无限行为。对于下推机，我们展示了如何贡献者计算高栈高可以模拟计算的许多贡献者，每个低栈高。总之，我们的研究结果特征的匿名性和匿名性的假设下，参数化系统的验证的复杂性。
2015-05-25 cs.DC cs.FL cs.LO
Model Checking with Program Slicing Based on Variable Dependence Graphs
在嵌入式控制系统中，由于软件复杂性导致例如与时序相关的问题，软件缺陷的潜在风险一直在增加。这些缺陷很少通过测试或模拟发现。为了检测这种缺陷，我们提出了一种建模方法，可以生成软件模型的模型检验与程序切片技术的基础上的变量依赖图。最后将该方法应用于一个汽车控制软件的实例中，验证了该方法的有效性。此外，我们开发了一个软件工具来自动化模型生成，并取得了35%的总验证时间减少模型检验。
2013-01-01 cs.LO cs.SE
On the Complexity of Existential Positive Queries
Universitat Pompeu Fabra（庞培法布拉大学）
系统地研究了一阶逻辑存在性正片段的模型检验的复杂性。特别是，对于一组存在的肯定句，我们考虑模型检验的句子被限制到落在一组，一个自然的问题，然后分类哪些句子集是易处理的，哪些是难处理的。关于固定参数的易处理性，我们给出了一个一般定理，该定理将此分类问题简化为原始正逻辑的相应问题，用于各种结构的表示。这个一般定理允许我们推导出具有有界元的存在肯定句集是固定参数易处理的当且仅当每个句子等价于有界变量逻辑中的句子。然后，我们使用经典的复杂性的镜头来研究这些固定参数听话的句子集。我们表明，这样的一组可以是NP-完全的，并考虑从这样的一组句子的有界变量逻辑的翻译所需的长度，我们证明了这个长度的超多项式下界使用可编译性理论，获得一个有趣的类型的公式大小下界。总的来说，本文的工具、概念和结果为将来考虑在表达性更强的逻辑上进行模型检验的复杂性奠定了基础。
2012-07-05 cs.AI cs.CC cs.LO
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard
带有归纳谓词的分离逻辑公式之间的蕴涵，也称为符号堆，已经被证明对于一大类归纳定义是可判定的。最近，提出了一个2-EXPTIME算法，并建立了一个EXPTIME硬界限，但没有精确的下限是已知的。在本文中，我们证明了决定谓词原子之间的蕴涵是2-EXPTIME困难的。证明是基于减少从指数空间有界交替图灵机的成员问题。
2020-04-16 cs.LO
The Complexity of Fragments of Second-Order HyperLTL
本文确定了二阶 HyperLTL 多个片段的可满足性、有限状态可满足性和模型检测的复杂度，指出它们均处于解析层级及更高层级。
2025-09-16 cs.LO
