Formal Verification of Basal Ganglia Model (BGM) of Brain using UPPAAL

Abstract

Parkinson’s disease (PD) is a neurological disorder that affects dopaminergic nerve cells in a specific area of brain called substantia nigra. PD symptoms include muscle rigidity, tremors, and changes in speech and gait. There is no cure for PD but surgical treatments, i.e., Deep Brain Stimulation (DBS), can help in relieving PD symptoms. Traditionally, DBS is done in an open-loop manner, where stimulation/pacing is always ON, irrespective of the patient need. As a consequence, patients can feel some side effects due to the con tinuous high frequency stimulation. Therefore, closed-loop DBS is preferred as it allows adjusting stimulation according to the patient need, and it con sumes less power as compared to open-loop DBS. However, selection of an appropriate biomarker for closing the feedback loop is a major challenge in close-loop DBS. In this thesis, we propose to utilize model checking, i.e., a formal verification technique used to exhaustively explore the complete state space of a system, for analyzing DBS controllers. We model the basal ganglia (BG) region from hybrid automaton to timed automata using timed abstrac tion. Thereafter, we analyze the timed automata of the closed-loop DBS controller in response to the BG model. Furthermore, we formally verified the closed-loop DBS using timed computation tree logic (TCTL) properties, i.e., safety, liveness and deadlock. We show that closed-loop DBS significantly outperforms existing open-loop DBS controller in terms of energy efficiency. In order to demonstrate the practical effectiveness of our work, we formally analyze the closed-loop DBS for power efficiency and time behavior with two different algorithms, i.e., Algorithms A and B. Our results demonstrate that the closed-loop DBS running the Algorithm B is efficient in terms of time and power as compared to Algorithm A but stability is not always guaranteed in Algorithm B.