Introduction

The Harmonics Mover software provides strategic decisions in online environments that depend on safety and other verifiable properties. In scenarios that change fast but need to make decisions confidently, our solution is to use Online Model Checking,
combining dependability of formal methods with dynamic responses from defined, rule-based strategies.

The current main application involves the problem of robotic radiation therapy, which we collaborated on together with the Institute of Medical Technology and Intelligent Systems.
Here, a patient is treated via a robot that must deliver radiation doses to a precise location in the body. However, the robot must compensate for the respiratory motion of the patient, which makes the successful and timely delivery of the does challenging. Our solution allows us to deliver the therapy faster than the reference approach while keeping safety concerns.

We describe here the overall workflow and how we implemented it as our Harmonics Mover software. We present the results and products of that research.
 

Explore

For more details on the

• online model checking (OMC) concept and implementation, see checking.
• simulation and implementation, see simulation.
• radiation therapy scenario, see scenario.
• associated models, see models.
• strategic decisions via rulebooks, see rules.

Also have a look at our source code and our paper.
 

Demo

Try our system out by yourself in our demo.
 

Further Information

For further information on the topic, you can read our previous paper on the topic:

Beckers, Lars; Gerlach, Stefan; Lübke, Ole; Schlaefer, Alexander; Schupp, Sibylle
Sliced online model checking for optimizing the beam scheduling problem in robotic radiation therapy
Electronic Proceedings in Theoretical Computer Science, EPTCS 399: 193-209 (2024-04-06)