{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T04:53:33Z","timestamp":1749099213892},"reference-count":29,"publisher":"MIT Press","issue":"4","content-domain":{"domain":["direct.mit.edu"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,3,18]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Deep brain stimulation (DBS) is a widely accepted treatment for the Parkinson's disease (PD). Traditionally, it is done in an open-loop manner, where stimulation is always ON, irrespective of the patient needs. As a consequence, patients can feel some side effects due to the continuous high-frequency stimulation. Closed-loop DBS can address this problem as it allows adjusting stimulation according to the patient need. The selection of open- or closed-loop DBS and an optimal algorithm for closed-loop DBS are some of the main challenges in DBS controller design, and typically the decision is made through sampling based simulations. In this letter, we used model checking, a formal verification technique used to exhaustively explore the complete state space of a system, for analyzing DBS controllers. We analyze the timed automata of the open-loop and closed-loop DBS controllers in response to the basal ganglia (BG) model. Furthermore, we present a formal verification approach for the closed-loop DBS controllers using timed computation tree logic (TCTL) properties, that is, safety, liveness (the property that under certain conditions, some event will eventually occur), and deadlock freeness. We show that the closed-loop DBS significantly outperforms existing open-loop DBS controllers in terms of energy efficiency. Moreover, we formally analyze the closed-loop DBS for energy efficiency and time behavior with two algorithms, the constant update algorithm and the error prediction update algorithm. Our results demonstrate that the closed-loop DBS running the error prediction update algorithm is efficient in terms of time and energy as compared to the constant update algorithm.<\/jats:p>","DOI":"10.1162\/neco_a_01569","type":"journal-article","created":{"date-parts":[[2023,2,24]],"date-time":"2023-02-24T20:25:41Z","timestamp":1677270341000},"page":"671-698","update-policy":"http:\/\/dx.doi.org\/10.1162\/mitpressjournals.corrections.policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of Deep Brain Stimulation Controllers for Parkinson's Disease Treatment"],"prefix":"10.1162","volume":"35","author":[{"given":"Arooj","family":"Nawaz","sequence":"first","affiliation":[{"name":"School of Electrical Engineering and Computer Science, National University of Sciences and Technology, Islamabad 44000, Pakistan arooj.nawaz@seecs.edu.pk"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[{"name":"School of Electrical Engineering and Computer Science, National University of Sciences and Technology, Islamabad 44000, Pakistan osman.hasan@seecs.edu.pk"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaista","family":"Jabeen","sequence":"additional","affiliation":[{"name":"Electrical and Computer Engineering Department, COMSATS University, Islamabad 45550, Pakistan shaista.sj@comsats.edu.pk"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"281","published-online":{"date-parts":[[2023,3,18]]},"reference":[{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-319-91908-9","article-title":"Continuous-time models for system design and analysis","volume":"10000","author":"Alur","year":"2019","journal-title":"Computing and software science"},{"issue":"2","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1002\/spe.1006","article-title":"Developing UPPAAL over 15 years","volume":"41","author":"Behrmann","year":"2011","journal-title":"Software: Practice and Experience"},{"issue":"6","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1016\/j.conb.2003.11.001","article-title":"Deep brain stimulation for Parkinson's disease","volume":"13","author":"Benabid","year":"2003","journal-title":"Current Opinion in Neurobiology"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1016\/j.neuroimage.2013.05.084","article-title":"Oscillations and the basalganglia: Motor control and beyond","volume":"85","author":"Brittain","year":"2014","journal-title":"NeuroImage"},{"issue":"1","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1093\/brain\/aww286","article-title":"Stimulating at the right time: Phase-specific deep brain stimulation","volume":"140","author":"Cagnan","year":"2017","journal-title":"Brain"},{"issue":"3","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1002\/mds.870130306","article-title":"The health burdens of Parkinson's disease","volume":"13","author":"Chrischilles","year":"1998","journal-title":"Movement Disorders"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","article-title":"NUSMV: A new symbolic model checker","author":"Cimatti","year":"2000","journal-title":"International Journal on Software Tools for Technology Transfer, 2"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","DOI":"10.3389\/fnint.2016.00017","article-title":"Mental side effects of deep brain stimulation (DBS) for movement disorders: The futility of denial","volume":"10","author":"Cyron","year":"2016","journal-title":"Frontiers in Integrative Neuroscience"},{"issue":"6","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1016\/S1474-4422(06)70471-9","article-title":"Epidemiology of Parkinson's disease","volume":"5","author":"de Lau","year":"2006","journal-title":"Lancet Neurology"},{"issue":"S14","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1002\/mds.20957","article-title":"Deep brain stimulation: Postoperative issues","volume":"21","author":"Deuschl","year":"2006","journal-title":"Movement Disorders"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1016\/j.parkreldis.2007.06.003","article-title":"The economic impact of Parkinson's disease","volume":"13","author":"Findley","year":"2007","journal-title":"Parkinsonism and Related Disorders"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS48487.2020.00018","article-title":"Model-based design of closed loop deep brain stimulation controller using reinforcement learning","volume-title":"Proceedings of the 2020 ACM\/IEEE 11th International Conference on Cyber-Physical Systems","author":"Gao","year":"2020"},{"key":"2023032023153457000_","article-title":"Formal verification methods","volume-title":"Encyclopedia of information science and technology","author":"Hasan","year":"2015"},{"issue":"1","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/j.nec.2013.08.006","article-title":"Creating the feedback loop: Closed-loop neurostimulation","volume":"25","author":"Hebb","year":"2014","journal-title":"Neurosurgery Clinics of North America"},{"issue":"4","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1113\/jphysiol.1952.sp004764","article-title":"A quantitative description of membrane current and its application to conduction and excitation in nerve","volume":"117","author":"Hodgkin","year":"1952","journal-title":"Journal of Physiology"},{"key":"2023032023153457000_","volume-title":"The SPIN model checker: Primer and reference manual","author":"Holzmann","year":"2003"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1136\/jnnp.2007.131045","article-title":"Parkinson's disease: Clinical features and diagnosis","volume":"79","author":"Jankovic","year":"2008","journal-title":"Journal of Neurology, Neurosurgery, and Psychiatry"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1109\/ICCPS.2018.00033","article-title":"Platform for model-based design and testing for deep brain stimulation","volume-title":"Proceedings of the 2018 ACM\/IEEE 9th International Conference on Cyber-Physical Systems","author":"Jovanov","year":"2018"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1038\/s41582-020-00426-z","article-title":"Technology of deep brain stimulation: Current status and future directions","volume":"17","author":"Krauss","year":"2021","journal-title":"Nature Review. Neurology"},{"issue":"11","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"2431","DOI":"10.1016\/j.clinph.2004.05.031","article-title":"Selection of stimulus parameters for deep brain stimulation","volume":"115","author":"Kuncel","year":"2004","journal-title":"Clinical Neurophysiology"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1109\/LICS.2003.1210075","article-title":"Model checking for probability and time: From theory to practice","volume-title":"Proceedings of the 8th Annual IEEE Symposium of Logic in Computer Science","author":"Kwiatkowska","year":"2003"},{"key":"2023032023153457000_","volume-title":"Parkinson's disease: National clinical guideline for diagnosis and management in primary and secondary care.","author":"National Collaborating Centre for Chronic Conditions","year":"2006"},{"issue":"14","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"1356","DOI":"10.1056\/NEJM2003ra020003","article-title":"Alzheimer's disease and Parkinson's disease","volume":"348","author":"Nussbaum","year":"2003","journal-title":"New England Journal of Medicine"},{"issue":"16","key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"1529","DOI":"10.1056\/NEJMct1208070","article-title":"Deep-brain stimulation for Parkinson's disease","volume":"367","author":"Okun","year":"2012","journal-title":"New England Journal of Medicine"},{"issue":"1","key":"2023032023153457000_","doi-asserted-by":"publisher","DOI":"10.1186\/s12984-017-0295-1","article-title":"Advances in closed-loop deep brain stimulation devices","volume":"14","author":"Parastarfeizabadi","year":"2017","journal-title":"Journal of Neuroengineering and Rehabilitation"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"2240","DOI":"10.1093\/brain\/awh571","article-title":"Bilateral deep brain stimulation in Parkinson's disease: A multicentre study with 4 years follow-up","volume":"128","author":"Rodriguez-Oroz","year":"2005","journal-title":"Brain"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","DOI":"10.3389\/fnins.2016.00119","article-title":"Proceedings of the Third Annual Deep Brain Stimulation Think Tank: A review of emerging issues and technologies","volume":"10","author":"Rossi","year":"2016","journal-title":"Frontiers in Neuroscience"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","DOI":"10.3389\/fnins.2019.00956","article-title":"Model-based evaluation of closed-loop deep brain stimulation controller to adapt to dynamic changes in reference signal","volume":"13","author":"Su","year":"2019","journal-title":"Frontiers in Neuroscience"},{"key":"2023032023153457000_","doi-asserted-by":"publisher","first-page":"1328","DOI":"10.1109\/TNSRE.2021.3095316","article-title":"An embedded multi-core real-time simulation platform of basal ganglia for deep brain stimulation","volume":"29","author":"Wei","year":"2021","journal-title":"IEEE Transactions on Neural Systems and Rehabilitation Engineering"}],"container-title":["Neural Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/direct.mit.edu\/neco\/article-pdf\/35\/4\/671\/2075292\/neco_a_01569.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/direct.mit.edu\/neco\/article-pdf\/35\/4\/671\/2075292\/neco_a_01569.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,20]],"date-time":"2023-03-20T23:15:48Z","timestamp":1679354148000},"score":1,"resource":{"primary":{"URL":"https:\/\/direct.mit.edu\/neco\/article\/35\/4\/671\/114871\/Formal-Verification-of-Deep-Brain-Stimulation"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,18]]},"references-count":29,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2023,3,18]]},"published-print":{"date-parts":[[2023,3,18]]}},"URL":"https:\/\/doi.org\/10.1162\/neco_a_01569","relation":{},"ISSN":["0899-7667","1530-888X"],"issn-type":[{"value":"0899-7667","type":"print"},{"value":"1530-888X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2023,4]]},"published":{"date-parts":[[2023,3,18]]}}}