Utility of Statistical Model Checking of Stochastic Hybrid Automata for Patient Controlled Analgesia

  • Darius Naujokaitis Kauno Technologijos Universitetas
  • Henrikas Pranevicius
  • Vytautas Pilkauskas
  • Osvaldas Pranevicius
  • Mindaugas Pranevicius
Keywords: Patient controlled analgesia, hybrid automata, verification, statistical model checking.



Opiate concentration in the effect compartment of the brain (OCEC) determines both, the pain control and the side effects. This concentration can be estimated using pharmacodynamics models; however, these models do not predict OCEC when delivery of the drug is random.We are proposing to use stochastic hybrid automata for the verification of individualized model of patient’s drug demands and model of patient’s pharmacokinetics for the estimation of OCEC, and to express results as the probability of falling below the minimum effective analgesic concentration (MEAC) and/or probability of exceeding toxic concentration threshold. Patient controlled analgesia (PCA) model was based on the stochastic hybrid automata, while the verification of the model was done using UPPALL-SMC tool. The suggested approach allowed for quantitative prediction of the OCEC.

DOI: http://dx.doi.org/10.5755/j01.eie.23.6.17572

Author Biography

Darius Naujokaitis, Kauno Technologijos Universitetas
Faculty of Informatics,Department of Applied Informatics,Lecturer