DL-PA和DCL-PC：模型检验和可满足性问题确实在PSPACE中

广义模态可满足性

Generalized Modal Satisfiability

众所周知，模态可满足性是PSPACE完备的（Ladner 1977）。然而，如果我们限制所使用的命题运算符的集合，复杂度可能会降低。请注意，存在无限数量的命题运算符，因为命题运算符只是一个布尔函数。我们对命题算子的每一个有限集合的模态可满足性的复杂性进行了完全分类，即，与以前工作相比，我们对无限数量的问题进行了分类。我们表明，根据命题算子的集合，模态可满足性是PSPACE-完全的，CONP-完全的，或在P.我们得到这个分割不仅为模态公式，但也为他们更简洁的表示使用模态电路。我们考虑了单模态和多模态的情况，并研究了有效性的对偶问题。

一些稠密性模态逻辑的复杂性（扩展版）

Complexity of some modal logics of density (extended version)

本文通过选择性过滤论证和类表方法，分别证明了稠密性单模态逻辑的可满足性问题属于$EXPTIME$，以及弱稠密性双模态逻辑的可满足性问题属于$PSPACE$。

论初等模态逻辑的复杂性

On the Complexity of Elementary Modal Logics

模态逻辑在计算机科学中有着广泛的应用。自20世纪70年代以来，模态可满足性问题的复杂性一直在研究，通常是在逐个案例的基础上证明结果。我们证明了一个非常普遍的分类广泛的一类相关的逻辑：模态逻辑的许多重要的子类可以通过限制允许的模型与一阶霍恩公式。我们证明了这些逻辑的可满足性问题是NP完全的或PSPACE困难的，并展示了一个简单的分类标准。此外，我们证明了许多PSPACE硬逻辑匹配的PSPACE上界。

穷人逻辑的复杂性

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的可满足性问题的复杂性进行了分类，对于算子集的所有其他限制。

具有分级路径模态的CTL * 的可满足性与模型检验

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的所有优点，例如，表达公平的能力。

描述逻辑ALC的广义可满足性

Generalized Satisfiability for the Description Logic ALC

基本描述逻辑ALC中的标准推理问题概念可满足性是PSPACE-完全的，并且在存在无限制公理的情况下是EXPTIME-完全的。ALC的几个片段，特别是FL、EL和DL-Lite家族中的逻辑，有一个更容易的可满足性问题;有时它甚至是易于处理的。我们分类的复杂性标准可满足性问题的所有可能的布尔和量词片段的ALC中存在的一般公理。

树上一阶逻辑二元片段的可满足性

Satisfiability of the Two-Variable Fragment of First-Order Logic over Trees

研究了有限无秩树上一阶逻辑二元片段的可满足性问题。我们使用的签名由一些一元谓词和二元导航谓词child、right sibling以及它们各自的传递闭包组成。我们证明了包含所有这些谓词的逻辑的可满足性问题是EXPSPACE-完全的。此外，我们考虑了结构类对奇异树的限制，即，我们假设在每个节点处恰好有一个一元谓词成立。我们观察到，完整的逻辑，甚至无序树保持有限奇异树的EXPSPACE-完全，但复杂性降低一些较弱的逻辑。也就是说，具有一个二元谓词的逻辑，后代是NEXPTIME-完全的，并且其保护版本是有限奇异树上的PSPACE-完全的，即使这两个逻辑在任意有限树上都是EXPSPACE-完全的。

上下文统一在PSPACE中

Context unification is in PSPACE

语境是带有一个“洞”的术语，即我们可以替换论点的地方。在上下文统一，我们给出了一个方程的条款与变量表示上下文，并询问这个方程的可满足性。上下文统一是二阶统一的一个自然子变量，是不可判定的，同时也是词方程的一个推广，是可判定的。这是这两者之间的独特问题，其可判定性是不确定的（近二十年来）。在本文中，我们证明了上下文统一是在PSPACE。在一阶签名是有限的（通常）假设下，结果成立。这一结果是通过扩展的再压缩技术，最近开发的作者和使用，特别是获得一个新的PSPACE算法满足字方程，上下文统一。重新压缩基于执行简单的压缩规则（替换相邻函数符号对），这些规则（概念上）应用于上下文方程的解，并且以某种方式修改方程，使得实际上可以直接对方程执行这样的压缩步骤，而不知道实际的解。

ALC的子布尔分片可满足性的复杂性

The Complexity of Satisfiability for Sub-Boolean Fragments of ALC

基本描述逻辑ALC中的标准推理问题概念可满足性是PSPACE-完全的，并且在存在无限制公理的情况下是EXPTIME-完全的。ALC的几个片段，特别是FL、EL和DL-Lite家族中的逻辑，有一个更容易的可满足性问题;有时它甚至是易于处理的。所有这些片段都以这样或那样的方式限制了布尔运算符的使用。我们着眼于系统的和更一般的限制的布尔运算符，并建立复杂的概念可满足性问题的存在公理。我们把易处理的和难处理的病例分开。

交互式论证下多主体论证逻辑的复杂性跳跃

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硬逻辑。

有界密度语法逻辑的递归窗口

Recursive windows for grammar logics of bounded density

本文推广有限窗口提出递归窗口方法，研究有界密度多模态逻辑，证明其可满足性问题是 PSPACE-完全的，并证明密度单模态逻辑属于 para-PSPACE。

带一阶前趋分离逻辑的复杂性

The Complexity of Prenex Separation Logic with One Selector

我们首先证明了具有$k\geq1$选择器域的分离逻辑（$\seplogk{k}$）的所有前向列公式的无限可满足性都可以化为有限可满足性。第二，我们表明，这需要的可判定性的有限和无限的可满足性问题的类前向公式的$\seplogk{1}$，减少到一阶理论的一元函数符号和一元谓词符号。我们还证明了复杂性不是初等的，通过减少从一元函数符号的一阶理论。最后证明了$\exists^*\forall^*$语言中带量词前缀的前趋$\seplogk{1}$公式的Bernays-Schönfinkel-Ramsey片段是\pspace -完全的.一个完整的（层次）分类的复杂性前束$\seplogk{1}$的定义，根据量词交替深度是一个悬而未决的问题。

弥补精化模态逻辑复杂性的差距

Closing a Gap in the Complexity of Refinement Modal Logic

精化模态逻辑（Refinement Modal Logic，RML），最近由Bozzelli等人提出，模态逻辑是经典模态逻辑的扩展，它允许人们对变化的模型进行推理。在本文中，我们研究与此逻辑相关的计算复杂性问题，解决了许多悬而未决的问题。具体来说，我们研究的复杂性，满足性的存在片段的RML，Bozzelli，范Ditmarsch和Pinchinat提出的问题。我们的主要结果是一个紧PSPACE上界这个问题，我们通过引入一个新的表系统实现。作为一个直接的后果，我们得到了严格的表征的复杂性RML可满足的任何固定数量的交替的细化量词。此外，通过一个简单的减少，我们建立RML的模型检验问题是PSPACE完全的，即使是一个单一的量词的公式。

关于控制权转移的推理

Reasoning About the Transfer of Control

我们介绍DCL-PC：一种逻辑，用于推理代理人和代理人联盟的能力如何通过将控制权从一个代理人转移到另一个代理人而改变。DCL-PC的逻辑基础是CL-PC，一种推理合作的逻辑，其中代理和代理联盟的能力源于原子布尔变量到单个代理的分布-联盟的选择对应于联盟控制的变量的分配。DCL-PC的基本模型结构是联盟C可以合作带来phi的形式。DCL-PC扩展了CL-PC的动态逻辑模态，其中原子程序的形式是代理i将变量p的控制权交给代理j;与动态逻辑中的常见情况一样，这些原子程序可以使用序列，迭代，选择和测试运算符组合以形成复杂的程序。通过将这种动态转移程序与合作模式相结合，可以推断代理人和联盟的权力如何受到控制权转移的影响。我们给出了两种替代语义的逻辑：一个直接的语义，在其中我们捕获的布尔变量的分布代理;和一个更传统的Kripke语义。我们证明了这些语义是等价的，然后给出了一个公理化的逻辑。我们调查的计算复杂性的模型检验和可满足性的DCL-PC，并表明，这两个问题是PSPACE完全的（因此不差于底层逻辑CL-PC）。最后，我们研究了DCL-PC的控制特性。我们区分一阶控制-代理或联盟通过分配值到代理或联盟控制下的变量来控制某些事务状态的能力-和二阶控制-代理通过将变量转移到其他代理来控制其他代理的能力。我们给出了二阶控制的逻辑刻画。

布尔可满足性的连通性

Connectivity of Boolean Satisfiability

对于布尔可满足性问题，解空间的结构由解图表征，其中顶点是解，并且两个解连通当且仅当它们在一个变量上不同。对于这个隐式定义的图，我们在这里研究st-连通性和连通性问题。基于Gopalan et al.（“The Connectivity of Boolean Satisfiability：Computational and Structural Dichotomies”，2006/2009），我们首先研究了由CSP给出的可满足性问题，更确切地说是由带常数的CNF（S）-公式给出的可满足性问题（如Schaefer在1978年著名的二分法定理中所考虑的）;我们证明了ST-连通性问题的计算二分法，断言它要么在多项式时间内可解，要么是PSPACE-完全的，并且是对齐的结构二分法，断言，连接组件的最大直径是线性的变量的数量，或者可以是指数;此外，我们显示了一个连通性问题的剖分，断言它是在P，CONP-完全，或PSPACE-完全。接下来，我们调查两个重要的变种：CNF（S）-公式没有常数，部分量化的公式;在这两种情况下，我们证明了类似的二分法的ST-连接和直径;对于连接问题，我们显示了一个二分法的情况下，量化的公式，而在没有常数的公式的情况下，我们确定一个可能的二分法的片段。最后，我们考虑B-公式的连通性问题，这是任意嵌套的公式建立从一些固定的连接词集B，和B-电路，这是布尔电路的门是从一些有限…

分次模态逻辑的PSPACE推理

PSPACE Reasoning for Graded Modal Logics

本文给出了一个判定阶化模态逻辑Gr（K_R）可满足性的PSPACE算法，它是命题模态逻辑K_R通过计数表达式的自然推广，在知识表示领域中起着重要作用。该算法采用了tableaux的方法，是第一个已知的算法，满足问题的复杂性下限。因此，我们准确地解决了问题的复杂性，并驳斥了ExpTime-hardness猜想。我们将结果推广到逻辑Gr（K_（R \cap I））上，用逆关系和可达关系的交扩充了Gr（K_R）.这建立了一种“理论基准”，所有算法方法都可以根据它来衡量。

立场线性时态逻辑（Standpoint LTL）的计算复杂度

Computational Complexity of Standpoint LTL

本文分析立场线性时态逻辑SLTL的计算复杂度，证明其可满足性问题为EXPSPACE完全，还提出约束方法得到PSPACE完全的SLTL片段，实现立场逻辑与LTL的低复杂度结合。

n-密集模态逻辑的参数复杂度

Parameterized complexity of n-dense modal logics

本文研究了n-密集模态逻辑的可满足性问题复杂度，通过参数化复杂度分析证明其属于para-PSPACE，并引入递归窗口工具进行扩展。

布尔可满足性的连通性：公式和电路的二分法

The Connectivity of Boolean Satisfiability: Dichotomies for Formulas and Circuits

对于布尔可满足性问题，解空间的结构由解图表征，其中顶点是解，并且两个解连通当且仅当它们在一个变量上不同。2006年，Gopalan等人研究了CSP的解图的连通性和相关的复杂性问题，主要是基于对可满足性算法和可满足性阈值的研究。他们证明了连通分量的直径和st-连通性问题的复杂性的二分法，并为连通性问题建立了一个二分法。最近，我们能够建立切除术[arXiv：1312.4524]。在这里，我们认为可满足性问题的布尔电路和命题公式，使用门，分别定义的连接问题。连接词，从一组固定的布尔函数。我们得到的直径和两个连通性问题的二分法：一方面，直径是线性的变量的数量，这两个问题是在P，而在另一边，直径可以是指数，和问题是PSPACE-完全的。对于部分量化的公式，我们显示了类似的二分法。

重新审视MITL以修复决策程序

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中得到了形式化的证明。

Resource separation in dynamic logic of propositional assignments

We extend dynamic logic of propositional assignments by adding an operator of parallel composition that is inspired by separation logics. We provide an axiomatisation via reduction axioms, thereby establishing decidability. We also prove that the complexity of both the model checking and the satisfiability problem stay in PSPACE.

变论域上一阶模态逻辑的计数量词可判定片段

Decidable fragments of first-order modal logics with counting quantifiers over varying domains

本文探讨了在常数域和变域上，一阶模态逻辑的各种自然单变量片段加上计数量词的计算复杂性。计数量词的加入为我们提供了一种丰富的语言，可以用它来简洁地表达关于满足给定一阶性质的对象的数量的陈述，使用单个变量。最佳NExpTime上界提供的最小一阶模态逻辑QK的一个变量片段的可满足性问题，在恒定和扩大/减少领域模型，计数量词被编码为二进制字符串。对于计数量词被编码为一元字符串的情况下，或被限制为一个有限的量词集，它表明，可满足性问题的扩展域是PSpace完全的，而减少域的问题是ExpTime-hard。

基于团队的CTL变体

A Team Based Variant of CTL

我们介绍了两个变种的计算树逻辑CTL的基础上的团队语义：一个异步的和同步的。对于这两个变种，我们调查的计算复杂性的可满足性以及模型检验问题。可满足性问题被证明是EXPTIME-完全的。在这里，考虑两种语义中的哪一种并不重要。对于模型检验，我们证明了同步情况下的PSPACE-完全性，异步情况下的P-完全性。此外，我们证明了这两种语义的几个有趣的基本属性。

同质性假设下前缀与后缀逻辑是初等的

The Logic of Prefixes and Suffixes is Elementary under Homogeneity

针对同质性假设下区间时序逻辑 BE 的有限可满足性问题，提出有界嵌套模态的等可满足范式，证明其复杂性为 EXPSPACE 完全。

布尔可满足性的连通性：非常数与量化变量

The Connectivity of Boolean Satisfiability: No-Constants and Quantified Variants

对于布尔可满足性问题，解空间的结构由解图表征，其中顶点是解，并且两个解连通当且仅当它们在一个变量上不同。Gopalan等人在Schaefer的框架下，受可满足性和可满足性阈值研究的启发，于2006年研究了解图的连通性和约束满足问题的相关复杂性问题。他们发现了连通分量的直径和st连通性问题的复杂性的二分法，并为我们最近能够证明的连通性问题提出了一个二分法。虽然Gopalan等人考虑了带常数的CNF（S）-公式，但我们在这里研究两个重要的变体：不带常数的CNF（S）-公式和部分量化公式。对于直径和ST-连通性问题，我们证明二分法类似于Gopalan等人。在这些设置。虽然我们还不能给出一个完整的分类的连接问题，我们确定的片段，它是在P，它是coNP完全的，它是PSPACE完全的，在类比Gopalan等人。的脊髓切除术。

逻辑K4xS5和S4xS5的EXPSPACE-完备性与子集空间的逻辑第二部分：EXPSPACE-难性

EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 2: EXPSPACE-Hardness

已知乘积逻辑K4 xS 5和S4 xS 5的可满足性问题是NEXPTIME-困难的，子集空间的逻辑SSL的可满足性问题是PSPACE-困难的。我们提高这些问题的复杂性的下限，表明这三个问题是EXPSPACE-硬下的对数空间减少。在另一篇论文中，我们表明，这些问题是在ESPACE。这表明这三个问题都是EXPSPACE完备的。

Dependency Stochastic Boolean Satisfiability: A Logical Formalism for NEXPTIME Decision Problems with Uncertainty

Stochastic Boolean Satisfiability (SSAT) is a logical formalism to model decision problems with uncertainty, such as Partially Observable Markov Decision Process (POMDP) for verification of probabilistic systems. SSAT, however, is limited by its descriptive power within the PSPACE complexity class. More complex problems, such as the NEXPTIME-complete Decentralized POMDP (Dec-POMDP), cannot be succinctly encoded with SSAT. To provide a logical formalism of such problems, we extend the Dependency Quantified Boolean Formula (DQBF), a representative problem in the NEXPTIME-complete class, to its s…

数据感知混合表aux

Data-Aware Hybrid Tableaux

本文提出了一种用于XPath的数据感知混合表aux演算，证明其正确性、完整性和终止性，并展示了其在多项式空间内的探索能力，确立了该逻辑的可满足性问题为P空间完全。

时序逻辑的同步团队语义

Synchronous Team Semantics for Temporal Logics

本文为LTL和CTL提出团队语义，使其能表达超性质，研究其计算复杂度并证明带有团队语义的LTL是HyperLTL的可行替代方案。

同质性假设下子区间逻辑的可满足性与模型检验

Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption

本文研究子区间逻辑D在齐次性假设下的可满足性与模型检验问题，证明二者在有限结构上均为PSPACE完全，丰富了易处理区间时态逻辑家族。

基于SAT编码的模态和描述逻辑自动推理--以K（m）/ALC可满足性为例

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）。我们提出了一个有效的编码，我们测试了一组广泛的基准，比较的方法与主要的国家的最先进的工具。虽然编码必然是最坏情况下的指数，从我们的实验中，我们注意到，在实践中，这种方法可以处理大多数或所有的问题，这是在其他方法的范围内，与性能相当，甚至更好，那些目前的国家的最先进的工具。

公式大小游戏与模态替换演算的模型检验

Formula size game and model checking for modal substitution calculus

本文通过公式大小游戏研究了MSC及其扩展的表达能力和模型检验复杂度，证明其与图灵机、mu演算等的复杂度关系，并建立了相关逻辑的复杂度分类。

Adding the Relation Meets to the Temporal Logic of Prefixes and Infixes makes it EXPSPACE-Complete

The choice of the right trade-off between expressiveness and complexity is the main issue in interval temporal logic. In their seminal paper, Halpern and Shoham showed that the satisfiability problem for HS (the temporal logic of Allen's relations) is highly undecidable over any reasonable class of linear orders. In order to recover decidability, one can restrict the set of temporal modalities and/or the class of models. In the following, we focus on the satisfiability problem for HS fragments under the homogeneity assumption, according to which any proposition letter holds over an interval if…

命题线性时态逻辑的一种可判定的扩展

A Decidable Timeout based Extension of Propositional Linear Temporal Logic

我们开发了一个基于超时的命题线性时序逻辑扩展（我们称之为TLTL），用于指定基于超时的实时的系统模型的时序特性。TLTL公式明确引用了一个运行的全局时钟以及静态定时变量和一个抽象超时行为的动态变量。我们扩展LTL的能力，表示超时约束。从表现力的观点来看，TLTL不能与包括TPTL、XCTL和MTL的重要的已知的基于时钟的实时逻辑相比，即，TLTL可以指定某些属性，这些属性不能在这些逻辑中指定（反之亦然）。我们定义了一个相应的超时表TLTL公式的可满足性检查。提出了一种基于超时Kripke结构的模型检验算法。此外，我们证明了这种扩展逻辑的有效性检查仍然是PSPACE完全的，即使在存在超时约束和无限状态模型。在离散时间语义下，有界的超时增量，模型检查问题，如果一个TLTL公式成立的超时Kripke结构也是PSPACE完全的。我们进一步证明了当TLTL在离散时间上解释时，它可以嵌入到一元二阶逻辑中，而当TLTL在稠密时间上解释而不满足非顶点条件时，所得到的逻辑是$Σ_1^1$ -完全的.

带求和算子的实数存在性理论

The Existential Theory of the Reals with Summation Operators

本文围绕实数存在性理论引入简洁类 succ-∃R，用非确定性实数 RAM 刻画该类并证明其与 ∃R 分离，同时确定若干逻辑与概率推理问题的完全性，并证明仅添加指数求和所得类 ∃R^Σ 包含于 PSPACE。

模态依赖逻辑的复杂性结果

Complexity Results for Modal Dependence Logic

模态依赖逻辑最近由Väänänen引入。它通过操作符=（）增强了基本模态语言。对于命题变量p_1，.，p_n，=（p_1，...，p_（n-1）;p_n）直观地说明p_n的值由p_1，.，p_（n-1）。Sevenster（J. Logic and Computation，2009）表明，对于非确定性指数时间，模态依赖逻辑的可满足性是完全的。在本文中，我们考虑片段的模态依赖逻辑得到的限制允许命题连接词的集合。我们证明了穷人依赖逻辑的可满足性，这种语言由使用合取、必要性和可能性（即，不允许分离），保持NEXPTIME-完全。如果我们只允许单调公式（没有否定，但有析取），复杂性下降到PSPACE完全性。我们还扩展了Väänänen的语言，允许经典的析取除了依赖析取，并表明可满足性问题仍然是NEXPTIME完全的。如果我们不允许否定和依赖析取，那么对于多项式层次的第二层来说，可满足性是完全的。通过这种方式，我们对Väänänen和Sevenster考虑的命题和依赖运算符的所有限制的可满足性问题的计算复杂性进行了完全分类。

多变量命题线性时间时态逻辑的复杂性

On complexity of propositional Linear-time Temporal Logic with finitely many variables

众所周知[DemriSchnoebelen 02]，命题线性时间时态逻辑LTL的可满足性和模型检查问题，在语言中只有一个命题变量，都是PSPACE完全的，这与LTL的这些问题的复杂性相一致，具有任意数量的命题变量[SislaClarke 85]。在本文中，我们表明，通过修改[SislaClarke 85]中LTL的空间硬度的原始证明，可以得到相同的结果;即，我们展示了如何修改来自[SislaClarke 85]的构造，以仅使用一个变量的公式来模拟多项式空间约束的图灵机的计算。我们相信，我们对[DemriSchnoebelen 02]结果的替代证明提供了对LTL的语义和计算特性的额外见解。

模型检测带立场模态的线性时序逻辑

Model Checking Linear Temporal Logic with Standpoint Modalities

本文提出带立场模态的线性时序逻辑的五种语义及通用模型检测算法，并证明三种情况下问题为PSPACE完全，区别于可满足性的EXPSPACE完全。

论时间均衡逻辑的复杂性

On the complexity of Temporal Equilibrium Logic

时态平衡逻辑（TEL）是一个很有前途的逻辑框架，它利用LTL风格的时态算子扩展了应答集程序设计的知识表示和推理能力。据我们所知，它是第一个完全适应标准时态逻辑（特别是LTL）的语法而不需要进一步构造的非单调逻辑。本文对TEL公式的时间均衡模型的一致性问题进行了系统的复杂性分析。它以前表明，在一般情况下，这个问题位于PSPACE和EXPSPACE之间的某个地方。在这里，我们建立一个下界匹配已知的EXPSPACE上界。此外，我们分析了各种自然的TEL公式子类的复杂性，确定易处理和难处理的片段。最后，本文通过解决极小LTL模型的可满足性问题，对逻辑LTL提供了一些新的见解。得到的复杂性结果突出了解释LTL有限或无限的话之间的实质性差异。

确定性时态逻辑与区间约束

Deterministic Temporal Logics and Interval Constraints

在时态逻辑中，一个中心问题是关于模态的选择及其相对表达能力，与决策问题的复杂性（如可满足性）相比。在本教程中，我们将说明在有限字模型上对此类问题的研究，首先是Schutzenberger最初定义的Unambient Starfree正则语言（UL）的逻辑，然后是带约束的扩展，它出现在区间逻辑中。我们提出了确定性的时间逻辑，与不同的方式，这也表征UL。所使用的工具和技术以“海龟程序”或“排名”的名义进行。这些都是简单的自动机。我们使用的性质，如秩方向性和秩凸性，以显示所有这些逻辑具有NP可满足性。其中一些模态的递归扩展使我们能够在有限线性阶上充分利用一阶逻辑。我们还讨论了区间约束模态扩展确定性时序逻辑，中间的表达。这些允许计数或简单的代数运算的路径。这些扩展逻辑的复杂度是PSpace，就像全时态逻辑一样（当使用二进制表示法时是ExpSpace）。

时间邻域的加入使前缀与子区间逻辑成为 EXPSPACE-完全问题

The addition of temporal neighborhood makes the logic of prefixes and sub-intervals EXPSPACE-complete

本文研究 chop 区间时序逻辑弱化片段 $\mathsf{BD}_{hom}$ 添加时间邻域模态 $A$ 后的扩展，证明所得逻辑 $\mathsf{BDA}_{hom}$ 的可满足性问题为 EXPSPACE-完全，表明该扩展同时提升了表达能力和计算复杂度。

Word equations in linear space

Satisfiability of word equations is an important problem in the intersection of formal languages and algebra: Given two sequences consisting of letters and variables we are to decide whether there is a substitution for the variables that turns this equation into true equality of strings. The exact computational complexity of this problem remains unknown, with the best lower and upper bounds being, respectively, NP and PSPACE. Recently, the novel technique of recompression was applied to this problem, simplifying the known proofs and lowering the space complexity to (nondeterministic) O(n log n…

计算树逻辑中的循环检测

Cycle Detection in Computation Tree Logic

时态逻辑是一种非常强大的形式主义，在形式系统的设计和验证中得到了深入的研究和应用。它的应用通常简化为解决特定的决策问题，如模型检验和可满足性。在这类问题中，解决方案通常需要在循环中检测一些特定的属性。例如，当使用基于自动机、博弈论、SCC分解等的经典技术时，就会发生这种情况。令人惊讶的是，迄今为止，还没有一个时态逻辑被认为具有讨论循环的明确能力。在本文中，我们介绍周期-CTL *，经典的分支时间时序逻辑CTL* 的扩展，随着周期量化，以便在周期上的谓词。这个逻辑非常有表现力。事实上，我们证明，它严格扩展CTL*，是正交的μ演算。我们还提供了一些涉及非正则性质的例子，证明了它的有用性。我们研究了Cycle-CTL* 的模型检验问题，并证明了它和CTL* 一样是PSPACE完备的.我们还研究了逻辑的存在循环片段的可满足性问题，并证明了它在2 ExpTime中是可解的。这一结果利用了自动机理论的方法，以及新的ad-hoc定义的互模拟和树状展开。

判定特征公式：在分支时间谱中的旅程

Deciding characteristic formulae: A journey in the branching-time spectrum

本文研究了在van Glabbeek分支时间谱中各逻辑中判定公式是否为特征公式的问题，分析了可满足性和素性问题的复杂性，并探讨了多项式时间与(co)NP或PSPACE完全问题之间的边界。

单计数器自动机上的有记忆线性时间逻辑的模型检验

Model checking memoryful linear-time logics over one-counter automata

我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。

高表达描述逻辑的实用推理

Practical Reasoning for Very Expressive Description Logics

描述逻辑是一类知识表示形式化体系，其主要特征是构造器从原子概念和角色构造复杂的概念和角色。表达角色构造器在许多应用中很重要，但在计算上可能存在问题。我们提出了一个算法，决定可满足性的DL ALC扩展与传递和逆角色和功能限制方面的一般概念包含公理和角色层次结构，早期的实验表明，该算法是非常适合实施。此外，我们还证明了仅具有传递和逆角色的ALC扩展仍然是PSPACE中的。我们调查这个家庭的DL的可判定性的限制，表明放松限制放置在数量限制中使用的各种角色导致所有推理问题的不可判定性。最后，我们描述了一些优化技术，这是至关重要的，在获得实现的决策过程中，尽管最坏情况下的问题的复杂性，表现出良好的性能与现实生活中的问题。

用于推理聚合-组合图神经网络的逻辑

A Logic for Reasoning About Aggregate-Combine Graph Neural Networks

提出一种计数模态线性不等式的模态逻辑，证明其公式与GNN可互相高效转化，且可满足性为PSPACE完全，支持用逻辑方法推理GNN属性。