{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:48:37Z","timestamp":1740142117552,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T00:00:00Z","timestamp":1526601600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s11334-018-0315-8","type":"journal-article","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T13:41:13Z","timestamp":1526650873000},"page":"83-100","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal probabilistic analysis of a surgical robot control algorithm with different virtual fixtures"],"prefix":"10.1007","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0452-8457","authenticated-orcid":false,"given":"Muhammad Saad","family":"Ayub","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,18]]},"reference":[{"key":"315_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Courcoubetis C, Henzinger TA, Ho PH (1993) Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Hybrid systems, Springer, Berlin, pp 209\u2013229","DOI":"10.1007\/3-540-57318-6_30"},{"issue":"1","key":"315_CR2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur R, Henzinger TA (1999) Reactive modules. Formal Methods Syst Des 15(1):7\u201348","journal-title":"Formal Methods Syst Des"},{"key":"315_CR3","unstructured":"Ayub MS, Hasan O (2017) Formal probabilistic analysis of a virtual fixture control algorithm for a surgical robot. In: Verification and evaluation of computer and communication systems (VECoS), pp 1\u201316"},{"key":"315_CR4","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge"},{"issue":"3","key":"315_CR5","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1109\/TRO.2007.895077","volume":"23","author":"O Bebek","year":"2007","unstructured":"Bebek O, Cavusoglu MC (2007) Intelligent control algorithms for robotic-assisted beating heart surgery. IEEE Trans Robot 23(3):468\u2013480","journal-title":"IEEE Trans Robot"},{"key":"315_CR6","doi-asserted-by":"crossref","unstructured":"Bresolin D, Guglielmo LD, Geretti L, Muradore R, Fiorini P, Villa T (2012) Open problems in verification and refinement of autonomous robotic systems. In: Euromicro conference on digital system design, pp 469\u2013476","DOI":"10.1109\/DSD.2012.96"},{"key":"315_CR7","doi-asserted-by":"crossref","unstructured":"Fainekos GE, Gazit HK, Pappas GJ (2005) Temporal logic motion planning for mobile robots. In: Robotics and automation, pp 2020\u20132025","DOI":"10.1109\/ROBOT.2005.1570410"},{"key":"315_CR8","volume-title":"Introduction to probability","author":"CM Grinstead","year":"1997","unstructured":"Grinstead CM, Snell JL (1997) Introduction to probability. American Mathematical Soc, Providence"},{"key":"315_CR9","unstructured":"Groote JF, Mateescu R (1999) Verification of temporal properties of processes in a setting with data. In: Algebraic methodology and software technology (AMAST), pp 74\u201390"},{"key":"315_CR10","volume-title":"The formal specification language mCRL2","author":"JF Groote","year":"2007","unstructured":"Groote JF, Mathijssen A, Reniers M, Usenko Y, Weerdenburg MV (2007) The formal specification language mCRL2. Citeseer, University Park"},{"key":"315_CR11","doi-asserted-by":"crossref","unstructured":"Hahn EM, Hermanns H, Wachter B, Zhang L (2009) Infamy: an infinite-state Markov model checker. In: Computer aided verification, pp 641\u2013647","DOI":"10.1007\/978-3-642-02658-4_49"},{"key":"315_CR12","doi-asserted-by":"crossref","unstructured":"Hahn EM, Hermanns H, Wachter B, Zhang L (2010) Param: a model checker for parametric Markov models. In: Computer aided verification, pp 660\u2013664","DOI":"10.1007\/978-3-642-14295-6_56"},{"key":"315_CR13","doi-asserted-by":"crossref","unstructured":"Hahn EM, Hermanns H, Wachter B, Zhang L (2010) Pass: abstraction refinement for infinite probabilistic models. In: Tools and algorithms for the construction and analysis of systems, pp 353\u2013357","DOI":"10.1007\/978-3-642-12002-2_30"},{"key":"315_CR14","doi-asserted-by":"crossref","unstructured":"Haidegger T, Beny\u00f3 B, Kov\u00e1cs L, Beny\u00f3 Z (2009) Force sensing and force control for surgical robots. In: Symposium on modeling and control in biomedical systems, pp. 401\u2013406","DOI":"10.3182\/20090812-3-DK-2006.0035"},{"key":"315_CR15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of practical logic and automated reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press, Cambridge"},{"key":"315_CR16","first-page":"7162","volume-title":"Formal verification methods. Encyclopedia of information science and technology","author":"O Hasan","year":"2014","unstructured":"Hasan O, Tahar S (2014) Formal verification methods. Encyclopedia of information science and technology. IGI Global, Hershey, pp 7162\u20137170"},{"issue":"3","key":"315_CR17","doi-asserted-by":"publisher","first-page":"1035","DOI":"10.1109\/JSYST.2014.2331146","volume":"10","author":"T Hassan","year":"2016","unstructured":"Hassan T, Hameed A, Nasir S, Kamal N, Hasan O (2016) Al-zahrawi: a telesurgical robotic system for minimal invasive surgery. IEEE Syst J 10(3):1035\u20131045","journal-title":"IEEE Syst J"},{"key":"315_CR18","unstructured":"Jeannet B, Argenio PD, Larsen K (2002) Rapture: A tool for verifying Markov decision processes. In: Concurrency theory (CONCUR), p 149"},{"key":"315_CR19","unstructured":"Jeannet B, DArgenio P, Larsen K (2010) Fortuna: model checking priced probabilistic timed automata. In: Quantitative evaluation of systems, pp 273\u2013281"},{"key":"315_CR20","doi-asserted-by":"crossref","unstructured":"Kazanzides P, Zuhars J, Mittelstadt B, Taylor RH (1992) Force sensing and control for a surgical robot. In: Robotics and automation, pp 612\u2013617","DOI":"10.1109\/ROBOT.1992.220224"},{"key":"315_CR21","unstructured":"Kim M, Kang KC, Lee H (2005) Formal verification of robot movements-a case study on home service robot shr100. In: Robotics and automation, pp 4739\u20134744"},{"key":"315_CR22","doi-asserted-by":"crossref","unstructured":"Kouskoulas Y, Renshaw D, Platzer A, Kazanzides P (2013) Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Hybrid systems: computation and control, pp 263\u2013272","DOI":"10.1145\/2461328.2461369"},{"key":"315_CR23","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Computer aided verification, pp 585\u2013591"},{"key":"315_CR24","doi-asserted-by":"crossref","unstructured":"Lahijanian M, Wasniewski J, Andersson SB, Belta C (2010) Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees. In: Robotics and automation, pp 3227\u20133232","DOI":"10.1109\/ROBOT.2010.5509686"},{"key":"315_CR25","doi-asserted-by":"crossref","unstructured":"Li L, Shi Z, Guan Y, Zhao C, Zhang J, Wei H (2014) Formal verification of a collision-free algorithm of dual-arm robot in hol4. In: Robotics and automation (ICRA), pp 1380\u20131385","DOI":"10.1109\/ICRA.2014.6907032"},{"key":"315_CR26","unstructured":"Mika\u00ebl L (2012) Formal verification of flexibility in swarm robotics. Thesis, Department of Computer Science, Universit libre de Bruxelles"},{"key":"315_CR27","unstructured":"Norman G, Parker D (2014) Quantitative verification: formal guarantees for timeliness, reliability and performance. Technical report, The London Mathematical Society and the Smith Institute"},{"key":"315_CR28","unstructured":"Oldenkamp HA (2007) Probabilistic model checking: a comparison of tools. Master\u2019s thesis, University of Twente, Enschede, Netherlands"},{"key":"315_CR29","doi-asserted-by":"crossref","unstructured":"Platzer A, Quesel JD (2008) Keymaera: a hybrid theorem prover for hybrid systems (system description). In: Automated reasoning, Springer, pp 171\u2013178","DOI":"10.1007\/978-3-540-71070-7_15"},{"key":"315_CR30","doi-asserted-by":"crossref","unstructured":"Rosenberg LB (1993) Virtual fixtures: perceptual tools for telerobotic manipulation. In: Virtual reality annual international symposium, pp 76\u201382","DOI":"10.1109\/VRAIS.1993.380795"},{"key":"315_CR31","doi-asserted-by":"crossref","unstructured":"Saberi AK, Groote JF, Keshishzadeh S (2013) Analysis of path planning algorithms: a formal verification-based approach. In: Robotics and automation ICRA, pp 232\u2013239","DOI":"10.7551\/978-0-262-31709-2-ch035"},{"key":"315_CR32","unstructured":"Scherer S, Lerda F, Clarke EM (2005) Model checking of robotic control systems. In: International symposium on artificial intelligence, robotics and automation in space (i-SAIRAS), pp 5\u20138"},{"key":"315_CR33","unstructured":"Webster M, Dixon C, Fisher M, Salem M, Saunders J, Koay K, Dautenhahn K (2014) Formal verification of an autonomous personal robotic assistant. In: Papers from the AAAI spring symposium (FVHMS 2014) on formal verification and modeling in human\u2013machine systems, pp 74\u201379"},{"key":"315_CR34","unstructured":"Whitcomb L, Yoerger D, Singh H, Howland J (1999) Advances in underwater robot vehicles for deep ocean exploration: navigation, control, and survey operations. In: International symposium on robotics research navigation, control and survey operations, pp 346\u2013353"},{"key":"315_CR35","doi-asserted-by":"crossref","unstructured":"Wulf D, M, Doyen L, Raskin JF (2004) Almost ASAP semantics: from timed models to timed implementations. In: Hybrid systems: computation and control, Springer, pp 296\u2013310","DOI":"10.1007\/978-3-540-24743-2_20"},{"issue":"4","key":"315_CR36","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1002\/rcs.213","volume":"4","author":"T Xia","year":"2008","unstructured":"Xia T, Baird C, Jallo G, Hayes K, Nakajima N, Hata N, Kazanzides P (2008) An integrated system for planning, navigation and robotic assistance for skull base surgery. J Med Robot Comput Assist Surg 4(4):321\u2013330","journal-title":"J Med Robot Comput Assist Surg"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-018-0315-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-018-0315-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-018-0315-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T21:55:31Z","timestamp":1558130131000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-018-0315-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,18]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["315"],"URL":"https:\/\/doi.org\/10.1007\/s11334-018-0315-8","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2018,5,18]]},"assertion":[{"value":"7 April 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 May 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 May 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}