Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic
关于模态逻辑的可满足性和有效性问题的复杂性刻画，已有大量的工作。特别地，Ladner证明了K、T和S4之间的所有逻辑的有效性问题是{ \sl PSPACE}-完全的，而对于S5则是{ \sl NP}-完全的。我们表明，在一个精确的意义上，这是\emph{negative introspection}，公理$\neg K p \rimp K \neg K p$，造成的差距。在精确的意义上，如果我们需要这个公理，那么可满足性问题是{ \sl NP}-完全的;没有它，它是{ \sl PSPACE}-完全的。
2006-03-05 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
Satisfiability for Knowing How over Linear Plans is NP-complete
Consejo Nacional de Investigaciones Científicas y Técnicas, CONICET（阿根廷国家科学研究委员会）；Universidad Nacional de Córdoba, FAMAF（科尔多瓦国立大学）；Pontificia Universidad Católica de Chile & IMFD & CENIA（智利天主教 Pontificia 大学）；Universidad Nacional de Río Cuarto（里奥夸尔托国立大学）；Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles（巴黎萨克雷大学）
本文研究了表达knowing-how断言的模态逻辑的可满足性问题，证明了该逻辑的可满足性是NP完全的，改进了已知的复杂性界限。
2026-05-19 cs.LO
A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics
Computing Laboratory（计算实验室）；Oxford University（牛津大学）；School of Computer Science（计算机科学学院）；University of Manchester（曼彻斯特大学）
本文研究了分级模态逻辑在自反性、序列性、对称性、传递性和欧几里得性等不同组合框架类上的可满足性问题，并为其获得了紧致的复杂性界限。
2009-05-19 cs.AI cs.CC cs.LO
Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
在过去的二十年中，模态和描述逻辑已被应用于计算机科学的许多领域，包括知识表示，形式化验证，数据库理论，分布式计算，以及最近的语义Web和本体。基于这个原因，模态逻辑和描述逻辑中的自动推理问题得到了深入的研究。特别地，已经提出了许多方法来有效地处理核心正规模态逻辑K（m）及其记法变体描述逻辑ALC的可满足性。虽然K（m）/ALC结构简单，但在计算上很难推理，它的可满足性是PSPACE完全的。在本文中，我们开始探索的想法，执行自动推理任务的模态和描述逻辑编码成SAT，以便处理的国家的最先进的SAT工具，与大多数以前的方法，我们开始我们的调查从满足性K（m）。我们提出了一个有效的编码，我们测试了一组广泛的基准，比较的方法与主要的国家的最先进的工具。虽然编码必然是最坏情况下的指数，从我们的实验中，我们注意到，在实践中，这种方法可以处理大多数或所有的问题，这是在其他方法的范围内，与性能相当，甚至更好，那些目前的国家的最先进的工具。
2014-01-15 cs.AI cs.LO
How Easy it is to Know How: An Upper Bound for the Satisfiability Problem
针对基于线性计划语义的“知道如何”模态逻辑，本文通过消除嵌套模态并调用命题逻辑可满足性预言机，证明其公式可满足性检查属于 $Σ_2^P$。
2023-09-29 cs.LO
Complexity of some modal logics of density (extended version)
本文通过选择性过滤论证和类表方法，分别证明了稠密性单模态逻辑的可满足性问题属于$EXPTIME$，以及弱稠密性双模态逻辑的可满足性问题属于$PSPACE$。
2025-07-15 cs.LO
The Parameterized Complexity of Reasoning Problems Beyond NP
今天的命题可满足性（SAT）求解器非常强大，可以用作解决NP完全问题的有效后端。然而，知识表示和推理中的许多基本问题位于多项式层次的第二层或更高层，因此多项式时间变换到SAT是不可能的，除非层次崩溃。最近的研究表明，在某些情况下，可以突破这些复杂性障碍的固定参数易处理（fpt）减少利用问题实例的结构方面的问题参数。在本文中，我们开发了一个一般的理论框架，支持分类的参数化问题，他们是否承认这样的FPT减少SAT或不。该框架基于几个新的参数化复杂性类。作为一个运行的例子，我们使用的框架来分类的复杂性的析取答案集编程的一致性问题，相对于各种自然参数。我们支持我们的理论的鲁棒性提供了一个新的复杂性类加权QBF可满足性，交替图灵机，和一阶模型检验的表征。此外，我们提供了一个纲要的参数化问题，是完整的新的复杂性类，包括相关的知识表示和推理，逻辑和组合学的问题。
2016-07-01 cs.CC cs.DS cs.LO
The Inverse Method Implements the Automata Approach for Modal Satisfiability
基于表格的模态和描述逻辑的可满足性判定过程在实践中表现得很好，但有时很难使用这些方法获得精确的最坏情况复杂度结果，特别是对于EXPTIME完全逻辑。相比之下，基于自动机的方法通常产生的算法，最佳的最坏情况下的复杂性可以很容易地证明。然而，这种方法得到的算法通常不仅是最坏情况，而且是最好情况的指数：它们首先构造一个在输入大小上总是指数的自动机，然后对这个大型自动机应用（多项式）空性测试。为了克服这个问题，必须尝试在执行空性测试的同时“动态”构建自动机。在本文中，我们将表明，模态逻辑K的Voronkov逆方法可以被看作是由K的自动机方法完成的空性测试的即时实现。这一结果的好处是双重的。首先，它表明，Voronkov的实现的逆方法，这在实践中表现得很好，是一个优化的基于自动机的可满足性过程的飞行实现K。第二，它可以用来给一个简单的证明的事实，Voronkov的优化不破坏完整的过程。我们还将表明，逆方法可以很容易地扩展到处理全球公理，并且在这种设置下，自动机方法的对应关系仍然成立。特别是，逆方法产生一个EXPTIME算法满足K w.r.t.全局公理
2004-12-22 cs.LO
A Simple Probabilistic Extension of Modal Mu-calculus
概率系统是人工智能领域的一个重要课题。作为规约语言，逻辑PCTL现在是概率属性推理的默认逻辑。在本文中，我们提出了一个自然和简洁的概率扩展μ演算，另一个突出的逻辑在并发理论。我们研究了与PCTL的关系。有趣的是，表现力与PCTL高度正交。所提出的逻辑捕获了一些有用的属性，不能在PCTL中表示。研究了模型检验和可满足性问题，证明了模型检验问题是UP和co-UP问题，可满足性检验可以归结为求解奇偶对策问题.这也与PCTL相反，PCTL的可满足性检查仍然是一个悬而未决的问题。
2015-05-08 cs.LO
Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities
我们提出了一个简单的理论解释的建设和正确性的增量和最坏情况下的模态逻辑的最佳决策过程与不测。该程序给出了一个抽象的重要方面的Goré和Widmann的PDL证明。从一个输入公式开始，该过程会生成一个Pratt样式的图形表，直到该表证明或否定该公式的可满足性。该程序提供了一个基础，实际证明，因为可满足性和不可满足性的公式，往往可以确定与小tableaux。
2012-09-06 cs.LO
Complexity results for modal logic with recursion via translations and tableaux
本文通过逻辑间翻译迁移复杂性结果，为带递归的多智能体模态逻辑构建表列系统并将其可满足性归约为μ-演算可满足性，得到通用2EXP上界。
2024-08-06 cs.LO
Non-Normal Modal Description Logics (Extended Version)
该研究提出一族扩展ALC语言的非正规模态描述逻辑，提供变域下NExpTime复杂度的表算法框架，给出部分系统到常域关系模型的归约，并证明限制模态算子应用片段的ExpTime紧复杂度。
2023-07-23 cs.LO
Better algorithms for satisfiability problems for formulas of bounded rank-width
针对命题模型计数问题#SAT，给出了一个参数化多项式算法，其运行时间在公式的秩宽度上是单指数的。以前，类似的算法是已知的--例如~ [Fischer，Makowsky，and Ravve] --对公式的宽度具有单指数依赖性。因此，我们的算法提出了一个指数级的运行时间的改善（因为ck-width达到指数级更高的值比rank-width），并可以为小值的rank-width的实际利益。我们还提供了一个算法的MAX-SAT问题沿着相同的路线。
2010-06-29 cs.DM cs.LO
Satisfiability and computing van der Waerden numbers
在本文中，我们汇集了组合学和命题可满足性领域。许多组合定理建立，往往建设性地，正整数函数的存在性，而实际上没有提供其封闭的代数形式或严格的上下界。拉姆齐理论的领域在这类结果中特别丰富。以计算范德瓦尔登数的问题为例，我们证明了这些问题可以用参数化命题理论来表示，这样，关于它们的可满足性的决定就决定了问题中的数（函数）。我们表明，通过使用通用的完整和本地搜索技术测试命题可满足性，这种方法变得有效-竞争与专门的方法。通过跟踪它，我们能够获得几个新的结果有关的问题计算范德瓦尔登数。我们还注意到，由于它们的属性，特别是它们的结构简单性和计算难度，在这项研究中出现的命题理论可以用于SAT求解器的开发，测试和基准测试。
2003-10-31 cs.LO
MaxSAT with Absolute Value Functions: A Parameterized Perspective
布尔可满足性问题到最优化问题的自然推广是确定在合取范式中的命题公式中可以同时满足的子句的最大数量的任务。在加权最大可满足性问题中，每个子句都有一个正的权重，并寻求最大权重的分配。文献几乎只考虑了正权重的情况。虽然一般情况下的问题只受到这个约束的轻微限制，但许多特殊情况在没有负权重的情况下变得微不足道。在这项工作中，我们研究了具有负权重的问题，并观察到该问题在计算上变得更加困难-我们从参数化的角度将其形式化，因为如果存在负权重，则该问题的各种变体变得W[1]-困难。允许负权重也引入了问题的新变体：我们可以最大化该和的绝对值，而不是最大化满足子句的权重之和。这被证明是令人惊讶的表达，甚至仅限于在析取范式，每个子句最多两个文字的单调公式。然而，在没有绝对值的版本相比，我们证明，这些变种是固定参数听话。作为技术上的贡献，我们提出了一个核化的一个辅助问题，在超图中，我们寻求，给定一个边加权超图，诱导子图，最大化的绝对值的总和边权重。
2022-04-26 cs.CC cs.DS cs.LO
On the Complexity of Elementary Modal Logics
模态逻辑在计算机科学中有着广泛的应用。自20世纪70年代以来，模态可满足性问题的复杂性一直在研究，通常是在逐个案例的基础上证明结果。我们证明了一个非常普遍的分类广泛的一类相关的逻辑：模态逻辑的许多重要的子类可以通过限制允许的模型与一阶霍恩公式。我们证明了这些逻辑的可满足性问题是NP完全的或PSPACE困难的，并展示了一个简单的分类标准。此外，我们证明了许多PSPACE硬逻辑匹配的PSPACE上界。
2008-02-13 cs.CC cs.LO
Canonical Models and the Complexity of Modal Team Logic
该研究通过引入典范模型将模态团队逻辑MTL的可满足性简化为模型检验，并证明其复杂性为TOWER(poly)完全问题，同时刻画了有界模态深度片段的初等层级复杂性。
2019-04-10 cs.LO
A Parameterized Complexity View on Description Logic Reasoning
Institute for Logic, Language and Computation（逻辑、语言与计算研究所）；University of Amsterdam（阿姆斯特丹大学）
描述逻辑是一种知识表示语言，它被设计成在表达性和计算易处理性之间取得平衡。许多不同的描述逻辑已经被开发出来，并且这些逻辑的许多计算问题由于它们的计算复杂性而被研究。然而，基本上所有的复杂性分析的推理问题的描述逻辑使用的经典复杂性理论的一维框架。参数化复杂性理论的多维框架能够提供推理问题复杂性的更详细的图像。在本文中，我们认为，参数化复杂性的框架有很多可以提供的描述逻辑推理问题的复杂性分析-当一个人需要一个渐进的和前瞻性的观点参数化的复杂性工具。我们通过三个案例研究来证实我们的论点。第一个案例研究的问题是概念可满足的逻辑ALC关于近无环的TBox。第二个案例研究关注ALC概念的可满足性，其参数由联合算子的出现次数和完全存在量化的出现次数来确定。第三个案例研究从参数化复杂性的角度对数据复杂性结果进行了批判性的审视。这三个案例研究代表了描述逻辑问题的参数化复杂性方法的广泛应用。
2018-08-11 cs.AI cs.CC cs.LO
Undecidability of a Very Simple Modal Logic with Binding
我们展示了什么可以说是最简单的非子布尔模态逻辑的约束力的隐式概念的可满足性问题的不可判定性。这一工作丰富了从混合逻辑到记忆逻辑的关于模态逻辑不可判定性的一系列已有结果。
2015-08-14 cs.LO
On the Satisfiability of Local First-Order Logics with Data
本文研究带数据一阶逻辑的可满足性问题，提出局部片段限制量化范围，证明半径-1片段可判定而更大半径不可判定，并给出存在片段完整的可判定性与复杂性图景。
2024-07-01 cs.LO
The Undecidability of Arbitrary Arrow Update Logic
Arbitrary Arrow Update Logic是一种动态模态逻辑，它使用任意箭头更新模态来量化所有箭头更新。这种逻辑的一些性质已经被确定，但直到现在，它仍然是一个开放的问题，是否逻辑的可满足性问题是可判定的。在这里，我们证明了任意箭头更新逻辑的可满足性问题是co-RE硬的，因此不可判定的，通过减少平铺问题。
2016-09-19 cs.LO
Decidable fragments of first-order modal logics with counting quantifiers over varying domains
本文探讨了在常数域和变域上，一阶模态逻辑的各种自然单变量片段加上计数量词的计算复杂性。计数量词的加入为我们提供了一种丰富的语言，可以用它来简洁地表达关于满足给定一阶性质的对象的数量的陈述，使用单个变量。最佳NExpTime上界提供的最小一阶模态逻辑QK的一个变量片段的可满足性问题，在恒定和扩大/减少领域模型，计数量词被编码为二进制字符串。对于计数量词被编码为一元字符串的情况下，或被限制为一个有限的量词集，它表明，可满足性问题的扩展域是PSpace完全的，而减少域的问题是ExpTime-hard。
2018-12-15 cs.LO
On the satisfiability problem for a 3-level quantified syllogistic
我们证明了一个集合的三个排序集理论公式，表示TLQSR，并承认一个限制形式的量化个人和集合变量，有一个可解的可满足性问题，证明它享有一个小的模型属性，即，任何可满足的TLQSR公式psi都有一个有限模型，其大小仅取决于psi本身的大小。我们还引入了TLQSR的子语言（TLQSR）^h，其公式的特征是具有长度以h \geq 2为界的量词前缀和其他一些句法约束，并证明了它们都具有NP-完全的可满足性问题.然后，我们证明了模态逻辑S5可以在（TLQSR）^[3]中形式化。
2013-04-08 cs.LO
Parameterized complexity of n-dense modal logics
University of Toulouse - IRIT - CNRS（图卢兹大学 - IRIT - 法国国家科学研究中心）
本文研究了n-密集模态逻辑的可满足性问题复杂度，通过参数化复杂度分析证明其属于para-PSPACE，并引入递归窗口工具进行扩展。
2026-04-13 cs.LO
Problems parameterized by treewidth tractable in single exponential time: a logical approach
我们介绍了模态逻辑的一个变体，称为存在计数模态逻辑（ECML），它捕获了绝大多数已知的问题是易处理的单指数时间时，参数化树宽。看来，所有这些结果可以被包含的定理，模型检验的ECML承认一个算法具有这样的复杂性。我们通过添加连接性要求扩展了ECML，并使用Cygan等人引入的Cut&Count技术。[4]，证明了当用树宽参数化时，扩展中可表达的问题在单指数时间内也是易处理的;然而，使用随机化。本文证明了所引入的逻辑的导航性的必要性，并给出了一个否定的结果：除非指数时间假设失效，否则涉及非非循环条件的两个基本问题C_1顶点删除和GIRTH> 1顶点删除（l>=5）不允许这样一个鲁棒的算法。
2011-04-15 cs.DS cs.LO
Closing a Gap in the Complexity of Refinement Modal Logic
精化模态逻辑（Refinement Modal Logic，RML），最近由Bozzelli等人提出，模态逻辑是经典模态逻辑的扩展，它允许人们对变化的模型进行推理。在本文中，我们研究与此逻辑相关的计算复杂性问题，解决了许多悬而未决的问题。具体来说，我们研究的复杂性，满足性的存在片段的RML，Bozzelli，范Ditmarsch和Pinchinat提出的问题。我们的主要结果是一个紧PSPACE上界这个问题，我们通过引入一个新的表系统实现。作为一个直接的后果，我们得到了严格的表征的复杂性RML可满足的任何固定数量的交替的细化量词。此外，通过一个简单的减少，我们建立RML的模型检验问题是PSPACE完全的，即使是一个单一的量词的公式。
2013-09-20 cs.CC cs.LO
NP Reasoning in the Monotone $μ$-Calculus
单调模态逻辑的可满足性检验是NP完全的。我们表明，这仍然是真实的逻辑时，扩展与conjunctive和交替自由不动点算子以及通用模态;由此产生的逻辑-conjunctive交替自由单调$μ$ -演算与通用模态-包含并发命题动态逻辑（CPDL）和交替自由片段的游戏逻辑片段。我们得到了我们的结果，通过多项式多Eloise节点的Büchi游戏的可满足性的表征。
2020-05-04 cs.FL cs.GT cs.LO
The Complexity of Satisfiability for Fragments of Hybrid Logic -- Part I
混合逻辑的可满足性问题是不可判定的。这引发了一个关于可判定和可处理片段的研究计划。在本文中，我们调查的影响，限制命题部分的语言的可判定性和可满足性问题的复杂性在任意的，传递的，总的框架，框架的基础上的等价关系。我们还考虑了不同的模态和混合算子。我们跟踪边界的可判定性，并给出了精确的复杂性，大多数片段，特别是包括否定的所有片段。对于单调片段，我们能够区分容易的情况下，从困难的情况下，这取决于允许的一组操作。
2009-06-08 cs.CC cs.LO
A Simplest Undecidable Modal Logic
模态逻辑在计算机科学中有着广泛的应用。自20世纪70年代以来，它们的可满足性问题的复杂性一直是一个活跃的研究领域。我们证明，即使是非常“简单”的模态逻辑可以是不可判定的：我们表明，有一个不可判定的模态逻辑，可以通过限制允许的模型与一阶公式，其中只有全称量词出现。
2011-05-04 cs.CC cs.LO
Parameterized Complexity of CTL: A Generalization of Courcelle's Theorem
我们提出了一个几乎完整的分类的可满足性问题的计算树逻辑CTL的所有操作符片段的参数化复杂性。研究的参数化是时间深度和结构路径宽度的总和。分类显示了W[1]-硬和固定参数易处理片段之间的二分法。FPT中唯一被证实的真正的操作符片段是仅包含AX的片段。此外，我们证明了一个推广的Courcelle定理的无限签名，这将被用来证明FPT成员的情况。
2015-03-24 cs.CC cs.LO
The Complexity of Poor Man's Logic
受描述逻辑的启发，我们研究了如果我们只允许从字面量、$\wedge$、$\Diamond$和$\Box$构建公式，模态可满足性问题的复杂性会发生什么。以前，唯一已知的结果是K的可满足性问题的复杂性从PSPACE完全下降到coNP完全（Schmidt-Schauss和Smolka，1991和Donini等人，1992年）。在本文中，我们表明，不是所有的模态逻辑的行为像K。特别是，我们表明，可满足性问题的复杂性，其中每个世界至少有一个继任者的帧下降PSPACE-完整的P，但相比之下，可满足性问题的类的帧中，每个世界最多有两个继任者仍然PSPACE-完整的。作为后者的结果的推论，我们也解决了开放的问题，从Donini等人。描述逻辑的复杂性分类（Donini等人，1997年）。在最后一节中，我们对K的可满足性问题的复杂性进行了分类，对于算子集的所有其他限制。
2005-12-24 cs.CC cs.LO
Reasoning about Strategies: on the Satisfiability Problem
策略逻辑（Strategy Logic，简称SL）是由Mogavero、Murano和Vardi提出的一种有用的形式主义，用于在多智能体并发游戏中明确地推理策略（作为一阶对象）。这种逻辑被证明是非常强大的，包含了所有主要的先前研究的模态逻辑的战略推理，包括ATL，ATL* 等。不幸的是，由于其高表达性，SL具有非基本可判定的模型检查问题，并且可满足性问题是不可判定的，特别是Sigma_1^1。为了得到一个可判定的子逻辑，本文引入并研究了单目标策略逻辑（SL[1G]，简称SL[1G]）。这是SL的一个语法片段，严格地包含ATL*，它包含了前束范式中的公式，每次有一个单一的时间目标，对于每个策略量化的代理。我们证明了SL[1G]与SL不同，SL[1G]具有有界树模型性质，并且它的可满足性问题在2ExpTime中是可判定的，因此并不比ATL* 的可满足性问题难.
2017-03-16 cs.LO
Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?
本文研究树语义下带命题量词的模态与时态逻辑的复杂性，证明限制于EX的tQCTL已是Tower困难，并在N有界树上为AExpPol完全，同时推广到多种模态逻辑。
2022-08-04 cs.LO
The Logic of Prefixes and Suffixes is Elementary under Homogeneity
针对同质性假设下区间时序逻辑 BE 的有限可满足性问题，提出有界嵌套模态的等可满足范式，证明其复杂性为 EXPSPACE 完全。
2023-04-22 cs.LO
A Modal Logic for Explaining some Graph Neural Networks
Université de Rennes（雷恩大学）
本文提出一种计数模态出现在线性不等式中的模态逻辑，并证明其与图神经网络可互相转换，且可满足性问题可判定，部分变体属于PSPACE。
2023-07-11 cs.AI cs.LO
Parameterised Complexity of Propositional Inclusion and Independence Logic
本文系统研究命题包含逻辑与独立性逻辑中模型检查和可满足性的参数化复杂性，表明多数参数化下问题处于 FPT 或为 paraNP 完全。
2023-07-13 cs.CC cs.LO
PSPACE Reasoning for Graded Modal Logics
本文给出了一个判定阶化模态逻辑Gr（K_R）可满足性的PSPACE算法，它是命题模态逻辑K_R通过计数表达式的自然推广，在知识表示领域中起着重要作用。该算法采用了tableaux的方法，是第一个已知的算法，满足问题的复杂性下限。因此，我们准确地解决了问题的复杂性，并驳斥了ExpTime-hardness猜想。我们将结果推广到逻辑Gr（K_（R \cap I））上，用逆关系和可达关系的交扩充了Gr（K_R）.这建立了一种“理论基准”，所有算法方法都可以根据它来衡量。
2000-05-08 cs.AI cs.CC cs.DS
Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption
本文研究子区间逻辑D在齐次性假设下的可满足性与模型检验问题，证明二者在有限结构上均为PSPACE完全，丰富了易处理区间时态逻辑家族。
2022-01-31 cs.FL cs.LO
Reasoning about Strategic Abilities in Stochastic Multi-agent Systems
本文提出概率交替时间μ演算PAMC用于随机多智能体系统策略能力推理，证明其复杂度性质并给出模型检测与可满足性检测算法，实现为开源工具且验证了有效性。
2024-12-12 cs.FL cs.GT cs.LO
From $μ$-Calculus to Alternating Tree Automata using Parity Games
$μ$ -无限树上的微积分和自动机是描述无限树语言的互补方式。利用$μ$ -Calculus与交替树自动机之间的对应关系，将模式$μ$ -Calculus公式编译成交替树自动机，解决了可满足性和模型检验问题.因此提倡一个自动机模型，专门为工作模式$μ$ -微积分。与Janin和Walukiewicz提出的自动机模型相比，自动机模型的优点是能够以更简单的方式处理任意分支。这两个问题（即，模型检验和可满足性）分别通过约简到交替树自动机的相应问题，即接受问题和非空问题来解决。这些问题，反过来，解决使用奇偶性游戏的语义交替树自动机被翻译成一个获胜的战略，在一个适当的奇偶性游戏。
2016-02-02 cs.FL cs.LO
Bridging the gap between modal temporal logics and constraint-based QSR as an ALC(D) spatio-temporalisation with weakly cyclic TBoxes
这项工作的目的是提供一个家庭的空间变化的定性理论，特别是空间场景的运动。为了实现这一点，我们考虑一个时空MTALC（D_x），著名的ALC（D）家族的描述逻辑（DL）与具体domanan。具体地说，具体域D_x由定性空间关系代数（RA）x生成。通过将MTALC（D_x）概念的可满足性归结为空间约束增强的弱交替自动机的空性问题，我们证明了MTALC（D_x）概念关于弱循环TBox的可满足性在非确定指数时间内是可判定的，尽管游程的接受条件除了标准情况外，CSP（约束满足问题）的一致性可能是无限的。结果提供了一个有效的表格式可满足性过程进行了讨论。
2003-07-17 cs.AI cs.LO
Computational Complexity of Standpoint LTL
本文分析立场线性时态逻辑SLTL的计算复杂度，证明其可满足性问题为EXPSPACE完全，还提出约束方法得到PSPACE完全的SLTL片段，实现立场逻辑与LTL的低复杂度结合。
2024-08-16 cs.LO
On the Parallel Parameterized Complexity of MaxSAT Variants
在最大可满足性问题（MAX-SAT）中，我们给出了一个合取范式的命题公式，并且必须找到一个满足尽可能多子句的赋值。我们研究了并行参数化的复杂性的各种版本的MAX-SAT和提供第一个常数时间的算法参数化的解决方案的大小或允许的超额相对于一些保证（“以上保证”版本）。对于双参数化版本的参数是我们允许离开不满足的条款的数量，我们提出了第一个并行算法MAX-2SAT（称为ALMOST-2SAT）。并行求解ALMOST-2SAT的困难来自于这样一个事实，即最初开发的迭代压缩方法是为了证明该问题是固定参数易于处理的，它本质上是顺序的。我们观察到，一个图流的值是一个参数，可以并行计算，并使用这一事实开发一个并行算法的顶点覆盖问题参数化以上的大小一个给定的匹配。最后，我们研究了MAX-SAT的并行复杂度，参数包括顶点覆盖数、树深、反馈顶点集数和输入关联图的树宽。虽然MAX-SAT是固定参数的所有这些参数听话，我们表明，它们允许不同程度的可能的并行化。对于所有四个，我们开发专用的并行算法是建设性的，这意味着他们输出一个最佳的分配-在对比的结果，可以通过并行元定理，往往只解决决策版本。
2022-06-02 cs.CC cs.LO
Decidability and Undecidability Results for Propositional Schemata
CNRS（法国国家科学研究中心）
我们定义了一个逻辑的命题公式图式添加到语法的命题逻辑索引命题和迭代连接词范围内的算术变量参数化的区间。可满足性问题是不可判定的，这个新的逻辑，但我们引入了一个非常一般的类的模式，称为有界线性，这个问题变得可判定。这个结果是通过减少到一个特定的类称为定期的模式，我们提供了一个健全的和完整的终止证明过程。这种模式演算允许一个捕获证明模式对应于一个大类的命题逻辑中指定的问题。我们还表明，可满足性问题再次成为不可判定的轻微扩展这一类，从而表明，有界线性模式代表了一个很好的妥协之间的表达性和可判定性。
2014-01-16 cs.AI cs.LO
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
UCLID 5是一个多模态形式化建模、验证和系统综合的工具。它使人们能够解决异构系统的验证问题，如硬件和软件的组合，或那些有多个，不同的规格，或系统，需要混合模式的建模。\uclid的一个新方面是强调使用语法引导和归纳综合来自动化建模和验证步骤。本文介绍了\uclid工具的新发展，包括新的语言功能，集成与新技术的语法指导合成和可满足性解决，支持hyperproperties和组合的公理和操作建模，演示新的问题类，和一个强大的实现。
2022-08-07 cs.LO
The Modal Logic of Stepwise Removal
我们调查模态逻辑的逐步删除的对象，既为它的内在利益作为一个逻辑的量化没有替换，并作为一个试点研究，以更好地了解动态认知逻辑的模型转换和逻辑的自由选择的图形变化，得到登记在不断增长的内存之间的复杂性跳跃。在介绍了这种逻辑（$\textsf{MLSR}$）及其相应的移除模态之后，我们分析了它的表达能力，并证明了一个互模拟特征定理。然后，我们提供了一个完整的希尔伯特式公理化的逻辑逐步删除的混合语言丰富的名词和公告运营商。接下来，我们证明了$\textsf{MLSR}$的模型检测是PSPACE完备的，而它的可满足性问题是不可判定的。最后，我们考虑一个精细结构的问题：通过将逐步移除模态添加到一阶逻辑片段中获得的表达能力。
2021-03-08 cs.LO math.LO
The Triguarded Fragment
University of Wrocław（弗罗茨瓦夫大学）；TU Dresden（德累斯顿工业大学）；ScaDS.AI Dresden/Leipzig（德累斯顿/莱比锡数据科学与工程中心）；TU Wien（维也纳工业大学）
该研究结合一阶谓词逻辑的守卫片段与两变量片段，提出三元守卫片段TGF，证明其可满足性问题在特定条件下的复杂度，且具有有限模型性质，为相关逻辑研究提供新的可判定片段。
2026-08-04 cs.LO
When Symmetry Yields NP-Hardness: Affine ML-SAT on S5 Frames
Universität Tübingen（蒂宾根大学）；Leibniz Universität Hannover（汉诺威莱布尼茨大学）
本文证明了在S5框架下，受限于XOR和1连接词的仿射ML-SAT问题为NP难性。
2025-12-19 cs.CC cs.LO
Complexity Jumps In Multiagent Justification Logic Under Interacting Justifications
证明逻辑（英语：Logic of Proofs），LP，及其后继者，证明逻辑（英语：Justification Logic），是模态逻辑对认识论方法的一种改进，其中考虑了证明/证明。在2000年，库兹涅茨证明了LP的可满足性是在多项式层次的第二层，这一结果已经成功地重复了所有其他单智能体证明逻辑的复杂性是已知的。我们引入了一个家庭的多代理的理由逻辑与代理之间的相互作用的理由，通过扩展和推广的两个代理版本的证明的逻辑Yavorskaya在2008年。对于这种多代理的情况，调整了来自单代理调整设置的已知概念和工具。我们目前的Tableau规则和一些初步的复杂性结果。在某些情况下，这些逻辑的可满足性问题仍然在多项式层次的第二层，而对于其他人来说，它是PSPACE或EXP-hard。此外，这个问题变得PSPACE硬，即使某些两个代理逻辑，而有三个代理的EXP硬逻辑。
2014-04-26 cs.LO
The decision problem of modal product logics with a diagonal, and faulty counter machines
在二变量一阶逻辑的命题模态（和代数）处理中，等式由“对角”常数建模，在通用框架的平方积中解释为恒等（也称为“对角”）关系。在这里，我们研究的决定问题的产品的两个任意模态逻辑配备这样的对角线。由于二元一阶逻辑中等式的存在或不存在并不影响其可满足性问题的复杂性，因此人们可能会认为，在一般的乘积逻辑中添加对角线也是无害的。我们证明，情况远非如此，复杂性可能会有相当大的跳跃，甚至从可判定到高度不可判定。我们的不可判定逻辑也可以被看作是一阶逻辑的新片段，其中添加等式将可判定片段改变为不可判定。我们证明了我们的结果的一个新的应用计数器机的问题。虽然我们的形式主义显然不能直接强制可靠的计数器机器计算，但模型中唯一对角线的存在使得有可能对相同指令序列的有损和插入错误计算进行编码。我们表明，给定这样一对错误的计算，就有可能根据它们重建可靠的运行。
2015-09-07 cs.LO
A Logic of "Black Box" Classifier Systems
针对机器学习二分类器的黑箱不透明性，本文提出乘积模态逻辑PLC，将黑箱解释为分类器集合上的不确定性，并给出公理化、可满足性复杂性结果及支持信息更新的动态扩展。
2024-03-01 cs.LO
Adding the Relation Meets to the Temporal Logic of Prefixes and Infixes makes it EXPSPACE-Complete
在表达性和复杂性之间选择正确的折衷是区间时态逻辑的主要问题。在他们的开创性论文中，Halpern和Shoham表明HS（艾伦关系的时序逻辑）的可满足性问题在任何合理的线性序类上都是高度不可判定的。为了恢复可判定性，可以限制时间模态的集合和/或模型的类别。在下文中，我们专注于HS片段在同质性假设下的可满足性问题，根据该假设，任何命题字母在区间上成立，如果它在所有点上成立。具有齐次性的完全HS问题已经被证明是非初等可判定的，但它唯一已知的下界是EXPSPACE（事实上，对于前缀和后缀BE的逻辑已经证明了EXPSPACE-困难，这是它的一个非常小的片段。本文证明了将Allen关系Meets加到BD上使BD成为EXPSPACE完备的。
2021-09-17 cs.LO
Deciding characteristic formulae: A journey in the branching-time spectrum
Reykjavik University（雷克雅未克大学）；Gran Sasso Science Institute（格兰萨索科学研究所）
本文研究了在van Glabbeek分支时间谱中各逻辑中判定公式是否为特征公式的问题，分析了可满足性和素性问题的复杂性，并探讨了多项式时间与(co)NP或PSPACE完全问题之间的边界。
2026-03-26 cs.LO
