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