paperbot · PL 论文追踪

全部论文 待读 收藏

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

时序邻域算子的加入使前缀与子区间逻辑变为 EXPSPACE-完全
LMCS vol.Volume 20, Issue 12024匹配度 1/10 · 该论文研究区间时序逻辑的复杂度,属于纯逻辑与自动机理论,未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析。虽然与形式化验证的逻辑基础有微弱关联,但与用户当前追的核心问题几乎没有直接交集。引用 0 inbox
L. Bozzelli, A. Montanari, A. Peron, P. Sala
crossref: 2026-09-10

AI 速览

一句话:证明在 BD_hom 中加入对应 Allen 关系 Meets 的时序邻域模态 A 后,所得 BDA_hom 的可满足性为 EXPSPACE-完全。

Stockmeyer 关于无星广义正则表达式非空性的非初等下界,与区间时序逻辑(尤其 chop 算子)的可满足性密切相关:chop 可视为正则语言连接的逆,homogeneous 假设下二者可相互归约。本文研究 chop 区间时序逻辑的弱化片段,它们等价于 Halpern–Shoham 区间逻辑片段。作者先考察含 B(begins)和 D(during)的 BD_hom,其 homogeneous 模型对应带并、补及前缀/中缀逆的受限正则语言,已知为 PSPACE-完全。再加入对应 Allen 关系 Meets 的时序邻域模态 A 后,表达力与复杂度均提高,BDA_hom 可满足性被证明为 EXPSPACE-完全。

问题
在 homogeneous 假设下,确定区间时序逻辑片段 BD_hom 及其加入时序邻域模态 A 后的扩展 BDA_hom 的可满足性复杂度与表达力关系。
方法
利用 chop 与正则连接、B/D/A 与前缀、中缀、Meets 关系的对应,将逻辑片段与受限正则语言联系起来并进行复杂度归约分析。
评估
通过可满足性复杂度的下界与上界证明 BDA_hom 是 EXPSPACE-完全,并与 BD_hom 已知的 PSPACE-完全性对比,表明表达力与复杂度均提升。
原文摘要(Abstract)

A classic result by Stockmeyer gives a non-elementary lower bound to the emptiness problem for star-free generalized regular expressions. This result is intimately connected to the satisfiability problem for interval temporal logic, notably for formulas that make use of the so-called chop operator. Such an operator can indeed be interpreted as the inverse of the concatenation operation on regular languages, and this correspondence enables reductions between non-emptiness of star-free generalized regular expressions and satisfiability of formulas of the interval temporal logic of chop under the homogeneity assumption. In this paper, we study the complexity of the satisfiability problem for suitable weakenings of the chop interval temporal logic, that can be equivalently viewed as fragments of Halpern and Shoham interval logic. We first consider the logic $\mathsf{BD}_{hom}$ featuring modalities $B$, for \emph{begins}, corresponding to the prefix relation on pairs of intervals, and $D$, for \emph{during}, corresponding to the infix relation. The homogeneous models of $\mathsf{BD}_{hom}$ naturally correspond to languages defined by restricted forms of regular expressions, that use union, complementation, and the inverses of the prefix and infix relations. Such a fragment has been recently shown to be PSPACE-complete . In this paper, we study the extension $\mathsf{BD}_{hom}$ with the temporal neighborhood modality $A$ (corresponding to the Allen relation \emph{Meets}), and prove that it increases both its expressiveness and complexity. In particular, we show that the resulting logic $\mathsf{BDA}_{hom}$ is EXPSPACE-complete.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2768,
  title = {The addition of temporal neighborhood makes the logic of prefixes and sub-intervals EXPSPACE-complete},
  author = {L. Bozzelli and A. Montanari and A. Peron and P. Sala},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 20, Issue 1},
  year = {2024},
  doi = {10.46298/lmcs-20(1:23)2024}
}