ON THE DIFFERENTIAL DYNAMIC LOGIC MODEL FOR HYBRID SYSTEMS

Veturia CHIROIU, Ligia MUNTEANU, Ciprian DRAGNE, Cristina STIRBU

Abstract


The contribution of this paper consists in advancing of a control strategy based on the differential dynamic logic (dL) for a cooperative surgeon-robot system whose behavior depends on the interaction between discrete dynamics deriving from the control and continuous dynamics deriving from surgical instrument moving. Such systems are called hybrid systems. The dL algorithm captures the logics of superposition of both dynamics and is capable to control the system in the most natural way. In our opinion, dL can be successfully used for avoiding the collisions of the surgical instrument with a critical domain in a virtual system composed by a surgical robot, a device for visualizing and analyzing the medical images and a six degree-of-freedom robotic arm designed for use in hepatic surgery.

Key words: Differential logic control; Hybrid systems; Surgical robotics; Collision avoidance.

Full Text:

PDF

References


Platzer, A., Differential dynamic logics. Automated theorem proving fir hybrid systems, PhD Thesis, Carl Von Ossientzky Universitat Oldenburg, 2008.

Platzer, A., Differential dynamic logic for hybrid systems, J. Autom. Reasoning, 41(2), 143–189, 2008.

Platzer, A., Quesel, J.D., Keymaera: A hybrid theorem prover for hybrid systems, in: Automated Reasoning, 4th Int. Joint Conf., vol. 5195, A. Armando, P. Baumgartner and G. Dowek (eds.), pp.171-178, 2008, Springer Verlag, Berlin Heidelberg.

Platzer, A., Clarke, E.M., Computing differential invariants of hybrid systems as fixed points, in: Gupta and Malik, Computer Aided Verification, CAV 2008, vol.5123, pp.176-189, 2008, Princeton, Springer, Berlin Heidelberg.

Platzer, A., Clarke, E.M., Computing differential invariants of hybrid systems as fixed points, Formal Methods in System Design 35(1), 98–120, 2009.

Platzer, A., Logical analysis of hybrid systems- proving theorems for complex dynamics, 2010, Springer Verlag, Berlin Heidelberg.

Platzer, A., A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems, Logical Methods in Computer Science, 8(4), 1–44, 2012.

Franzle, M., Herde, C., Hysat - An efficient proof engine for bounded model checking of hybrid systems, Formal Methods in System Design, 30(2), 179–198, 2007.

Kouskoulas, Y., Renshaw, D., Platzer, A., Kazanzides, P., Certifying the safe design of a virtual fixture control algorithm for a surgical robot, in: Proc. 16th International Conf. on Hybrid Systems: Computation and Control, 263–272, 2013.

Kazanzides, P., Virtual Fixture Computation, Note on Combining the Effects of Multiple Virtual Fixtures, 2011.

Kouskoulas, Y., Platzer, A., Kazanzides, P., Formal methods for robotic system control software, Johns Hopkins Appl. Technical Digest, 32(2), 490-498, 2013.

Eppinger, S., Seering, W., Understanding bandwidth limitations in robot force control, Proceeding IEEE International Conference on Robotics and Automation, 1987.

Pisla, D., Birlescu, I., Vaida, C., Tucan, P., Pisla, A., Gherman, B., Crisan, N., Plitea, N., Algebraic modeling of kinematics and singularities for a prostate biopsy parallel robot, Proceedings of the Romanian Academy, series A, 19(3) 489-497, 2018

Chiroiu, V., Munteanu, L., Rugina, C., On the control of a cooperatively robotic system by using a hybrid logic algorithm, Proceedings of the Romanian Academy, series A, 2018 (in press).

Munteanu, L., Brisan, C., Chiroiu, V., Donescu, St., A 3D model for tire/road dynamic contact, Acta Technica Napocensis, Series: Applied Mathematics and mechanics, 55(3), 611–614, 2012.

Munteanu, L., Chiroiu, V., Brişan, C., Dumitriu, D., Sireteanu, T., Petre, S., On the 3D normal tire/off-road vibro-contact problem with friction, Mechanical Systems and Signal Processing, 54-55, 377-393, 2014.

Gilardi, G., Sharf, I., Literature survey of contact dynamics modelling, Mechanism and Machine Theory, 37, 1213–1239, 2002.

Avramescu, C., Sisteme diferentiale cu conditii la limita generale, Bul. Inst. Politehn., Iasi, 11, 35-42, 1965.

Lang, H., Hindennach, M., Radtke, A., Peitgen, H.O., Virtual Liver Surgery: Computer-assisted operation planning in 3D liver model, in Renzo Dionigi, Recent advances in liver surgery, Chapter 5, Landes Bioscience, Austin, Texas, USA, 2009.


Refbacks

  • There are currently no refbacks.


JOURNAL INDEXED IN :