Online Strategy Synthesis for Safe and Optimized Control of Steerable Needles
Open Access
- 21 October 2021
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 348, 128-135
- https://doi.org/10.4204/eptcs.348.9
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.This publication has 24 references indexed in Scilit:
- Playing Optimally on Timed Automata with Random DelaysLecture Notes in Computer Science, 2012
- Synthia: Verification and Synthesis for Timed AutomataLecture Notes in Computer Science, 2011
- Reachability in Stochastic Timed GamesLecture Notes in Computer Science, 2009
- Timed Control with Observation Based and Stuttering Invariant StrategiesLecture Notes in Computer Science, 2007
- Nonholonomic Modeling of Needle SteeringThe International Journal of Robotics Research, 2006
- Efficient On-the-Fly Algorithms for the Analysis of Timed GamesLecture Notes in Computer Science, 2005
- Optimal Strategies in Priced Timed Game AutomataLecture Notes in Computer Science, 2004
- The tool KronosLecture Notes in Computer Science, 1996
- On the synthesis of discrete controllers for timed systemsLecture Notes in Computer Science, 1995
- A theory of timed automataTheoretical Computer Science, 1994