用形式化验证让助穿机器人实时判断安全风险并自适应调整动作。
Symbolic Runtime Verification and Adaptive Decision-Making for Robot-Assisted Dressing
- 基于贝叶斯更新的马尔可夫链模型，动态感知用户状态和环境反馈。
- 通过概率逻辑验证，实现对衣物勾挂等危险的实时可达性分析与成本收益权衡。
- 适合需要高安全性与可解释性的医疗辅助机器人场景。
我们提出一种用于机器人助穿的控制框架，将底层危险响应与运行时监控及形式化验证相结合。采用参数化离散时间马尔可夫链（pDTMC）建模穿衣过程，通过贝叶斯推断根据传感数据和用户反馈动态更新转移概率。来自危险分析的安全约束以概率计算树逻辑表达，并利用概率模型检测器进行符号化验证。该方法评估了衣物勾挂规避与升级策略之间的可达性、成本与奖励权衡，支持实时自适应决策。本方案为安全敏感、可解释的机器人辅助提供了一种形式化且轻量的基础。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。