Symbolic Runtime Verification and Adaptive Decision-Making for Robot-Assisted Dressing
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910916389371904 |
|---|---|
| author | Rafiq, Yasmin Vázquez, Gricel Calinescu, Radu Dogramadzi, Sanja Hierons, Robert M |
| author_facet | Rafiq, Yasmin Vázquez, Gricel Calinescu, Radu Dogramadzi, Sanja Hierons, Robert M |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_15666 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Symbolic Runtime Verification and Adaptive Decision-Making for Robot-Assisted Dressing Rafiq, Yasmin Vázquez, Gricel Calinescu, Radu Dogramadzi, Sanja Hierons, Robert M Robotics 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. |
| title | Symbolic Runtime Verification and Adaptive Decision-Making for Robot-Assisted Dressing |
| topic | Robotics |
| url | https://arxiv.org/abs/2504.15666 |