Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Sliced Online Model Checking for Optimizing the Beam Scheduling Problem in Robotic Radiation Therapy

Lars Beckers, Stefan Gerlach, Ole Lübke, Alexander Schlaefer, Sibylle Schupp

TL;DR

The paper tackles motion-induced delays in robotic radiation therapy by introducing Online Model Checking (OMC) to dynamically verify and select feasible beams in real time. It employs a 1D sinusoidal-based motion model and extends to a synchronized set of three parallel 1D models to represent 3D respiration, with Uppaal-SMC used for probabilistic beam verification within short time horizons. Key contributions include a verified beam-scheduling approach, a synchronized 3D modeling framework, and a Rust/Uppaal-based implementation with real and synthetic data; results show idle-time reductions of up to 37.21% without compromising target coverage, compared to a static beam schedule, while a naive ML approach underperforms. The work demonstrates the practical potential of online model checking for safe, time-sensitive beam delivery and lays groundwork for future AI-guided refinements in motion prediction and verification timing.

Abstract

In robotic radiation therapy, high-energy photon beams from different directions are directed at a target within the patient. Target motion can be tracked by robotic ultrasound and then compensated by synchronous beam motion. However, moving the beams may result in beams passing through the ultrasound transducer or the robot carrying it. While this can be avoided by pausing the beam delivery, the treatment time would increase. Typically, the beams are delivered in an order which minimizes the robot motion and thereby the overall treatment time. However, this order can be changed, i.e., instead of pausing beams, other feasible beam could be delivered. We address this problem of dynamically ordering the beams by applying a model checking paradigm to select feasible beams. Since breathing patterns are complex and change rapidly, any offline model would be too imprecise. Thus, model checking must be conducted online, predicting the patient's current breathing pattern for a short amount of time and checking which beams can be delivered safely. Monitoring the treatment delivery online provides the option to reschedule beams dynamically in order to avoid pausing and hence to reduce treatment time. While human breathing patterns are complex and may change rapidly, we need a model which can be verified quickly and use approximation by a superposition of sine curves. Further, we simplify the 3D breathing motion into separate 1D models. We compensate the simplification by adding noise inside the model itself. In turn, we synchronize between the multiple models representing the different spatial directions, the treatment simulation, and corresponding verification queries. Our preliminary results show a 16.02 % to 37.21 % mean improvement on the idle time compared to a static beam schedule, depending on an additional safety margin. Note that an additional safety margin around the ultrasound robot can decrease idle times but also compromises plan quality by limiting the range of available beam directions. In contrast, the approach using online model checking maintains the plan quality. Further, we compare to a naive machine learning approach that does not achieve its goals while being harder to reason about.

Sliced Online Model Checking for Optimizing the Beam Scheduling Problem in Robotic Radiation Therapy

TL;DR

The paper tackles motion-induced delays in robotic radiation therapy by introducing Online Model Checking (OMC) to dynamically verify and select feasible beams in real time. It employs a 1D sinusoidal-based motion model and extends to a synchronized set of three parallel 1D models to represent 3D respiration, with Uppaal-SMC used for probabilistic beam verification within short time horizons. Key contributions include a verified beam-scheduling approach, a synchronized 3D modeling framework, and a Rust/Uppaal-based implementation with real and synthetic data; results show idle-time reductions of up to 37.21% without compromising target coverage, compared to a static beam schedule, while a naive ML approach underperforms. The work demonstrates the practical potential of online model checking for safe, time-sensitive beam delivery and lays groundwork for future AI-guided refinements in motion prediction and verification timing.

Abstract

In robotic radiation therapy, high-energy photon beams from different directions are directed at a target within the patient. Target motion can be tracked by robotic ultrasound and then compensated by synchronous beam motion. However, moving the beams may result in beams passing through the ultrasound transducer or the robot carrying it. While this can be avoided by pausing the beam delivery, the treatment time would increase. Typically, the beams are delivered in an order which minimizes the robot motion and thereby the overall treatment time. However, this order can be changed, i.e., instead of pausing beams, other feasible beam could be delivered. We address this problem of dynamically ordering the beams by applying a model checking paradigm to select feasible beams. Since breathing patterns are complex and change rapidly, any offline model would be too imprecise. Thus, model checking must be conducted online, predicting the patient's current breathing pattern for a short amount of time and checking which beams can be delivered safely. Monitoring the treatment delivery online provides the option to reschedule beams dynamically in order to avoid pausing and hence to reduce treatment time. While human breathing patterns are complex and may change rapidly, we need a model which can be verified quickly and use approximation by a superposition of sine curves. Further, we simplify the 3D breathing motion into separate 1D models. We compensate the simplification by adding noise inside the model itself. In turn, we synchronize between the multiple models representing the different spatial directions, the treatment simulation, and corresponding verification queries. Our preliminary results show a 16.02 % to 37.21 % mean improvement on the idle time compared to a static beam schedule, depending on an additional safety margin. Note that an additional safety margin around the ultrasound robot can decrease idle times but also compromises plan quality by limiting the range of available beam directions. In contrast, the approach using online model checking maintains the plan quality. Further, we compare to a naive machine learning approach that does not achieve its goals while being harder to reason about.
Paper Structure (14 sections, 2 equations, 20 figures)

This paper contains 14 sections, 2 equations, 20 figures.

Table of Contents

  1. Introduction
  2. Ultrasound Guided Motion Compensated Radiation Therapy
  3. Online Model Checking
  4. Modeling
  5. 1D motion modeling
  6. 3D motion modeling
  7. Beam verification
  8. Data
  9. Beam Checking Application
  10. Experiments
  11. AI Enhancements
  12. Summary
  13. Model declarations
  14. Evaluation model

Figures (20)

  • Figure 1: Illustration of the situation we consider. Figure a) shows the the general setup with the patient and the robot mounted ultrasound (US) transducer, as well as the target which moves along the patient's superior-inferior axis. Figure b) depicts a position of the target where two beams, A and B, are both feasible and can be delivered. Figure c) shows another target position for which beam B would be partially blocked and therefore infeasible. Note, that the range of motion of the target may vary and for some intervals during the overall treatment, beam B may also be feasible throughout the full breathing cycle.
  • Figure 2: Two interacting robots: One robot is used for treatment delivery and the other robot is used for ultrasound image guidance.
  • Figure 3: Excerpt from a 1D beam list.
  • Figure 6: Partial superior-inferior portion of the breathing curve of patient DB126-Fx1 in blue along time on the x axis. Model variable values of period as red line, base as green line through the middle of the blue line, with the sum formula values c0, c1, c2, c3 and s0, s1, s2, s3 dotted. Illustrated with an expectation query of the statistical model checker for the minimal and maximal curve point by the purple line atop the blue line and the green line along 0 on the y axis.
  • Figure 7: Architecture diagram of the software systems that we employ for our experiments. Each temporal slice consists of: (1) Client sends beam list, (2) Server uses Online Model Checking (OMC) to receive models predicting respiratory motion, (3) OMC uses Uppaal for model creation and verification, (4) Server starts Uppaal processes to verify beams, (5) Server sends list of beam results.
  • ...and 15 more figures