LTLf（有限轨迹线性时序逻辑）

LTLf（Linear Temporal Logic over finite traces）是经典 LTL 的变体，专门用于有限轨迹的时序性质规约。传统 LTL 假设无限轨迹，而许多实际系统（如业务流程、机器人任务）在有限步内终止，LTLf 为此提供了形式化语义。其技术核心包括将 LTLf 公式自动机化（DFA）以及基于自动机的规划与合成算法。LTLf 在 AI 规划、反应式合成、业务流程管理等领域有广泛应用，代表工作包括 De Giacomo 和 Vardi 等人的系列论文。