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

Darius Naujokaitis, Henrikas Pranevicius, Vytautas Pilkauskas, Osvaldas Pranevicius, Mindaugas Pranevicius



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


Patient controlled analgesia; hybrid automata; verification; statistical model checking.

Full Text: PDF


  • There are currently no refbacks.

Print ISSN: 1392-1215
Online ISSN: 2029-5731