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.

翻译：时间逻辑被形式化方法与人工智能社区广泛使用。线性时序逻辑是一种流行的时序逻辑，因其易用性以及表达能力与复杂性之间的平衡而备受重视。LTL在表达能力上与一元一阶逻辑等价，其可满足性判定为PSPACE完全问题。另一种时序逻辑——线性动态逻辑（LDL）与一元二阶逻辑等价，但其可满足性判定方法无法应用于LDL公式的非平凡子集。本文提出了有限迹上的自动机线性动态逻辑（ALDL_f），并证明ALDL_f公式的可满足性判定属于PSPACE。作为有限迹上线性动态逻辑（LDL_f）的变体，ALDL_f将命题逻辑与非确定性有限自动机（NFA）相结合以表达时序约束。ALDL_f在表达能力上与一元二阶逻辑等价，这是在零开销下相较于LTL在表达能力上的提升。