Formal Analysis of the Kinematic Jacobian in Screw Theory
Sponsor
National Key RD Plan Plan 2017YFC0806700 National Natural Science Foundation of China 61472468 61572331 61602325 61702348 Capacity Building for Sci-Tech InnovationFundamental Scientific Research Funds 025185305000 Capital Normal University Major (key) Nurturing Project
Published In
Formal Aspects of Computing
Document Type
Citation
Publication Date
11-1-2018
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.
Locate the Document
DOI
10.1007/s00165-018-0468-0
Persistent Identifier
https://archives.pdx.edu/ds/psu/27800
Citation Details
Shi, Z., Wu, A., Yang, X., Guan, Y., Li, Y., & Song, X. (2018). Formal analysis of the kinematic Jacobian in screw theory. Formal Aspects of Computing, 30(6), 739–757. https://doi.org/10.1007/s00165-018-0468-0