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.

翻译：在机器人放射治疗中，来自不同方向的高能光子射束被导向患者体内的靶区。靶区运动可通过机器人超声进行追踪，并通过同步射束运动进行补偿。然而，移动射束可能导致射束穿过超声换能器或其搭载机器人。虽然可通过暂停射束输送避免此问题，但治疗时间会因此增加。通常，射束按最小化机器人运动进而缩短总治疗时间的顺序输送。但此顺序可被更改，即无需暂停射束，转而输送其他可行射束。我们通过应用模型检测范式选择可行射束来解决射束动态排序问题。由于呼吸模式复杂且快速变化，任何离线模型都过于不精确。因此，模型检测需在线进行，即预测患者短期内的当前呼吸模式，并检查哪些射束可安全输送。在线监测治疗过程提供了动态重排射束的能力，从而避免暂停并缩短治疗时间。鉴于人类呼吸模式复杂且可能快速变化，我们需要一种可快速验证的模型，并通过正弦曲线叠加进行近似。此外，我们将三维呼吸运动简化为独立的一维模型。通过向模型内部添加噪声来补偿简化带来的误差。进而同步代表不同空间方向的多个模型、治疗仿真及对应的验证查询。初步结果显示，与静态射束调度相比，根据附加安全余量的不同，本方法在空闲时间上的平均改善幅度达16.02%至37.21%。需注意，超声机器人周围附加安全余量虽可减少空闲时间，但会限制可用射束方向范围从而降低计划质量。相比之下，采用在线模型检测的方法能保持计划质量。此外，我们与一种难以推理且未能实现目标的朴素机器学习方法进行了比较。