×

Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm. (English) Zbl 1367.65032

Summary: Conformal geometric algebra (CGA) is an advanced geometric language used in solving three-dimensional Euclidean geometric problems due to its simple, compact and coordinate-free formulations. It promises to stimulate new methods and algorithms in all areas of science dealing with geometric properties, especially for engineering applications. This paper presents a higher-order logic formalization of CGA theories in the HOL-Light theorem prover. First, we formally define the classical algebraic operations and representations of geometric entities in the new framework. Second, we use these results to reason about the correctness of operation properties and geometric features such as the distance between the geometric entities and their rigid transformations in higher-order logic. Finally, in order to demonstrate the practical effectiveness and utilization of this formalization, we use it to formally model the grasping algorithm of a robot based on the conformal geometric control technique and verify the property that whether the robot can grasp firmly or not.

MSC:

65D18 Numerical aspects of computer graphics, image analysis, and computational geometry
15A66 Clifford algebras, spinors
70E60 Robot dynamics and control of rigid bodies
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aristidou A., Lasenby J.: FABRIK: a fast, iterative solver for the inverse kinematics problem. Graph. Models 73(4), 243-260 (2011) · doi:10.1016/j.gmod.2011.05.003
[2] Bayro-Corrochano, E., Bernal-Marin, M.: Generalized hough transform and conformal geometric algebra to detect lines and planes for building 3D maps and robot navigation. In: Intelligent Robots and Systems (IROS), IEEE/RSJ International Conference on, pp. 810-815 (2010)
[3] Bayro-Corrochano E., Zamora-Esquivel J.: Differential and inverse kinematics of robot devices using conformal geometric algebra. Robotica 25(1), 43-61 (2007) · doi:10.1017/S0263574706002980
[4] Blanchette, J.C., Nipkow, T.: Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. Lecture Notes in Computer Science, pp. 131-146 (2010) · Zbl 1291.68326
[5] Buchholz, S.; Sommer, G.; Sommer, G. (ed.), Introduction to neural computation in Clifford algebra, 291-314 (2001), Heidelberg · Zbl 1073.68645 · doi:10.1007/978-3-662-04621-0_12
[6] Carbajal-Espinosa, O., Osuna-Gonzalez, G., Gonzalez-Jimenez, L. et al.: Visual servoing and robust object manipulation using symmetries and conformai geometric algebra. In: Humanoid Robots (Humanoids), IEEE-RAS International Conference on, pp. 1051-1056 (2014) · Zbl 1177.65036
[7] Dorst L., Fontijne D., Mann S.: Geometric Algebra for Computer Science: An Object Oriented approach to Geometry. Morgan Kaufmann, San Francisco (2007)
[8] Franchini S., Gentile A., Sorbello F. et al.: ConformalALU: a conformal geometric algebra coprocessor for medical image processing. IEEE Trans. Comput. 64(4), 955-970 (2015) · Zbl 1360.68932 · doi:10.1109/TC.2014.2315652
[9] Gonzalez-Jimenez, L.E., Carbajal-Espinosa, O.E., Bayro-Corrochano, E.: Geometric techniques for the kinematic modeling and control of robotic manipulators. In: Proc. of IEEE ICRA, pp. 5831-5836 (2011) · Zbl 1073.68645
[10] Han D.S., Yang Q.L., Xing J.C.: UML-Based modeling and formal verification for software self-adaptation. J. Softw. 26(4), 730-746 (2015)
[11] Harrison, J.: HOL Light: A Tutorial Introduction. Lecture Notes in C Computer Science, pp. 265-269 (1996)
[12] Harrison, J.: Towards Self-verification of HOL Light. Lecture Notes in Computer Science, pp. 177-191 (2006) · Zbl 1222.68364
[13] Harrison, J.: https://code.google.com/p/hol-light/source/browse/trunk/Multivariate/clifford.ml (2010) · Zbl 1260.68373
[14] Harrison J.: The HOL light theory of Euclidean space. J. Autom. Reasoning 50(2), 173-190 (2013) · Zbl 1260.68373 · doi:10.1007/s10817-012-9250-9
[15] Hasan, O., Ahmad, M.: Formal analysis of steady state errors in feedback control systems using HOL-light. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), 18-22 March, Grenoble, France, pp. 1423-1426 (2013)
[16] Hestenes D.: Spacetime physics with geometric algebra. Am. J. Phys. 71(7), 691-714 (2003) · doi:10.1119/1.1571836
[17] Hildenbrand, D., Bayro-Corrochano, E., Zamora, J.: Advanced geometric approach for graphics and visual guided robot object manipulation. In: Proc. of IEEE ICRA, pp. 4727-4732 (2005)
[18] Hildenbrand, D.: Geometric computing in Computer Graphics and Robotics using Conformal Geometric Algebra. PhD Thesis, Technische Universitaet Darmstadt (2007)
[19] Hildenbrand D., Zamora J., Bayro-Corrochano E.: Inverse kinematics computation in computer graphics and robotics using conformal geometric algebra. Adv. Appl. Clifford Algebras 18(3), 699-713 (2008) · Zbl 1177.65036 · doi:10.1007/s00006-008-0096-5
[20] Hildenbrand D.: Foundations of geometric algebra computing. Geom. Comput. 1479(4), 27-30 (2012)
[21] Hildenbrand, D., Koch, A.: Gaalop: high performance computing based on conformal geometric algebra. Geom. Comput. (2013) · Zbl 1214.68434
[22] Hitzer E., Perwass C.: Interactive 3D space group visualization with CLUCalc and the clifford geometric algebra description of space groups. Adv. Appl. Clifford Algebras 20(4), 631-658 (2010) · Zbl 1242.20060 · doi:10.1007/s00006-010-0214-z
[23] Kim J.S., Jin H.J., Park J.H.: Inverse kinematics and geometric singularity analysis of a 3-SPS/S redundant motion mechanism using conformal geometric algebra. Mech. Mach. Theory 90, 23-36 (2015) · doi:10.1016/j.mechmachtheory.2015.02.009
[24] Klein, G., Elphinstone, K., Heiser, G., et al.: seL4: Formal Verification of an OS Kernel. Acm Symposium on Operating Systems Principles, pp. 207-220 (2009)
[25] Li H.: Conformal geometric algebra and algebraic manipulations of geometric invariants. J. Comput. Aided Des. Comput. Graph. 18(7), 902-911 (2006)
[26] Li, H.: Automated theorem proving in the homogeneous model with Clifford bracket algebra. In: Dorst, L. (eds.) Applications of Geometric Algebra in Computer Science and Engineering, pp. 69-78. Boston (2002) · Zbl 1028.15027
[27] Li, M., Guan, J.: Possibilistic C-Spherical Shell clustering algorithm based on conformai geometric algebra. Signal Processing (ICSP), IEEE 10th International Conference on, pp. 1347-1350 (2010) · Zbl 1312.15031
[28] Li, H., Hestenes, D., Rockwood, A.: A universal model for conformal geometries of euclidean, spherical and double-hyperbolic spaces. Geom. Comput. Clifford Algebras, 77-104 (2001) · Zbl 1071.51501
[29] Lopez-Franco, C., Arana-Daniel, N., Bayro-Corrochano, E.: Vision-based robot control with omnidirectional cameras and conformal geometric algebra. In: IEEE International Conference on Robotics and Automation (ICRA), pp. 2543-2548 (2010)
[30] Lounesto P.: Clifford algebras and Hestenes spinors. Found. Phys. 23(9), 1203-1237 (1993) · doi:10.1007/BF01883677
[31] Oviedo-Barriga, J., Carbajal-Espinosa, O., Gonzalez-Jimenez, L. et al.: Robust tracking of bio-inspired references for a biped robot using geometric algebra and sliding modes. In: Proc. of IEEE ICRA, pp. 5317-5322 (2013)
[32] Pham, M.T., Tachibana, K., Yoshikawa, T. et al.: A clustering method for geometric data based on approximation using conformal geometric algebra. In: IEEE International Conference on Fuzzy Systems (FUZZ-IEEE), pp. 2540-2545 (2011)
[33] Resten Y., Maler O., Marcus M. et al.: Symbolic model checking with rich assertional languages. Comput. Aided Verification 43(2), 424-435 (2006)
[34] Shirokov D.: Calculation of elements of spin groups using generalized Pauli’s theorem. Adv. Appl. Clifford Algebras 25(1), 227-244 (2014) · Zbl 1312.15031 · doi:10.1007/s00006-014-0471-3
[35] Siddique, U., Hasan, O.: On the formalization of gamma function in HOL. J. Autom. Reason. 407-429 (2014) · Zbl 1315.68224
[36] Suter, J.: Geometric Algebra Primer. Available: http://www.jaapsuter.com (2003)
[37] Wang, C., Wu, H., Miao, Q.: Inverse kinematics computation in robotics using Conformal Geometric Algebra. Technology and Innovation Conference (ITIC), International pp. 1-5. IET (2009)
[38] Wu W.J.: Basic principles of mechanical theorem proving in elementary geometries. J. Autom. Reason. 2(3), 221-252 (1986) · Zbl 0642.68163 · doi:10.1007/BF02328447
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.