约束驱动的超Petri网合成

摘要

本文提出超Petri网方法，从布尔规范合成Petri网，显式区分可观测标记和底层执行，确保所有可观测状态满足逻辑约束。通过月球车案例展示了逻辑可行性与可执行行为之间的根本不匹配，为机器人系统设计提供了结构化方法。