論文の概要: Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

• arxiv url: http://arxiv.org/abs/2511.15227v1
• Date: Wed, 19 Nov 2025 08:28:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-20 15:51:28.703774
• Title: Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca
• Title（参考訳）: タイムレベッカを用いたROS2マルチロボットシステムのモデル化とモデルチェッキング
• Authors: Hiep Hong Trinh, Marjan Sirjani, Federico Ciccozzi, Abu Naser Masud, Mikael Sjödin,
• Abstract要約: Timed Rebecaはアクターベースのモデリング言語で、リアクティブ、並列、タイムセマンティクスをサポートする。 本稿では,マルチボットシステムの設計と検証にモデルを使用する方法,モデルチェックを効率的に行うために継続的システムを個別にモデル化する方法を示す。 RebecaとROS2のコードは、複数の自律ロボットシステムをモデル化するための基盤となる。
• 参考スコア（独自算出の注目度）: 1.3048920509133806
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Model-based development enables quicker prototyping, earlier experimentation and validation of design intents. For a multi-agent system with complex asynchronous interactions and concurrency, formal verification, model-checking in particular, offers an automated mechanism for verifying desired properties. Timed Rebeca is an actor-based modelling language supporting reactive, concurrent and time semantics, accompanied with a model-checking compiler. These capabilities allow using Timed Rebeca to correctly model ROS2 node topographies, recurring physical signals, motion primitives and other timed and time-convertible behaviors. The biggest challenges in modelling and verifying a multi-robot system lie in abstracting complex information, bridging the gap between a discrete model and a continuous system and compacting the state space, while maintaining the model's accuracy. We develop different discretization strategies for different kinds of information, identifying the 'enough' thresholds of abstraction, and applying efficient optimization techniques to boost computations. With this work we demonstrate how to use models to design and verify a multi-robot system, how to discretely model a continuous system to do model-checking efficiently, and the round-trip engineering flow between the model and the implementation. The released Rebeca and ROS2 codes can serve as a foundation for modelling multiple autonomous robots systems.
• Abstract（参考訳）: モデルベースの開発は、より高速なプロトタイピング、初期の実験、設計意図の検証を可能にする。 複雑な非同期インタラクションと並行処理を備えたマルチエージェントシステムでは、特に形式的検証、モデルチェックは、望ましいプロパティを自動検証するメカニズムを提供する。 Timed Rebecaはアクターベースのモデリング言語で、リアクティブ、並列、タイムセマンティクスをサポートし、モデルチェックコンパイラが付属している。 これらの機能により、Timed Rebecaを使用してROS2ノードのトポグラフィーを正しくモデル化し、物理信号、モーションプリミティブなどの時間的および時間的変換可能な振る舞いを再現することができる。 マルチロボットシステムのモデル化と検証における最大の課題は、複雑な情報を抽象化し、離散モデルと連続システムのギャップを埋め、モデルの精度を維持しながら状態空間をコンパクト化することにある。 我々は、異なる種類の情報に対して異なる離散化戦略を開発し、抽象の「十分な」しきい値を特定し、効率的な最適化手法を適用して計算を高速化する。 この作業では、マルチロボットシステムの設計と検証にモデルを使用する方法、モデルチェックを効率的に行うために継続的システムを個別にモデル化する方法、モデルと実装の間のラウンドトリップエンジニアリングフローをデモします。 RebecaとROS2のコードは、複数の自律ロボットシステムをモデル化するための基盤となる。

関連論文リスト

• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。 本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
  論文  参考訳（メタデータ） (2025-10-02T06:25:10Z)
• OptMerge: Unifying Multimodal LLM Capabilities and Modalities via Model Merging [124.91183814854126]
  モデルマージは、複数のエキスパートモデルをひとつのモデルに組み合わせようとしている。 本稿ではMLLMのトレーニングと評価のタスクを明確に分割したモデルマージ研究のベンチマークを紹介する。 モデルマージは、トレーニングデータを必要とせずに改善されたMLLMを構築するための有望な方法であることがわかった。
  論文  参考訳（メタデータ） (2025-05-26T12:23:14Z)
• Generative diffusion model surrogates for mechanistic agent-based biological models [0.003897077734517544]
  CPM(Cellular-Potts Model)は、CPMを開発・尋問する強力なフレームワークである。 サロゲートモデルは複雑な生物学的システムのCPMを加速的に評価することができる。 我々は、in vitroで血管新生を調べるために使用されるCPMのAI代理分類器を訓練する。 我々の研究は、生体システムのデジタル双対を開発するためのDDPMの実装に向けた一歩である。
  論文  参考訳（メタデータ） (2025-05-01T08:19:51Z)
• Domain-aware Control-oriented Neural Models for Autonomous Underwater Vehicles [2.4779082385578337]
  ドメイン認識のレベルが異なる制御指向パラメトリックモデルを提案する。 データ駆動型ブラックボックスとAUVダイナミクスのグレイボックス表現を構築するために、普遍微分方程式を用いる。
  論文  参考訳（メタデータ） (2022-08-15T17:01:14Z)
• Closed-form Continuous-Depth Models [99.40335716948101]
  連続深度ニューラルモデルは高度な数値微分方程式解法に依存している。 我々は,CfCネットワークと呼ばれる,記述が簡単で,少なくとも1桁高速な新しいモデル群を提示する。
  論文  参考訳（メタデータ） (2021-06-25T22:08:51Z)
• Anomaly Detection of Time Series with Smoothness-Inducing Sequential Variational Auto-Encoder [59.69303945834122]
  Smoothness-Inducing Sequential Variational Auto-Encoder (SISVAE) モデルを提案する。 我々のモデルは、フレキシブルニューラルネットワークを用いて各タイムスタンプの平均と分散をパラメータ化する。 合成データセットと公開実世界のベンチマークの両方において,本モデルの有効性を示す。
  論文  参考訳（メタデータ） (2021-02-02T06:15:15Z)
• A Novel Anomaly Detection Algorithm for Hybrid Production Systems based on Deep Learning and Timed Automata [73.38551379469533]
  DAD:DeepAnomalyDetectionは,ハイブリッド生産システムにおける自動モデル学習と異常検出のための新しいアプローチである。 深層学習とタイムドオートマトンを組み合わせて、観察から行動モデルを作成する。 このアルゴリズムは実システムからの2つのデータを含む少数のデータセットに適用され、有望な結果を示している。
  論文  参考訳（メタデータ） (2020-10-29T08:27:43Z)
• Action-Conditional Recurrent Kalman Networks For Forward and Inverse Dynamics Learning [17.80270555749689]
  ロボットのモデルベース制御において、正確な前方および逆ダイナミクスモデルの推定が重要な要素である。 本稿では,フォワードモデル学習のためのアーキテクチャと,逆モデル学習のためのアーキテクチャを提案する。 どちらのアーキテクチャも、予測性能の点で、既存のモデル学習フレームワークと分析モデルを大きく上回っている。
  論文  参考訳（メタデータ） (2020-10-20T11:28:25Z)
• Hybrid modeling: Applications in real-time diagnosis [64.5040763067757]
  我々は、機械学習にインスパイアされたモデルと物理モデルを組み合わせた、新しいハイブリッドモデリングアプローチの概要を述べる。 このようなモデルをリアルタイム診断に利用しています。
  論文  参考訳（メタデータ） (2020-03-04T00:44:57Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。