.png){kind=icon}
.png){kind=icon}
Return
Formal verification of physical human-robot interaction using interactive theorem proving
.png){kind=icon}
PRE
AI
DOI：10.1515/jisys-2025-0101.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Physical Human-robot Interaction (pHRI) involves physical collaboration between humans and robots to perform tasks safely and efficiently in shared environments. Traditionally, pHRI behavior has been analyzed using analytical or simulation-based methods, which may suffer from human error and incomplete coverage of system behavior. Formal methods, such as Interactive Theorem Proving (ITP), offer a mathematically rigorous alternative by constructing logical models of system dynamics and verifying their properties through deduction and proof. This paper proposes an ITP-based approach for the formal analysis of pHRI dynamics using the HOL Light theorem prover. We formalize the one-dimensional admittance control equations, derive their Laplace-domain representations, and conduct a formal stability analysis of the corresponding open and closed-loop controllers. To complement the formal verification, the verified open-loop admittance controller is implemented and simulated in MATLAB, where the step-response and root-locus analyses confirm the formally proven stability guarantees. The results demonstrate that the proposed framework provides both mathematical rigor and practical consistency for ensuring safe and reliable human-robot interaction.
Keywords:
physical Human-robot interaction
differential equations
laplace transform
higher-order logic
interactive theorem proving
HOL Light
Journal
J
IF:
2
Papers:
34
Citations:
0