模差逻辑很难

利用模分解捕获多项式时间

Capturing Polynomial Time using Modular Decomposition

本文提出模分解定理，将图类规范化归约为素图规范化，证明带计数的不动点逻辑捕获置换图类的多项式时间，并表明模分解树及余图识别与规范化可在对数空间计算。

直觉隐含使模型检验困难

Intuitionistic implication makes model checking hard

研究了传递Kripke模型上直觉命题逻辑和模态命题逻辑的模型检验问题的复杂性。更具体地说，我们考虑直觉逻辑IPC，基本命题逻辑BPL，形式命题逻辑FPL和Jankov逻辑KC。我们证明了所有这些直觉逻辑的蕴涵片段的模型检验问题是P-完全的。对于BPL和FPL，我们甚至在只有一个变量的蕴涵片段上也达到了P-困难。对于它们的模态同伴的严格蕴涵片段，得到了相同的硬度结果。此外，我们调查是否公式较少的变量和额外的连接使模型检验更容易。而对于蕴涵片段之外的无变量公式，FPL模型检验被证明是在LOGCFL中，问题仍然是BPL的P-完全。

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

It is known that the satisfiability problems of the product logics K4xS5 and S4xS5 are NEXPTIME-hard and that the satisfiability problem of the logic SSL of subset spaces is PSPACE-hard. We improve these lower bounds for the complexity of these problems by showing that all three problems are EXPSPACE-hard under logspace reduction. In another paper we show that these problems are in ESPACE. This shows that all three problems are EXPSPACE-complete.

线性时间时序逻辑计数模型的复杂性

The Complexity of Counting Models of Linear-time Temporal Logic

我们确定的复杂性计数模型的有界大小的规格表示的线性时间时序逻辑。如果边界是以一元形式给出的，那么计算单词模型是P-完全的;如果边界是以二进制形式给出的，那么计算非确定性多项式空间图灵机的运行次数是一样困难的。如果边界是以一元形式给出的，那么对树模型进行计数就像对非确定性指数时间图灵机的接受运行进行计数一样困难。对于边界的二进制编码，这个问题至少和计算非确定性指数空间图灵机的接受次数一样困难。另一方面，它并不比计数非确定性双指数时间图灵机的接受运行更难。

论初等模态逻辑的复杂性

On the Complexity of Elementary Modal Logics

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