EXPSPACE-Completeness of the Logics K4xS5 and S4xS5 and the Logic of Subset Spaces, Part 1: ESPACE-Algorithms

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.

On the freeze quantifier in Constraint LTL: decidability and complexity

Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, logics with lambda-abstraction etc.). We show that Constraint LTL over the simple domain (N,=) augmented with the freeze quantifier is undecidable which is a surpri…

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

Computational Complexity of Standpoint LTL

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

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

The Existential Theory of the Reals with Summation Operators

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