PROSKILL: A formal skill language for acting in robotics

要約

自律ロボットにとって、行動は重要な意思決定機能です。
演技は、監督するアクティビティ (洗練、ローカル回復、一時的なディスパッチング、外部の非同期イベント、コマンドの実行など) を実装およびモデル化するスキルに依存しており、すべてオンラインで行われます。
プランニングとロボット プラットフォームの間に座って、演技は多くの場合、プログラミングのプリミティブとこれらのスキルを実行するインタープリターに依存します。
ロボットの機能コンポーネントをプログラムするための正式なフレームワークを提供した経験に基づいて、演技スキルをプログラムするための新しい言語を提案します。
この言語は、正式なモデルに明確にマップされ、オフラインでプロパティをチェックしたり、スキル (より正確には正式に同等のもの) を実行したり、実行時検証を実行したりするために使用できます。
この新しい言語でドローンの測量ミッションをプログラムし、プログラム上のいくつかの形式的特性を証明し、ミッションを実行するためにドローン上で形式モデルを直接実行する方法を実際の例で説明します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google