Sliced Online Model Checking for Optimizing the Beam Scheduling Problem in Robotic Radiation Therapy
Electronic Proceedings in Theoretical Computer Science(2024)
摘要
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
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要