Formal analysis of the kinematic Jacobian in screw theory |
| |
| Authors: | Zhiping Shi Aixuan Wu Xiumei Yang Yong Guan Yongdong Li Xiaoyu Song |
| |
| Affiliation: | 1.Beijing Advanced Innovation Center for Imaging Technology,Capital Normal University,Beijing,China;2.Beijing Center for Mathematics and Information Interdisciplinary Sciences,Capital Normal University,Beijing,China;3.Beijing Key Laboratory of Light Industrial Robot and Safety Verification,Capital Normal University,Beijing,China;4.Engineering and Computer Science,Portland State University,Portland,USA |
| |
| Abstract: | As robotic systems flourish, reliability has become a topic of paramount importance in the human–robot relationship. The Jacobian matrix in screw theory underpins the design and optimization of robotic manipulators. Kernel properties of robotic manipulators, including dexterity and singularity, are characterized with the Jacobian matrix. The accurate specification and the rigorous analysis of the Jacobian matrix are indispensable in guaranteeing correct evaluation of the kinematics performance of manipulators. In this paper, a formal method for analyzing the Jacobian matrix in screw theory is presented using the higher-order logic theorem prover HOL4. Formalizations of twists and the forward kinematics are performed using the product of exponentials formula and the theory of functional matrices. To the best of our knowledge, this work is the first to formally analyze the kinematic Jacobian using theorem proving. The formal modeling and analysis of the Stanford manipulator demonstrate the effectiveness and applicability of the proposed approach to the formal verification of the kinematic properties of robotic manipulators. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
