Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

技術要約：Timed Rebecaを用いたROS2マルチロボットシステムのモデリングおよびモデル検査

問題提起
マルチロボットシステム（MRS）の開発には、複雑な非同期相互作用、並行性、および連続的な物理ダイナミクスが伴う。形式検証、特にモデル検査は、システムの安全性やライブネスといった特性を検証するための決定論的な手段を提供するが、ロボティクスへの適用においては「離散と連続のギャップ」が障壁となる。モデル検査は有限状態の離散モデルを必要とするが、ロボットの振る舞い（移動、センシング）は連続的である。さらに、連続的なダイナミクスを離散モデルに変換する際、状態空間の爆発を招いたり、抽象化されたモデルが実際の物理システムを正確に表現できなくなる（忠実度の喪失）ことがよくある。既存のアプローチは、ロボットの振る舞いを過度に単純化したり（例：ロボットを無次元の点として扱う）、形式モデルと実際の実装コード（例：ROS2）との間の厳密なリンクを提供できなかったりすることが多い。

手法
著者らは、Timed Rebecaの形式モデルとROS2実装の間の隔たりを埋める、実用的な双方向エンジニアリング・ワークフローを提案している。

1. アーキテクチャとマッピング:

   • システムは、分散ノード（ROS2）のネットワークとしてモデル化され、それがTimed Rebecaにおける「rebecs（アクター）」へとマッピングされる。
   • ROS2の通信メカニズム（パブリッシュ・サブスクライブ、サービス）は、Rebecaのメッセージサーバ（msgsrv）および非同期メッセージパッシングへとマッピングされる。
   • 連続変数（位置、速度、時間）は離散化される。ロボットのポーズはグリッドセルと離散的な角度（45°刻み）にマッピングされ、レーザースキャンデータは角度ステップ（2°刻み）へと離散化される。

2. 離散化戦略:

   • 連続的な物理現象と離散的な状態との間のギャップを管理するために、著者らはナイキスト・シャノンのサンプリング定理から導出された特定の制約を導入している。
   • 速度 vs スキャンレート: 安全制約として、グリッドセルを通過する時間が、センサーのスキャン周期の少なくとも2倍であること（$action\_time > 2 \times signal\_period$）が設定される。これにより、離散モデルの粒度においてロボットの位置が観測可能であることが保証される。
   • グリッド解像度 vs ロボットサイズ: 制約により、グリッドセルのサイズがロボットの物理的寸法よりも小さくなること（$cell\_width < robot\_length / \sqrt{2}$）が保証される。これにより、離散ステップ間で発生する衝突を見逃さないようにする。

3. 最適化とツール:

   • 状態空間の爆発に対処するため、著者らは三角関数の事前計算やルックアップテーブルの使用といった最適化技術を採用し、モデル検査中のオンザフライでの計算を排除している。
   • ワークフローは反復的である。まずプロトタイプモデルが作成され、次にROS2コードの開発が行われる。その後、構造的および振る舞い的な等価性を確保するためにモデルが調整され、コードとの意味的な整合性が確認される。

4. 検証:

   • Timed Rebecaモデルは、モデルチェッカーである「Afra」を用いて検証される。
   • 検証される主な特性には、衝突回避（2台のロボットが交差しない）、到達可能性／デッドロックフリー（すべてのロボットがターゲットに到達する）、および混雑回避（ロボットが無限に停滞しない）が含まれる。
   • 検証結果は、ROS2シミュレーション（RViz2を使用）に対して検証され、モデルが予測した失敗が実際のシステムにおいて再現されること、および安全な構成がパスすることを確認する。

主な貢献

1. ラウンドトリップ・エンジニアリング: 抽象的なTimed Rebecaモデルと展開されたROS2実装との間で意味的な一貫性を維持するプロセスを示しており、モデルが単なる理論的な演習ではなく、コードの忠実な表現であることを保証している。
2. 離散化戦略: 連続的な物理的振る舞い（運動学、センサーデータ）を、忠実度を損なうことなく離散的な形式モデルにマッピングするための特定の手法を開発した。これには、安全な動作パラメータ（スキャンレートに対する速度制限など）を決定するための、ナイキスト由来の制約の適用が含まれる。
3. 実用的な検証: モデル検査の結果がROS2の実行と一致することを実証している。モデルによって予測された違反（例：特定の速度とスキャンレートの組み合わせによる衝突）はシミュレーション上で再現され、安全な構成はすべてのシミュレーションをパスしている。
4. 並行性の処理: アクターベースのモデリングと、ターゲットを絞った離散化およびデータの最適化を組み合わせることで、マルチロボットの並行性と状態空間の爆発という課題に対処している。

結果
著者らは、5台の自律移動ロボットが交差する経路を持つ50x50のグリッド内をナビゲートするシナリオを用いて、このアプローチを評価した。

• 正常に動作するケース: パラメータが導出された安全制約（例：スキャンレートに基づく速度制限）に従っている場合、モデルチェッカーは到達可能性と衝突回避を検証した。ROS2シミュレーションもこれらの結果を裏付け、すべてのロボットは衝突することなくターゲットに到達した。
• 動作しないケース: パラメータが制約に違反した場合（例：一様な速度によるロックステップ運動、またはナイキスト由来の制限を超える速度）、モデルチェッカーは迅速に反例（衝突）を特定した。ROS2シミュレーションもこれらの失敗を再現し、衝突率は制約違反の深刻度と相関していた。
• 状態空間の効率性: 動作しないケースでは、モデルチェッカーは（7,000状態未満の探索で反例を見つけ）早期に終了したが、正常に動作するケースでは、徹底的な探索（最大約20,000状態）を必要とした。これは、安全でない構成を検出する上での本アプローチの効率性を示している。

意義と主張
本論文は、単なるシミュレーションではなく、モデル検査を通じて連続的なロボットの振る舞いを分析するために、「十分な」抽象レベルを備えた離散モデルを作成するという「実用的なモデリング・アプローチ」を提供すると主張している。

• ギャップの架け橋: 中心的な意義は、連続的なダイナミクスを、検証にはコンパクトでありながら、実際の実装において安全特性が保持されるほど忠実な離散モデルへと、成功裏に翻訳した点にある。
• 早期検出: 本研究は、モデル検査が、実行の非決定的な性質のために従来のシミュレーションが見逃す可能性のある、稀な安全性問題（例：特定の並行性に起因する衝突）を明らかにできることを示している。
• 拡張性と限界: 著者らは、現在のモデルとコード間の手動の同期はエラーが発生しやすいこと、およびパスの長さが増加するとメモリ制約によって拡張性が制限されることを認め、限界についても述べている。しかし、彼らの手法は、単純なシングルロボットや無次元の障害物シナリオを超え、高度な自律システムをモデル化し検証しようとする研究者にとって、基礎的なリファレンスを提供すると主張している。

結論として、モデル検査は離散化という課題を伴うものの、物理的制約に基づいた原則的な戦略と反復的な検証を用いることで、複雑なマルチロボットシステムの重要な特性を効果的に検証できると述べている。