一句话：提出 ALDL_f，将命题逻辑与 NFA 结合，在有限轨迹上表达时序约束，可满足性属于 PSPACE，且表达力等价 MSO。
线性时序逻辑 LTL 因易用且表达力与复杂度平衡而广受欢迎，其表达力等价于一元一阶逻辑，可满足性为 PSPACE-complete。线性动态逻辑 LDL 则等价于一元二阶逻辑，但其可满足性检查方法无法应用于 LDL 的一个非平凡子集。本文提出有限轨迹上的自动机线性动态逻辑 ALDL_f，它是有限轨迹线性动态逻辑 LDL_f 的变体，将命题逻辑与非确定性有限自动机 NFA 结合以表达时序约束。作者证明 ALDL_f 的可满足性属于 PSPACE，并且其表达力等价于一元二阶逻辑。这意味着相比 LTL，ALDL_f 在不增加可满足性复杂度量级的情况下获得了更强的表达力。
Temporal logics are widely used by the Formal Methods and AI communities. Linear Temporal Logic is a popular temporal logic and is valued for its ease of use as well as its balance between expressiveness and complexity. LTL is equivalent in expressiveness to Monadic First-Order Logic and satisfiability for LTL is PSPACE-complete. Linear Dynamic Logic (LDL), another temporal logic, is equivalent to Monadic Second-Order Logic, but its method of satisfiability checking cannot be applied to a nontrivial subset of LDL formulas. Here we introduce Automata Linear Dynamic Logic on Finite Traces (ALDL_f) and show that satisfiability for ALDL_f formulas is in PSPACE. A variant of Linear Dynamic Logic on Finite Traces (LDL_f), ALDL_f combines propositional logic with nondeterministic finite automata (NFA) to express temporal constraints. ALDL$_f$ is equivalent in expressiveness to Monadic Second-Order Logic. This is a gain in expressiveness over LTL at no cost.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2108-12003,
title = {Automata Linear Dynamic Logic on Finite Traces},
author = {Kevin W. Smith and Moshe Y. Vardi},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:2)2025}
}