Symbolic Runtime Verification and Adaptive Decision-Making for Robot-Assisted Dressing

要約

ランタイムモニタリングと正式な検証により、低レベルのハザード応答を増強するロボット支援ドレッシングのコントロールフレームワークを提示します。
パラメトリックディスクリートタイムマルコフチェーン（PDTMC）はドレッシングプロセスをモデル化し、ベイジアン推論は感覚とユーザーのフィードバックに基づいてこのPDTMCの遷移確率を動的に更新します。
ハザード分析からの安全上の制約は、確率的計算ツリー論理で表され、確率的モデルチェッカーを使用して象徴的に検証されます。
私たちは、衣料品の緩和とエスカレーションのための到達可能性、コスト、報酬のトレードオフを評価し、リアルタイムの適応を可能にします。
私たちのアプローチは、安全性を認識し、説明可能なロボット支援のための正式でありながら軽量な基盤を提供します。

要約(オリジナル)

We present a control framework for robot-assisted dressing that augments low-level hazard response with runtime monitoring and formal verification. A parametric discrete-time Markov chain (pDTMC) models the dressing process, while Bayesian inference dynamically updates this pDTMC’s transition probabilities based on sensory and user feedback. Safety constraints from hazard analysis are expressed in probabilistic computation tree logic, and symbolically verified using a probabilistic model checker. We evaluate reachability, cost, and reward trade-offs for garment-snag mitigation and escalation, enabling real-time adaptation. Our approach provides a formal yet lightweight foundation for safety-aware, explainable robotic assistance.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google