Differential-dynamic logic for cooperative robotic systems
Keywords:
hybrid systems, differential-dynamic logic, cooperation man-robot, straight lines or curved bordersAbstract
Hybrid systems are dynamical systems with interacting discrete transitions and continuous evolutions described by differential equations. They combine the digital and continuous physical effects resulting from the cooperation between the man and the robot. The man and the robot handle the same tool, and the control algorithm has the role to prevent the man to cross the critical borders of a 2D safety workplace and to move into undesirable locations. The man manipulates the tool during his activity without interacting with the robot, but near the boundaries of the working area, the robot intervenes to guide the man towards safe trajectories. The scope of the paper is to provide a coherent logical analysis for such hybrid systems defined on 2D safe domains with critical straight lines or curved borders. The differential-dynamic logic (dL) is used to capture the logical content of the dynamics of such systems.
References
VERL, A., SCHÄFFER, A.A., BROCK, O. (Eds.), Soft robotics. Transferring theory to applications, Springer-Verlag, 2015.
FRÄNZLE, M., HERDE, C., HySAT: An efficient proof engine for bounded model checking of hybrid systems, Formal Methods in System Design, 30, 2, pp. 179–198, 2007.
PLATZER, A., Differential-algebraic dynamic logic for differential-algebraic programs, J. Log. Comput., 20, 1, pp. 309–352, 2010.
PLATZER, A., A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems, Logical Methods in Computer Science, 8, 4, pp. 1–44, 2012.
PLATZER, A., Differential dynamic logic for hybrid systems, J. Autom. Reasoning, 41, 2, pp. 143– 189, 2008.
XIA, T., BAIRD, C., JALLO, G., HAYES, K., NAKAJIMA, N., An integrated system for planning, navigation and robotic assistance for skull base surgery, Int. J. of Med. Robot., 4, 4, pp. 321–330. 2008.
KOUSKOULAS, Y., RENSHAW, D., PLATZER, A., KAZANZIDES, P., Certifying the safe design of a virtual fixture control algorithm for a surgical robot, Proc. of the 16th International Conf. on Hybrid Systems: Computation and Control, 2013, pp. 263–272.
PLATZER, A., QUESEL, J.-D., Keymaera: a hybrid theorem prover for hybrid systems, 4th International Joint Conference on Automated Reasoning, Vol. 5195 of Lecture Notes in Computer Science book series (Eds. A. Armando, P. Baumgartner and G. Dowek), SpringerVerlag, 2008, pp. 171–178.
VL?D?REANU, L., ION, I., New approaches on modular walking robots with force-position hybrid control, Rev. Roum. Sci. Techn. – Méc. Appl., 55, 2, pp. 167–182, 2010.
STAICU, St., Kinematics of a translation-rotation hybrid parallel robot, Ro. Techn. Sci. – Appl. Mech., 60, 3, pp. 171–183, 2015.
PLATZER, A., Logical analysis of hybrid systems. Proving theorems for complex dynamics, Springer-Verlag, 2010.
MARTIN, W., COHEN, E., Surface completion of an irregular boundary curve using a concentric mapping, Proceedings of the 5th International Conference on Curves and Surfaces, Saint-Malo, France, 2002, pp. 1–10.
ZHENG, J. J., BALL, A.A., Control point surfaces over non-four-sided areas, Comput. Aided Geom. Design, 14, 9, pp. 807–821, 1997.
BRANICKY, M.S., BORKAR, V.S., MITTER, S.K., A unified framework for hybrid control: model and optimal control theory, IEEE Trans. Automat. Contr., 43, 1, pp. 31–45, 1998.
CHAOCHEN, Z., JI, W., RAVN, A.P., A formal description of hybrid systems, in: Hybrid Systems III, Vol. 5195 of Lecture Notes in Computer Science book series (Eds. R. Alur, T.A. Henzinger, E.D. Sontag), Springer-Verlag, 1995, pp. 511–530.
CHUTINAN, A., KROGH, B.H., Computational techniques for hybrid system verification, IEEE Trans. Automat. Contr., 48, 1, pp. 64–75, 2003.
CLARKE, E.M., FEHNKER, A., HAN, Z., KROGH, B.H., OUAKNINE, J., STURSBERG, O., THEOBALD, M., Abstraction and counterexample-guided refinement in model checking of hybrid systems, Int. J. Found. Comput. Sci., 14, 4, pp. 583–604, 2003.
CLARKE, E.M., GRUMBERG, O., PELED, D.A., Model checking, MIT, Cambridge, MA, USA, 1999.
COLLINS, G.E., HONG, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. Symb. Comput., 12, 3, pp. 299–328, 1991.
COOK, S.A., Soundness and completeness of an axiom system for program verification, SIAM J. Comput., 7, 1, pp. 70–90, 1978.
DAMM, W., HUNGAR, H., OLDEROG, E.R., Verification of cooperating travel agents, Int. J. Control, 79, 5, pp. 395–421, 2006.
Published
Issue
Section
Copyright (c) 2020 The Romanian Journal of Technical Sciences. Applied Mechanics.
This work is licensed under a Creative Commons Attribution 4.0 International License.