约束驱动的超Petri网合成
Constraint-Driven Synthesis of Hyper Petri Nets
浏览论文内容
中文总结 AI 辅助
研究用Petri网对受约束机器人系统行为建模与合成，提出超Petri网方法从布尔规范合成Petri网，明确可观测标识与执行语义，通过两个场景证明该方法，为系统设计提供结构化方式并提出新研究方向。
中文摘要 AI 辅助
本文探讨使用Petri网对受约束机器人系统行为进行建模与合成。研究如何构建模型，使所有可观测系统状态满足给定逻辑约束且与可执行变迁语义保持一致。为此引入超Petri网（HyPN）方法，从布尔规范合成Petri网，明确区分可观测标识与底层Petri网执行。该方法引入由可允许（原子）激发序列诱导的可观测状态上的显式执行语义，确保所有可观测标识满足约束，揭示逻辑可行性与可执行行为间的根本不匹配。在受月球车系统启发的两个场景中得以证明。这些结果对机器人和自主系统设计尤为重要，提供结构化方式确保正确系统配置，同时明确考虑执行约束。所提框架还在执行抽象、可允许变迁系统及在满足约束状态间导航的策略选择方面提出新研究方向。
英文摘要
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.
发表机构
- Warsaw University of Technology（华沙技术大学）
- NASA Jet Propulsion Laboratory（美国宇航局喷气推进实验室）
- California Institute of Technology（加州理工学院）
机构由 AI 辅助整理，请以论文原文为准。
