The main simulation runs within the Server component, which is requested (1) for and thus supplies (5) the next decision in the procedure control. In the real world, the Client would be the robot that executes the procedure. While testing, this can be substituted by data files and interactive user input. The Server component then interacts (2) with the OMC component that templates (3) new model instances based on the current sensor data and the underlying Model Checker, here UPPAAL.
Using the Online Model Checking approach, we have model instances that describe the respiratory motion within a short time period. Thus, we know the current position, but use (4) the model (and in turn its underlying formula) to estimate future steps of our simulation.
In principle, the executing robot can change its operation in every step, but this would be very suboptimal.
Strategies
In order to select the best possible course of action, we provide multiple different strategies.These consist of specialised pre-selection approaches for prioritizing model checking queries and of different sets of rules.
Rules use the available information of both the position and model information, as well as query results to signal preference for a particular choice in the next step.
The choice that a rule would make is weighted, for example based on its safety distance violation probability.
The robot then executes the choice, e.g. staying with the same or changing to a different radiation beam in the therapy procedure. The rulesets are customisable based on the included rules and associated priorities.
A simulation is completed when either the procedure time window has ended or all goals have been completed.
Here, a goal is the complete application of a radiation beam within its safety distance. Completing all goals is thus a successful therapy session. In each step of the simulation, only one goal is pursued, but they can be pursued in any order, and even be paused in between.
In the therapy scenario, it is desirable to complete the session as early as possible. A secondary concern is to switch and pause goals as less as possible, since this is not completely free and finely controlled in reality. We can compare different strategies in the same testing scenario by its statistics w.r.t these measures.The software allows us in interactive testing to view multiple different strategies at the same time.
