Acting is an important decisional function for autonomous robots. Acting relies on skills to implement and to model the activities it oversees: refinement, local recovery, temporal dispatching, external asynchronous events, and commands execution, all done online. While sitting between planning and the robotic platform, acting often relies on programming primitives and an interpreter which executes these skills. Following our experience in providing a formal framework to program the functional components of our robots, we propose a new language, to program the acting skills. This language maps unequivocally into a formal model which can then be used to check properties offline or execute the skills, or more precisely their formal equivalent, and perform runtime verification. We illustrate with a real example how we can program a survey mission for a drone in this new language, prove some formal properties on the program and directly execute the formal model on the drone to perform the mission.

翻译：执行是自主机器人的一项重要决策功能。执行依赖于技能来实现和建模其所监督的活动：在线完成细化、局部恢复、时间调度、外部异步事件以及命令执行。作为规划与机器人平台之间的桥梁，执行通常依赖于编程原语和一个执行这些技能的解释器。基于我们在为机器人功能组件提供形式化编程框架方面的经验，我们提出了一种新的语言，用于编程执行技能。该语言明确映射到一个形式化模型，该模型随后可用于离线验证属性、执行技能（或更准确地说，其形式等价形式）并进行运行时验证。我们通过一个真实示例展示了如何用这种新语言为无人机编程一项勘测任务，证明该程序的某些形式化属性，并直接在无人机上执行形式化模型以完成任务。