STS: Models

STS > Research > Model Checking & Abstract Interpretation > Online Model Checking > Models

Models

For Online Model Checking, we require relatively simple models that can be queried within a short time period.
Specifically, we use Statistical Model Checking (SMC) to obtain non-guaranteed, but rankable answers.
For our radiation therapy application, we use a model that describes the sine wave of the primary respiratory motion axis of a patient.
We then query this model with which probability a certain distance is not exceeded within the time window of interest.

You can jump directly to the resulting automata model or follow the process step by step:

Base formula

This is the sum formula that represents the respiratory motion that we want to model. The sum formula combines four smaller curves into a prediction curve. The parameters are derived from observed movements via sensors that are decomposed using a standard method.

Formula values

Here you see the respiration movement together with the period and base values. The period and base values are primary parameters of the resulting curve. The period is used in the sum formula as frequency and the base is a global offset.

Partial Curves

This plot shows you an overlay of multiple models, overlapping each other slightly, each with a prediction curve that resembles the respiration. Further, each has four additional, smaller curves that summed together form the prediction curve. The smaller curves are the parts of the sum formula, while the prediction curve is the overall result.

Prediction curve

In this plot you can see the repiration movement and the prediction of this movement. You can see that the prediction lines overlap slightly, and thus are able to cover the movement continuously. A new prediction curve starts at the moment a new model is generated, marked with dots.

Network of Timed Automata

Here, you can see the Network of Timed Automata (NTA) that comprise this model. The "FSTerm" and "Summer" automata provide the formula that is evaluated to get the sine wave of the motion. The "result" is the position on the motion axis at a certain point in time. The point in time is stepped forward by the aplty named "Timer".

Additionally, two more automata introduce randomization into the parameters of the core formula to model uncertainty of the real movement. As you can see, the model itself is quite simple. However, it also has a 'program code' side to it, which defines the various parameters mentioned in the formulas. These are the frequency ("f") of the wave, its "base" level compared to zero, multiple sine ("s") and cosine ("c") factors, a "drift" factor over time, and an uncertainty ("rate") level.

Here you see the respiration movement together with a period and a base value. The curves from previous plots are represented by values and the formula is part of the model.

Uncertainty

The modeled uncertainty is meant to cover only normal variations within the motion.
Sudden changes to a completely different level are not predictable in this way, because these would be not well descibed using the existing sine wave. Considering the goal of our scenario, limiting the queries to a guaranteed safe distance would be useless, because then some therapy goals are not achiveable.

The online approach is instead intended to cover us for this case by design.
A certain model is only used for a short period of time before it is superseded by a new model.
The continued updates with new sensor data provide the full picture of motion together and thus we quickly receive updated results and changed decisions when changes occur.

This plot shows why adding uncertainty is necessary. You can see two changes in the general motion. At these changes, the newly generated model is not able to predict the motion accurately. Since the changes are rather small (cf. y axis) and the respiration is over approximated, this is not yet critical. However, model checking allows us to not only cover a single path, but a region of possible paths.

Data

While the uncertainty is set by the user, the rest are data that is set by sensor information. Templating this data into a model is a core part of our online process. On the bottom of this page you see a plot of that data from a part of a simulated session.

What do I see here?

The plot shows the values (Y axis) changing over time (X axis) for every newly templated instance of a model.
In this session, a new model was created every three seconds.
The values of one model are variables in a mathematical equation of the respiratory motion in its current state.
Note that these values do not share the same units.

The values are:

the period of the wave,
its base height,
the sine (s0, ...) and cosine (c0, ...) factors,
and the expected drift of the result.

Further, we provide our computed minimum and maximum expected position of the patient.

How do I interact?

You can click and hold and draw a rectangle to zoom into the plot to make a smaller timeframe more visible.
You can also click on the values in the legend on the side to remove those from the plot.

What can I observe?

Even though the actual motion data is not visible, you can recognize and differentiate times of steady motion and large shifts.

The period and base are a coarse description of the current position of the patient.
The sine and cosine factors and the drift are not informative on first sight.
If you zoom in at the beginning, you can observe a relatively steady motion.
If you zoom in in the middle, you can observe a shift to a different base line. This would not be predictable by data until that point.
You can also observe different breathing depth if you compare between consecutive data points.
The base height is in between the minimum and maximum expected position.

More