Logo Institute for Software Systems
Institute for Software Systems
Logo Institute for Software Systems
Institute for Software Systems
EN
DE
Search
EN
DE
Search
More
Online Model Checking
Models
Uppaal
Simulation
Scenario
CommonRoad
Demo
Example
STS > Research > Model Checking & Abstract Interpretation > Simulation > Scenario
| Back to Harmonics Mover Homepage |

The setting of our application is robotic radiation therapy, in which a robot directs multiple beams at a target volume in a human body. These beams are intended to deliver a certain dose of radiation inside the target volume to be effective for therapy. Outside of this volume, the dose should be as low as possible to avoid damage to the patient, e.g. their organs.
A list of beams is composed before a therapy session, which is successful when all beams are delivered. However, this does not require us to observe a particular order of this list. The reference approach tries to optimize the movement time of the executing robot and is also fixed before the session.

Problem Definition

The main problem in this scenario is the respiratory motion of the patient. It consits of varying breathing patterns, but also sudden changes are possible, e.g. coughing.
The patient's movement is not plannable in advance. Thus, it is commonly detected by ultrasound sensors (in graphic: US) during treatment. The robot must compensate the movement without interfering with anything else.

Considering two beams A, and B in the graphic. Both are possible to deliver at first, but beam B would need to be switched off once it interferes with the ultrasound sensor causing the delivery system to wait. Choosing beam B would thus prolong the treatment at this point in time, while beam A could be chosen instead.

Optimization Goals

We characterize this as Beam Scheduling Problem, in which we want to minimize the time beam delivery is inactive due to collisions. Our solution is to create a dynamic list of possible beams in every time slot. We try to continue along the existing list and finish beams that are already started, but insert different beams if necessary.
Checking which beams are feasable at a certain time step is facilitated by our Online Model Checking approach. When multiple beams are possible, we must make a strategic decision, e.g. prefer to continue with the current beam.

In the end, the aim is to provide a successful therapy session, i.e. find a delivery time slot for every beam. This requires strategic foresight, because a shift in the respiratory motion might make it impossible to deliver a beam. At the same time, we only have a short time prediction of the behaviour.

 

 

TU Hamburg
Institute for Software Systems (E-16)
Am Schwarzenberg-Campus 3 (E)
21073 Hamburg
E-mail : sts-office@tuhh.de
Phone : 040-42878-3460
Links
Imprint / Impressum
Privacy / Datenschutz