Online Strategy Synthesis for Safe and Optimized Control of Steerable Needles

TL;DR

This paper presents an online strategy synthesis method that ensures safe, adaptive control of steerable needles in medical procedures by combining formal safety guarantees with environment-aware reactive planning.

Contribution

It introduces a novel online approach that combines classical strategy synthesis with real-time model updates for safe needle steering in uncertain environments.

Findings

Successfully applied to medical needle steering

Provides safety guarantees during dynamic environment changes

Enables reactive and prospective planning for complex systems

Abstract

Autonomous systems are often applied in uncertain environments, which require prospective action planning and retrospective data evaluation for future planning to ensure safe operation. Formal approaches may support these systems with safety guarantees, but are usually expensive and do not scale well with growing system complexity. In this paper, we introduce online strategy synthesis based on classical strategy synthesis to derive formal safety guarantees while reacting and adapting to environment changes. To guarantee safety online, we split the environment into region types which determine the acceptance of action plans and trigger local correcting actions. Using model checking on a frequently updated model, we can then derive locally safe action plans (prospectively), and match the current model against new observations via reachability checks (retrospectively). As use case, we successfully apply online strategy synthesis to medical needle steering, i.e., navigating a (flexible and beveled) needle through tissue towards a target without damaging its surroundings.