用约束驱动方法生成可执行的机器人行为模型，确保状态始终满足逻辑要求。
Constraint-Driven Synthesis of Hyper Petri Nets
- 基于布尔规格合成带约束的佩特里网，区分可观测状态与底层执行
- 构建显式执行语义，保证所有可观测状态均满足约束条件
- 适用于需严格保障安全性的自主系统设计，如月球车控制
本文研究如何利用佩特里网（PNs）对受约束的机器人系统行为进行建模与合成。目标是构建一种模型，使得所有可观测系统状态均满足给定逻辑约束，同时保持可执行转移语义的一致性。为此，提出超佩特里网（HyPN）方法，从布尔规格合成佩特里网，并明确区分可观测标记与底层佩特里网执行。该方法引入可观测状态上的显式执行语义，由允许的（原子）触发序列诱导，从而在构造上确保所有可观测标记满足约束，并揭示了逻辑可行性与可执行行为之间的根本不匹配。该方法在两个受月球车系统启发的场景中得到验证。结果对机器人与自主系统的设计具有重要意义，提供了一种结构化方式以确保正确系统配置，同时显式考虑执行约束。该框架还为执行抽象、允许转移系统及约束满足状态间的策略选择提出了新的研究方向。
原文摘要 · Abstract (English)
This paper addresses the modeling and synthesis of constrained robotic system behaviors using Petri nets (PNs). It investigates how to construct models in which all observable system states satisfy given logical constraints while remaining consistent with executable transition semantics. To answer this, we introduce the Hyper Petri Net (HyPN) approach, which synthesizes Petri nets from Boolean specifications while explicitly distinguishing between observable markings and underlying Petri net execution. The proposed method introduces an explicit execution semantics over observable states, induced by admissible (atomic) firing sequences, ensuring by construction that all observable markings satisfy the constraints and revealing a fundamental mismatch between logical feasibility and executable behavior. This is demonstrated in two scenarios inspired by a lunar rover system. These results are particularly relevant for the design of robotic and autonomous systems, as they provide a structured way to ensure correct system configurations while explicitly accounting for execution constraints. The proposed framework further suggests new research directions in execution abstraction, admissible transition systems, and policy selection for navigating between constraint-satisfying states.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。