論文の概要: RoboCertProb: Property Specification for Probabilistic RoboChart Models

• arxiv url: http://arxiv.org/abs/2403.08136v1
• Date: Tue, 12 Mar 2024 23:47:00 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-14 16:22:46.535393
• Title: RoboCertProb: Property Specification for Probabilistic RoboChart Models
• Title（参考訳）: RoboCertProb:確率的RoboChartモデルの仕様
• Authors: Kangfeng Ye and Jim Woodcock
• Abstract要約: 本研究は,RoboChartでモデル化された確率論的ロボットシステムの量的特性を特定するためのRoboCertProbを提案する。 RoboChartモデル上でRoboCertProbを解釈するために、マルコフ意味論(DTMCとMDP)をRoboChartに与える。 プロパティ仕様に加えて、RoboCertProbは、RoboChartモデルで緩やかな定数と未指定の関数と操作を設定する権利も私たちに与えています。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: RoboChart is a core notation in the RoboStar framework which brings modern modelling and formal verification technologies into software engineering for robotics. It is a timed and probabilistic domain-specific language for robotics and provides a UML-like architectural and state machine modelling. This work presents RoboCertProb for specifying quantitative properties of probabilistic robotic systems modelled in RoboChart. RoboCertProb's semantics is based on PCTL*. To interpret RoboCertProb over RoboChart models, we give a Markov semantics (DTMCs and MDPs) to RoboChart, derived from its existing transformation semantics to the PRISM language. In addition to property specification, RoboCertProb also entitles us to configure loose constants and unspecified functions and operations in RoboChart models. It allows us to set up environmental inputs to verify reactive probabilistic systems not directly supported in probabilistic model checkers like PRISM because they employ a closed-world assumption. We implement RoboCertProb in an accompanying tool of RoboChart, RoboTool, for specifying properties and automatically generating PRISM properties from them to formally verify RoboChart models using PRISM. We have used it to analyse the behaviour of software controllers for two real robots: an industrial painting robot and an agricultural robot for treating plants with UV lights.
• Abstract（参考訳）: RoboChartはRoboStarフレームワークの中核的な表記法であり、ロボット工学のソフトウェア工学にモダンなモデリングとフォーマルな検証技術をもたらす。 ロボット工学のためのタイムドで確率的なドメイン固有言語であり、UMLのようなアーキテクチャと状態マシンのモデリングを提供する。 本研究は,RoboChartでモデル化された確率論的ロボットシステムの量的特性を特定するためのRoboCertProbを提案する。 RoboCertProbのセマンティクスはPCTL*に基づいている。 RoboChartモデル上でRoboCertProbを解釈するために、既存の変換セマンティクスからPRISM言語に派生したマルコフ意味論(DTMCとMDP)をRoboChartに与える。 プロパティ仕様に加えて、RoboCertProbは、RoboChartモデルで緩やかな定数と未指定の関数と操作を設定する権利も私たちに与えています。 これにより、PRISMのような確率論的モデルチェッカーで直接サポートされていない反応確率システムを、クローズドワールドの仮定を採用するため、環境入力を設定して検証することができる。 我々はRoboChartの付属ツールであるRoboToolにRoboCertProbを実装し、プロパティの指定とPRISMプロパティの自動生成を行い、PRISMを用いたRoboChartモデルの検証を行う。 我々は、産業用塗装ロボットと、植物を紫外線で治療する農業用ロボットの2つの実際のロボットに対して、ソフトウェアコントローラの動作を分析するためにこれを使用しました。

関連論文リスト

• Learning Object Properties Using Robot Proprioception via Differentiable Robot-Object Interaction [52.12746368727368]
  微分可能シミュレーションは、システム識別の強力なツールとなっている。 本手法は,オブジェクト自体のデータに頼ることなく,ロボットからの情報を用いてオブジェクト特性を校正する。 低コストなロボットプラットフォームにおける本手法の有効性を実証する。
  論文  参考訳（メタデータ） (2024-10-04T20:48:38Z)
• ReKep: Spatio-Temporal Reasoning of Relational Keypoint Constraints for Robotic Manipulation [31.211870350260703]
  キーポイント制約(キーポイント制約、英: Keypoint Constraints)は、ロボット操作における制約を視覚的に表現した表現である。 ReKepはPython関数として表現され、環境の3Dキーポイントのセットを数値的なコストにマッピングする。 車輪付きシングルアームプラットフォームと静止式デュアルアームプラットフォーム上でのシステム実装について述べる。
  論文  参考訳（メタデータ） (2024-09-03T06:45:22Z)
• RoboPoint: A Vision-Language Model for Spatial Affordance Prediction for Robotics [46.63773228934993]
  本稿では,ロボットドメインやニーズに対して,視覚言語モデル(VLM)を命令チューニングする,自動合成データ生成パイプラインを提案する。 パイプラインを使用して、与えられた言語命令に対する画像キーポイントの価格を予測するVLMであるRoboPointを訓練する。 実験の結果,RoboPointは空間空き量の予測精度が21.8%,下流タスクの成功率が30.5%,最先端VLMが21.8%向上していることがわかった。
  論文  参考訳（メタデータ） (2024-06-15T19:22:51Z)
• RoboScript: Code Generation for Free-Form Manipulation Tasks across Real and Simulation [77.41969287400977]
  本稿では,コード生成を利用したデプロイ可能なロボット操作パイプラインのためのプラットフォームである textbfRobotScript を提案する。 自由形自然言語におけるロボット操作タスクのためのコード生成ベンチマークも提案する。 我々は,Franka と UR5 のロボットアームを含む,複数のロボットエボディメントにまたがるコード生成フレームワークの適応性を実証した。
  論文  参考訳（メタデータ） (2024-02-22T15:12:00Z)
• Interactive Planning Using Large Language Models for Partially Observable Robotics Tasks [54.60571399091711]
  大きな言語モデル(LLM)は、オープン語彙タスクを実行するロボットエージェントを作成することで、驚くべき成果を上げている。 LLMを用いた部分的に観測可能なタスクのための対話型計画手法を提案する。
  論文  参考訳（メタデータ） (2023-12-11T22:54:44Z)
• Creative Robot Tool Use with Large Language Models [47.11935262923095]
  本稿では,暗黙的な身体的制約や長期計画を含むタスクにおいて,ツールを創造的に活用できるロボットの実現可能性について検討する。 我々は、自然言語命令を受け入れ、シミュレーションと実環境の両方でロボットを制御する実行可能なコードを出力するシステムであるRoboToolを開発した。
  論文  参考訳（メタデータ） (2023-10-19T18:02:15Z)
• RT-1: Robotics Transformer for Real-World Control at Scale [98.09428483862165]
  我々は,有望なスケーラブルなモデル特性を示す,ロボティクストランスフォーマーと呼ばれるモデルクラスを提示する。 実世界の課題を遂行する実ロボットの大規模データ収集に基づいて,様々なモデルクラスと,データサイズ,モデルサイズ,データの多様性の関数として一般化する能力について検証した。
  論文  参考訳（メタデータ） (2022-12-13T18:55:15Z)
• ProgPrompt: Generating Situated Robot Task Plans using Large Language Models [68.57918965060787]
  大規模言語モデル(LLM)は、タスク計画中の潜在的な次のアクションを評価するために使用することができる。 本稿では, プログラム型LCMプロンプト構造を用いて, 配置環境間での計画生成機能を実現する。
  論文  参考訳（メタデータ） (2022-09-22T20:29:49Z)
• Manipulation of Articulated Objects using Dual-arm Robots via Answer Set Programming [10.316694915810947]
  調音物体の操作はロボティクスにおいて最も重要なものであり、最も複雑な操作の1つと見なすことができる。 従来、この問題は、柔軟性と移植性に欠けるアドホックなアプローチによって対処されてきた。 本稿では,ロボット制御アーキテクチャにおける調音オブジェクトの自動操作のための解答セットプログラミング(ASP)に基づくフレームワークを提案する。
  論文  参考訳（メタデータ） (2020-10-02T18:50:39Z)

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

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