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.

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