Autonomous agents that perform everyday manipulation actions need to ensure that their body motions are semantically correct with respect to a task request, causally effective within their environment, and feasible for their embodiment. In order to enable robots to verify these properties, we introduce the Law of Task-Achieving Body Motion as an axiomatic correctness specification for body motions. To that end we introduce scoped Task-Environment-Embodiment (TEE) classes that represent world states as Semantic Digital Twins (SDTs) and define applicable physics models to decompose task achievement into three predicates: SatisfiesRequest for semantic request satisfaction over SDT state evolution; Causes for causal sufficiency under the scoped physics model; and CanPerform for safety and feasibility verification at the embodiment level. This decomposition yields a reusable, implementation-independent interface that supports motion synthesis and the verification of given body motions. It also supports typed failure diagnosis (semantic, causal, embodiment and out-of-scope), feasibility across robots and environments, and counterfactual reasoning about robot body motions. We demonstrate the usability of the law in practice by instantiating it for articulated container manipulation in kitchen environments on three contrasting mobile manipulation platforms
翻译:执行日常操作动作的自主智能体需要确保其体运动在任务请求方面语义正确、在其环境中因果有效,并且对其具体形态具有可行性。为了使机器人能够验证这些特性,我们引入任务达成体运动定律作为体运动的公理化正确性规范。为此,我们引入限定范围的任务-环境-形态(TEE)类,该类将世界状态表示为语义数字孪生(SDT),并定义适用的物理模型,从而将任务达成分解为三个谓词:SatisfiesRequest(针对SDT状态演化的语义请求满足性)、Causes(在限定物理模型下的因果充分性)以及CanPerform(在形态层面的安全性与可行性验证)。这种分解产生了一个可重用、独立于具体实现的接口,该接口支持运动合成以及对给定体运动的验证。它还支持类型化故障诊断(语义性、因果性、形态性及超范围性)、跨机器人及环境的可行性分析,以及关于机器人体运动的反事实推理。我们通过在三种不同的移动操作平台上,针对厨房环境中的铰接式容器操作实例化该定律,展示了其在实践中的可用性。