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

TL;DR

The paper addresses safety and reliability in robot-assisted dressing under runtime uncertainty by modeling the task as a parametric discrete-time Markov chain ($pDTMC$) whose transition probabilities are updated online via Bayesian inference. Safety and performance requirements are specified in probabilistic computation tree logic ($PCTL$) and precomputed symbolically with PRISM+PARAM, enabling real-time evaluation through parameter substitution without re-running the model checker; key expressions include $P_{\leq 0.1}[F\, s=8]$, $P_{\geq 0.9}[F\, s=3]$, and $P_{=?}[F\, s=7]$. An adaptive loop combines runtime Bayesian updates with offline symbolic verification to guide decisions with low overhead, while hazard-informed evaluation ensures compliance with safety constraints. The evaluation demonstrates reachability, cost, and reward trade-offs for snag mitigation and escalation, revealing how hybrid human- and autonomous-recovery pathways can compensate for weaknesses in either approach and improving safety in a complex, close-contact setting. Overall, the framework offers a lightweight, explainable approach for runtime assurance in robot-assisted dressing and is adaptable to broader human-robot interaction tasks.

Abstract

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.

Figures (6)

• Figure 1: High-level control architecture showing runtime adaptation via symbolic verification.
• Figure 2: Abstraction of the pDTMC RAD model. Transition probabilities ($p_{[.]}$) govern state transitions. Timeout conditions (e.g., $t = \texttt{MAX\_TIME}$ in $s_6$) ensure escalation resolution. Rewards ($R_{[.]}$) and costs ($C_{[.]}$) are linked to outcome states.
• Figure 3: Probability of successful mitigation (reaching $s_7$) for varying autonomous mitigation success probability ($p_7$) and human failure probability ($p_8$). Lighter regions indicate higher success rates.
• Figure 4: Reachability probability of undetected snag escalation ($s_2$) as a function of detection probability $p_2$ and undetected escalation probability $p_3$. Lighter regions indicate higher failure probability. Dashed contour lines highlight key risk thresholds: $P=0.5$ (Safety Threshold) and $P=0.8$ (Critical Risk). Annotated zones mark high-risk and safe regions.
• Figure 5: Annotated heatmap showing the expected cost of undetected snag escalation, computed as $C_{S2} \cdot P_{=?}[F\, s=2]$, over varying detection probability ($p_2$) and escalation persistence ($p_3$). The Alert Zone (Cost $\geq$ 0.3) highlights failure-prone conditions; the Safe Zone (Cost $<$ 0.3) reflects robust detection and recovery.