-
Sliced Online Model Checking for Optimizing the Beam Scheduling Problem in Robotic Radiation Therapy
Authors:
Lars Beckers,
Stefan Gerlach,
Ole Lübke,
Alexander Schlaefer,
Sibylle Schupp
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…
▽ More
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.
△ Less
Submitted 27 March, 2024;
originally announced March 2024.
-
Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories
Authors:
Till Hofmann,
Stefan Schupp,
Gerhard Lakemeyer
Abstract:
Representing time is crucial for cyber-physical systems and has been studied extensively in the Situation Calculus. The most commonly used approach represents time by adding a real-valued fluent $\mathit{time}(a)$ that attaches a time point to each action and consequently to each situation. We show that in this approach, checking whether there is a reachable situation that satisfies a given formul…
▽ More
Representing time is crucial for cyber-physical systems and has been studied extensively in the Situation Calculus. The most commonly used approach represents time by adding a real-valued fluent $\mathit{time}(a)$ that attaches a time point to each action and consequently to each situation. We show that in this approach, checking whether there is a reachable situation that satisfies a given formula is undecidable, even if the domain of discourse is restricted to a finite set of objects. We present an alternative approach based on well-established results from timed automata theory by introducing clocks as real-valued fluents with restricted successor state axioms and comparison operators. %that only allow comparisons against fixed rationals. With this restriction, we can show that the reachability problem for finite-domain basic action theories is decidable. Finally, we apply our results on Golog program realization by presenting a decidable procedure for determining an action sequence that is a successful execution of a given program.
△ Less
Submitted 5 February, 2024;
originally announced February 2024.
-
Computer Aided Design and Grading for an Electronic Functional Programming Exam
Authors:
Ole Lübke,
Konrad Fuger,
Fin Hendrik Bahnsen,
Katrin Billerbeck,
Sibylle Schupp
Abstract:
Electronic exams (e-exams) have the potential to substantially reduce the effort required for conducting an exam through automation. Yet, care must be taken to sacrifice neither task complexity nor constructive alignment nor grading fairness in favor of automation. To advance automation in the design and fair grading of (functional programming) e-exams, we introduce the following: A novel algorith…
▽ More
Electronic exams (e-exams) have the potential to substantially reduce the effort required for conducting an exam through automation. Yet, care must be taken to sacrifice neither task complexity nor constructive alignment nor grading fairness in favor of automation. To advance automation in the design and fair grading of (functional programming) e-exams, we introduce the following: A novel algorithm to check Proof Puzzles based on finding correct sequences of proof lines that improves fairness compared to an existing, edit distance based algorithm; an open-source static analysis tool to check source code for task relevant features by traversing the abstract syntax tree; a higher-level language and open-source tool to specify regular expressions that makes creating complex regular expressions less error-prone. Our findings are embedded in a complete experience report on transforming a paper exam to an e-exam. We evaluated the resulting e-exam by analyzing the degree of automation in the grading process, asking students for their opinion, and critically reviewing our own experiences. Almost all tasks can be graded automatically at least in part (correct solutions can almost always be detected as such), the students agree that an e-exam is a fitting examination format for the course but are split on how well they can express their thoughts compared to a paper exam, and examiners enjoy a more time-efficient grading process while the point distribution in the exam results was almost exactly the same compared to a paper exam.
△ Less
Submitted 14 August, 2023;
originally announced August 2023.
-
Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks
Authors:
Joanna Delicaris,
Stefan Schupp,
Erika Ábrahám,
Anne Remke
Abstract:
This paper proposes an algorithm to maximize reachability probabilities for rectangular automata with random clocks via a history-dependent prophetic scheduler. This model class incorporates time-induced nondeterminism on discrete behavior and nondeterminism in the dynamic behavior. After computing reachable state sets via a forward flowpipe construction, we use backward refinement to compute maxi…
▽ More
This paper proposes an algorithm to maximize reachability probabilities for rectangular automata with random clocks via a history-dependent prophetic scheduler. This model class incorporates time-induced nondeterminism on discrete behavior and nondeterminism in the dynamic behavior. After computing reachable state sets via a forward flowpipe construction, we use backward refinement to compute maximum reachability probabilities. The feasibility of the presented approach is illustrated on a scalable model.
△ Less
Submitted 4 May, 2023; v1 submitted 28 April, 2023;
originally announced April 2023.
-
Robot Swarms as Hybrid Systems: Modelling and Verification
Authors:
Stefan Schupp,
Francesco Leofante,
Leander Behr,
Erika Ábrahám,
Armando Taccella
Abstract:
A swarm robotic system consists of a team of robots performing cooperative tasks without any centralized coordination. In principle, swarms enable flexible and scalable solutions; however, designing individual control algorithms that can guarantee a required global behavior is difficult. Formal methods have been suggested by several researchers as a mean to increase confidence in the behavior of t…
▽ More
A swarm robotic system consists of a team of robots performing cooperative tasks without any centralized coordination. In principle, swarms enable flexible and scalable solutions; however, designing individual control algorithms that can guarantee a required global behavior is difficult. Formal methods have been suggested by several researchers as a mean to increase confidence in the behavior of the swarm. In this work, we propose to model swarms as hybrid systems and use reachability analysis to verify their properties. We discuss challenges and report on the experience gained from applying hybrid formalisms to the verification of a swarm robotic system.
△ Less
Submitted 14 July, 2022;
originally announced July 2022.
-
Controlling Golog Programs against MTL Constraints
Authors:
Till Hofmann,
Stefan Schupp
Abstract:
While Golog is an expressive programming language to control the high-level behavior of a robot, it is often tedious to use on a real robotic system. On an actual robot, the user needs to consider low-level details, such as enabling and disabling hardware components, e.g., a camera to detect objects for gras**. In other words, high-level actions usually pose implicit temporal constraints on the…
▽ More
While Golog is an expressive programming language to control the high-level behavior of a robot, it is often tedious to use on a real robotic system. On an actual robot, the user needs to consider low-level details, such as enabling and disabling hardware components, e.g., a camera to detect objects for gras**. In other words, high-level actions usually pose implicit temporal constraints on the low-level platform, which are typically independent of the concrete program to be executed. In this paper, we propose to make these constraints explicit by modeling them as MTL formulas, which enforce the execution of certain low-level platform operations in addition to the main program. Based on results from timed automata controller synthesis, we describe a method to synthesize a controller that executes both the high-level program and the low-level platform operations concurrently in order to satisfy the MTL specification. This allows the user to focus on the high-level behavior without the need to consider low-level operations. We present an extension to Golog by clocks together with the required theoretical foundations as well as decidability results.
△ Less
Submitted 7 April, 2022;
originally announced April 2022.
-
Modeling R$^3$ Needle Steering in Uppaal
Authors:
Sascha Lehmann,
Antje Rogalla,
Maximilian Neidhardt,
Anton Reinecke,
Alexander Schlaefer,
Sibylle Schupp
Abstract:
Medical cyber-physical systems are safety-critical, and as such, require ongoing verification of their correct behavior, as system failure during run time may cause severe (or even fatal) personal damage. However, creating a verifiable model often conflicts with other application requirements, most notably regarding data precision and model accuracy, as efficient model checking promotes discrete d…
▽ More
Medical cyber-physical systems are safety-critical, and as such, require ongoing verification of their correct behavior, as system failure during run time may cause severe (or even fatal) personal damage. However, creating a verifiable model often conflicts with other application requirements, most notably regarding data precision and model accuracy, as efficient model checking promotes discrete data (over continuous) and abstract models to reduce the state space. In this paper, we approach the task of medical needle steering in soft tissue around potential obstacles. We design a verifiable model of needle motion (implemented in Uppaal Stratego) and a framework embedding the model for online needle steering. We mitigate the conflict by imposing boundedness on both the data types, reducing from R^3 to Z^3 when needed, and the motion and environment models, reducing the set of allowed local actions and global paths. In experiments, we successfully apply the static model alone, as well as the dynamic framework in scenarios with varying environment complexity and both a virtual and real needle setting, where up to 100% of targets were reached depending on the scenario and needle.
△ Less
Submitted 18 March, 2022;
originally announced March 2022.
-
Online Strategy Synthesis for Safe and Optimized Control of Steerable Needles
Authors:
Sascha Lehmann,
Antje Rogalla,
Maximilian Neidhardt,
Alexander Schlaefer,
Sibylle Schupp
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 cla…
▽ More
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.
△ Less
Submitted 24 October, 2021;
originally announced October 2021.
-
Synthesizing Strategies for Needle Steering in Gelatin Phantoms
Authors:
Antje Rogalla,
Sascha Lehmann,
Maximilian Neidhardt,
Johanna Sprenger,
Marcel Bengs,
Alexander Schlaefer,
Sibylle Schupp
Abstract:
In medicine, needles are frequently used to deliver treatments to subsurface targets or to take tissue samples from the inside of an organ. Current clinical practice is to insert needles under image guidance or haptic feedback, although that may involve reinsertions and adjustments since the needle and its interaction with the tissue during insertion cannot be completely controlled. (Automated) ne…
▽ More
In medicine, needles are frequently used to deliver treatments to subsurface targets or to take tissue samples from the inside of an organ. Current clinical practice is to insert needles under image guidance or haptic feedback, although that may involve reinsertions and adjustments since the needle and its interaction with the tissue during insertion cannot be completely controlled. (Automated) needle steering could in theory improve the accuracy with which a target is reached and thus reduce surgical traumata especially for minimally invasive procedures, e.g., brachytherapy or biopsy. Yet, flexible needles and needle-tissue interaction are both complex and expensive to model and can often be computed approximatively only. In this paper we propose to employ timed games to navigate flexible needles with a bevel tip to reach a fixed target in tissue. We use a simple non-holonomic model of needle-tissue interaction, which abstracts in particular from the various physical forces involved and appears to be simplistic compared to related models from medical robotics. Based on the model, we synthesize strategies from which we can derive sufficiently precise motion plans to steer the needle in soft tissue. However, applying those strategies in practice, one is faced with the problem of an unpredictable behavior of the needle at the initial insertion point. Our proposal is to implement a preprocessing step to initialize the model based on data from the real system, once the needle is inserted. Taking into account the actual needle tip angle and position, we generate strategies to reach the desired target. We have implemented the model in Uppaal Stratego and evaluated it on steering a flexible needle in gelatin phantoms; gelatin phantoms are commonly used in medical technology to simulate the behavior of soft tissue. The experiments show that strategies can be synthesized for both generated and measured needle motions with a maximum deviation of 1.84mm.
△ Less
Submitted 28 April, 2020;
originally announced April 2020.
-
Tool Support of Formal Methods for Privacy by Design
Authors:
Sibylle Schupp
Abstract:
Formal methods are, in principle, suited for supporting the recent paradigm of privacy by design, but no overview is available that summarizes which particular approaches have been investigated, for which application domains they are suited, and whether they are implemented and available as tools. Using the techniques of search-based literature review and snowballing this paper answers those quest…
▽ More
Formal methods are, in principle, suited for supporting the recent paradigm of privacy by design, but no overview is available that summarizes which particular approaches have been investigated, for which application domains they are suited, and whether they are implemented and available as tools. Using the techniques of search-based literature review and snowballing this paper answers those questions for a selected set of research papers.
△ Less
Submitted 26 March, 2019;
originally announced March 2019.
-
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Authors:
Robin Adams,
Sibylle Schupp
Abstract:
Privacy by design (PbD) is the principle that privacy should be considered at every stage of the software engineering process. It is increasingly both viewed as best practice and required by law. It is therefore desirable to have formal methods that provide guarantees that certain privacy-relevant properties hold. We propose an approach that can be used to design a privacy-compliant architecture w…
▽ More
Privacy by design (PbD) is the principle that privacy should be considered at every stage of the software engineering process. It is increasingly both viewed as best practice and required by law. It is therefore desirable to have formal methods that provide guarantees that certain privacy-relevant properties hold. We propose an approach that can be used to design a privacy-compliant architecture without needing to know the source code or internal structure of any individual component. We model an architecture as a set of agents or components that pass messages to each other. We present in this paper algorithms that take as input an architecture and a set of privacy constraints, and output an extension of the original architecture that satisfies the privacy constraints.
△ Less
Submitted 30 January, 2019;
originally announced January 2019.
-
Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis
Authors:
Stefan Schupp,
Johanna Nellen,
Erika Ábrahám
Abstract:
In this paper we propose an improvement for flowpipe-construction-based reachability analysis techniques for hybrid systems. Such methods apply iterative successor computations to pave the reachable region of the state space by state sets in an over-approximative manner. As the computational costs steeply increase with the dimension, in this work we analyse the possibilities for improving scalabil…
▽ More
In this paper we propose an improvement for flowpipe-construction-based reachability analysis techniques for hybrid systems. Such methods apply iterative successor computations to pave the reachable region of the state space by state sets in an over-approximative manner. As the computational costs steeply increase with the dimension, in this work we analyse the possibilities for improving scalability by dividing the search space in sub-spaces and execute reachability computations in the sub-spaces instead of the global space. We formalise such an algorithm and provide experimental evaluations to compare the efficiency as well as the precision of our sub-space search to the original search in the global space.
△ Less
Submitted 16 July, 2017;
originally announced July 2017.
