解读

面试官通过“放弃PDDL”这一逆向决策点，考察候选人对规划形式化表达能力边界的清醒认知，以及能否在国内真实工业场景中权衡建模成本、求解效率与可解释性。回答需体现：

1. 明确PDDL的时序与状态机表达缺陷；
2. 给出可量化、可落地的国内案例，而非学术玩具问题；
3. 指出切换后的形式化工具链与Agent工程落地路径。

知识点

1. PDDL 3.1的固有短板：仅支持STRIPS/ADL风格动作，无法原生表达线性时序逻辑（LTL）、分支时序逻辑（CTL）、实时约束（RTCTL）及混成状态机；
2. 国内工业强约束场景：高铁调度、证券交易、电力现货市场等，对毫秒级时序刚性、状态循环禁止、计数器/时钟变量有法规级要求；
3. 可替代形式化工具：TLA+、UPPAAL、Spin Promela、Signal Temporal Logic (STL)，可直接对接Model Checker与Runtime Verification框架；
4. Agent工程落地要点：形式化模型需自动生成可执行代码（如Java/C++定时任务），并与大模型Planner通过Guarded Action Interface解耦，确保安全对齐。

答案

当系统约束超出PDDL的时序与状态机表达能力时，应果断放弃PDDL，改用线性时序逻辑（LTL）或实时模型检测语言。
真实案例一：高铁列车自动折返调度

• 约束：中国铁路上海局“虹桥站折返”规则要求列车必须在120 s内完成换端、关门、信号升级三步，且禁止任何一步重入（即状态循环零容忍）。
• PDDL痛点：无法表达**“全局禁止重复进入关门状态”的LTL公式G(!close_door ∧ X(close_door → X(!close_door U departure)))；也无法引入连续时钟变量**做120 s硬实时截止。
• 解决方案：改用UPPAAL建模，将列车车门、信号机、司机操作建模为Timed Automata，用TCTL验证**“换端→关门→出发”总耗时≤120 s；生成C++定时任务嵌入Agent执行层，大模型Planner仅负责高阶路径选择**，时序约束由UPPAAL Runtime Monitor兜底。

真实案例二：上交所期权做市商风控

• 约束：证监会《股票期权交易管理办法》第38条要求做市商在500 ms内对delta超限触发对冲，且日内连续对冲次数不得超过60次（防操纵）。
• PDDL痛点：无法表达**“过去24 h内计数器≤60”的Past-LTL公式H(count≤60)；也无法刻画500 ms硬截止的STL语义◇0,500ms**。
• 解决方案：改用Signal Temporal Logic (STL)，在RTAMT工具链中编写monitor specification，自动生成Java字节码植入做市商Agent；Planner层调用强化学习生成对冲动作，但每步动作需通过STL Monitor的即时布尔 verdict，否则被强制丢弃并报警。

总结：当法规或安全条例出现**“硬实时+计数器+状态循环禁止”三类特征时，PDDL的动作范式与规划器已无法给出可验证的保证**，必须切换至时序逻辑形式化并配套模型检测/运行时验证工具链，才能满足国内监管审计要求。

拓展思考

1. 混合范式：在大模型Agent内部，可保持PDDL用于高层任务分解（如“把货物从A运到B”），但把关键安全片段（如“叉车臂必须在3 s内退出货架”）抽取为STL子规范，通过Guarded Domain Bridge实现双形式化协同，兼顾求解效率与安全可证。
2. 监管科技趋势：中国证监会已启动《算法交易合规接口》行业标准草案，明确要求核心风控规则须以时序逻辑形式化备案，未来PDDL-only的Agent将无法通过券商现场检查；提前储备TLA+/STL建模能力，将成为Agent工程师的合规护城河。