UPPAAL SMC model specification

Enviar para

Título:
UPPAAL SMC model specification
Autor: Souvannasouck, Marc
Assuntos: Modelling and simulation
Descrição: Environment Template This UPPAAL SMC template represents an environmental model, named "Env". It uses a clock variable, "ec", to keep track of time within this environment. The template defines a function, "update()", that is used to update the environment. The function sets the clock "ec" back to zero, then adjusts a variable "eff" (which seems to represent some measure of effectiveness) according to certain conditions. If "eff" is greater than or equal to the product of 1 and the difference between 4 and another variable "adh", "eff" is decreased by the product of 1 and the difference between 4 and "adh". If "eff" is greater than 0 but does not meet the previous condition, "eff" is decreased by 1. If "eff" doesn't meet any of these conditions, it remains the same. The template includes a single location with an invariant condition that "ec" must be less than or equal to 9. This means that the system can remain in this location as long as the value of "ec" is less than or equal to 9. A self-loop transition is present in the template, with a guard condition that the transition occurs when "ec" is greater than or equal to 9. When this transition occurs, the "update()" function is called, thus resetting the clock and potentially adjusting "eff". Overall, this template seems to represent a periodic update of the "eff" variable, where the period is determined by the "ec" clock and influenced by the "adh" variable. This could model some sort of environmental influence on the effectiveness of a process. Asthma Flare Template The template uses a clock variable "hc", possibly representing time spent in hospital. It also includes two functions, "light()" and "no_flare()", which return different values based on the state of a variable "p". This could be used to represent different rates of flare occurrences based on the patient's condition severity. The model includes four locations or states: NoFlare, Light, Serious, and Hospital. The initial state is NoFlare, as indicated by the "init" tag. The NoFlare location has an exponential rate label of "8*p". This could be used to represent the time until the next event (i.e., moving to a different state), with higher values of "p" leading to faster transitions. The Light and Serious locations are marked as urgent, which in UPPAAL means that time can't progress in these states, leading to immediate transitions to other states. The Hospital location has an invariant condition that "hc" must be less or equal to 1. This could represent a limit on the duration of a hospital stay. The template also includes various transitions between states. For instance, there's a transition from the Hospital to the NoFlare state if "hc" is greater or equal to 1, with the cost increasing by 3745 (which could represent the cost of a hospital visit). Other transitions are associated with probability expressions, "no_flare()" and "light()", and assignments, such as "sf++" (increasing the serious flare count) and "flares++" (increasing the total flare count). There's also a transition from Serious to Hospital, resetting "hc" to 0, representing the start of a hospital stay. Patient The UPPAAL SMC model outlined above describes a "Patient" template, which is used to represent the condition of a patient with asthma in a simulation. This model captures the dynamics of a patient’s asthma condition over time, as well as their adherence to treatment protocols. The patient’s condition and adherence level can influence the severity of their asthma, which is categorized into four states: Intermittent, Mild, Moderate, and Severe. Firstly, the model defines several clocks such as pc (patient clock in months, with pc=0 indicating the patient is 6 years old), and tp1 through tp4, which measure the time spent in each asthma severity state. The template then describes several locations representing the asthma severity states: Intermittent, Mild, Moderate, and Severe. In each location, the model maintains invariants that ensure the patient can only stay in one state at a time. The branchpoints and transitions in the model represent the changes in the patient’s condition and adherence level over time. These transitions occur based on various factors, such as the time elapsed since the last state change (pc>=1) and the current adherence level. The probability of these transitions is determined by the functions down() and up(), reflecting the dynamic nature of the patient’s condition. Each transition is labeled with an assignment that modifies the patient’s state (p) or adherence level (adh), and a probability that determines how likely this transition is to occur. The model also has initial urgent locations and an init transition which sets the initial conditions of the simulation. This model, while a simplification of real-world dynamics, captures important aspects of pediatric asthma management. It pro- vides a basis for simulating different treatment protocols and understanding how patient adherence and treatment efficacy might impact the progression of the disease. G_Treatment Template At the core of this template are multiple states, namely Step1, Step2, Step3, and Step4, corresponding to the GINA guidelines. The transitions between these steps are governed by the number of asthma flares and the time elapsed since the last treatment adjustment (tracked by the tc clock). The tc clock resets every time a treatment change occurs, reflecting the dynamic nature of asthma management. Each step of the GINA protocol carries distinct costs, determined by monthly averages extracted from realistic data, as supplied by a medical expert and substantiated by resources from the Dutch Healthcare Authority (NZA)1 and the Dutch Pharmacotherapeutic Compass2. These costs, considering the flare frequency associated with each stage, are aggregated cumulatively to the ’cost’ variable. Specifically, costs account for medication expenses related to each step and potential hospitalizations due to severe asthma flares, along with the regular costs of doctor consultations. The transition conditions between the steps, described by the ’guard’ labels, are based on both the number of flares and the tc value. If the conditions are met, the template executes at() function which alters the treatment step (’m’), resets the tc clock, recalculates the cost (’v’), and adds it to the total cost. This function provides an abstract representation of a treatment adjustment in response to the patient’s condition. This template, thus, provides a simplified but valuable abstraction of the dynamic and responsive nature of pediatric asthma treatment, incorporating both the clinical (flares, treatment step) and economic (cost) aspects. MST_Treatment This model consists of two primary states. The first state, associated with a time-invariant condition tc<=1, reflects that it waits one month. Upon the completion of this month, the model transitions to a branchpoint and adds a monthly cost of 50 to the total cost, denoting a constant monthly expense for treatment management. Here we measure the p state of the patient using eHealth [4] with two alternate paths available. One path leads to the ’Check’ state with a probability of 2 (reflecting a 2% chance). In this case, the model doesn’t make any changes to the treatment step. On the other path, taken with a 98% chance, the model equates the current treatment level (’m’) with the patient’s condition (’p’) before proceeding to the ’Check’ state. Once in the ’Check’ state, the model awaits for the tc clock to reach 1 month. Upon this, the model performs a synchronization using check! calling the MST_Check template, and the t() function is executed. This function resets the tc clock, calculates the cost for the treatment level for the next month, and adds it to the total cost. In essence, this template represents a monthly review of the patient’s condition and adjustment of the treatment regimen. It incorporates probabilistic transitions to reflect the inherent uncertainties in patient response and the decision-making process of clinicians. MST_FlareReset This template just resets the flare counter to make MST_Treatment be comparable with G_Treatment. G_Check This template represents the GINA doctor's check. Every six months or if the patient is hospitalized we conduct this check. We add the cost of this check to the total. We modify the eff variable with a probability based on the adherence level of the patient (more adherent => medication is more effective). MST_Check This template represents MST doctor's check. Every month at the MST, the patient's state (p) is measured using eHealth. With 98% it is measured correctly, with 2% it is not and is assumed unchanged.
Editor: figshare
Data de criação/publicação: 2023
Idioma: Inglês

Links

org

UPPAAL SMC model specification

Souvannasouck, Marc

figshare 2023

Buscando em bases de dados remotas. Favor aguardar.