We present a method for the automatic derivation of runtime monitoring specifications for unmanned aerial vehicles (UAVs) based on symbolic control behavior. Starting from a symbolic control policy, which is synthesized from formal mission specifications, we simulate the controller together with a reduced-order plant model to generate reference trajectories. These are transformed into geometry based monitors composed of tolerance tubes and consistency metrics that compare observed and reference behavior. The specifications are computed online, allowing situation dependent adaptation. Monitors operate externally, require no access to internal controller states, and enable real time detection of deviations. The approach is evaluated on physical experiments with micro UAVs.

The contributions of this short technical note are two-fold. Firstly, we introduce a modified version of a generalized Bellman-Ford algorithm calculating the value function of optimal control problems defined on hyper-graphs. Those Bellman-Ford algorithms can be used in particular for the synthesis of near-optimal controllers by the principle of symbolic control. Our modification causes less nodes of the hyper-graph being iterated during the execution compared to our initial version of the algorithm published in 2020. Our second contribution lies in the field of Plan recognition applied to drone missions driven by symbolic controllers. We address and resolve the Plan and Goal Recognition monitor's dependence on a pre-defined initial guess for a drone's task allocation and mission execution. To validate the enhanced implementation, we use a more challenging scenario for UAV-based aerial firefighting, demonstrating the practical applicability and robustness of the system architecture.

The computation of symbolic controllers for non-linear plants is typically computationally expensive due to the well-known curse-of-dimensionality. In fact, those controllers must be computed before operating the closed loop. This note presents a method to modify symbolic controllers while they are operating the closed loop to avoid spontaneously inserted state obstacles. In addition, we utilize methods of plan recognition in combination with our new algorithm for providing a technique of decentralized runtime assurance for efficient task allocation and mission guidance in a multi-UAV setting. Promising results and the applicability of the found method is demonstrated by simulation and experiments with real physical systems.

We present a forest fire firefighting simulation tool named FORFIS that is implemented in Python. Unlike other existing software, we focus on a user-friendly software interface with an easy-to-modify software engine. Our tool is published under GNU GPLv3 license and comes with a GUI as well as additional output functionality. The used wildfire model is based on the well-established approach by cellular automata in two variants - a rectangular and a hexagonal cell decomposition of the wildfire area. The model takes wind into account. In addition, our tool allows the user to easily include a customized firefighting strategy for the firefighting agents.

Being a fully algorithmic procedure, symbolic controller synthesis offers weighty advantages over other established synthesis procedures. In fact, the returned controllers provably enforce the given specification in the control loop making verification steps obsolete. However, the curse-of-dimensionality prevents this scheme from being applied to industrial problems. Applications to real experiments are indeed rare. In this note, we demonstrate how to utilize symbolic optimal control in order to control miniature quadcopters at the level of mission guidance. Specifically, a firefighting scenario using a Crazyflie 2.1 drone is considered, which involves reach-avoid and reach-and-stay control tasks. Furthermore, we present a runtime monitor, automatically derived from the synthesized symbolic controller. Based on the methodologies of plan recognition, this monitor observes the drone’s flightpath and infers the current controller mode. Thus, it is able to predict the upcoming manoeuvres of the drone.

Symbolic optimal control is a powerful method to synthesize algorithmically correct-by-design state-feedback controllers for nonlinear plants. Its solutions are (near-)optimal with respect to a given cost function. In this note, it is demonstrated how symbolic optimal control can be used to calculate controllers for an optimized routing guidance of vehicle systems in continuous state space. In fact, the capacitated vehicle routing problem and a variant of travelling salesman problem are investigated. The latter problem has a relevant application in case of loss of vehicles during mission. A goods delivery scenario and a reconnaissance mission, involving bicycle and aircraft dynamics respectively, are provided as examples.

We present ABS, a software for Abstraction-Based Synthesis of controllers for continuous-state control systems. The tool distinguishes itself from previously known such software by being formally correct, i.e., any controller synthesized by ABS is mathematically guaranteed to solve the control problem provided as input. ABS achieves this quality by providing an input language with mathematically defined semantics and a respective compiler, and by carefully taking into account all numerical and rounding errors that might be incurred at either compile- or run-time. To mitigate computational overhead caused by the aforementioned approach, ABS implements, e.g. on-the-fly synthesis algorithms with greatly reduced memory requirement. The tool is currently applicable to invariance and reachability problems and requires state measurement. We discuss structure, algorithmic details and basic usage of ABS, and we demonstrate on two examples that its performance compares favorably with that of competing, not formally correct synthesis software. The source code of ABS is publicly available. See http://www.reiszig.de/gunther/pubs/ABS.html

This paper proposes an algorithmic method to heuristically solve the famous Travelling Salesman Problem (TSP) when the salesman's path evolves in continuous state space and discrete time but with otherwise arbitrary (nonlinear) dynamics. The presented method is based on the framework of Symbolic Control. In this way, our method returns a provably correct state-feedback controller for the underlying coverage specification, which is the TSP leaving out the requirement for optimality on the route. In addition, we utilize the Lin-Kernighan-Helsgaun TSP solver to heuristically optimize the cost for the overall taken route. Two examples, an urban parcel delivery task and a UAV reconnaissance mission, greatly illustrate the powerfulness of the proposed heuristic.

The present work deals with quantitative two-phase reach-avoid problems on nonlinear control systems. This class of optimal control problem requires the plant's state to visit two (rather than one) target sets in succession while minimizing a prescribed cost functional. As we illustrate, the naive approach, which subdivides the problem into the two evident classical reach-avoid tasks, usually does not result in an optimal solution. In contrast, we prove that an optimal controller is obtained by consecutively solving two special quantitative reach-avoid problems. In addition, we present a fully-automated method based on Symbolic Optimal Control to practically synthesize for the considered problem class approximately optimal controllers for sampled-data nonlinear plants. Experimental results on parcel delivery and on an aircraft routing mission confirm the practicality of our method.

Symbolic controller synthesis is a fully-automated and correct-by-design synthesis scheme whose limitations are its immense memory and runtime requirements. A current trend to compensate for this downside is to develop techniques for parallel execution of the scheme both in mathematical foundation and in software implementation. In this paper we present a generalized Bellman-Ford algorithm to be used in the so-called symbolic optimal control, which is an extension of the aforementioned synthesis scheme. Compared to the widely used Dijkstra algorithm our algorithm has two advantages. It allows for cost functions taking arbitrary (e.g. negative) values and for parallel execution with the ability for trading processing speed for memory consumption. We motivate the usefulness of negative cost values on a scenario of aerial firefighting with unmanned aerial vehicles. In addition, this four-dimensional numerical example, which is rich in detail, demonstrates the great performance of our algorithm.

In this note, the application of a plant model-based fault detection method for nonlinear control systems on aircraft takeoff is introduced. This method utilizes non-deterministic finite-state automata, which approximate the fault-free dynamics of the plant. The aforementioned automaton is computed in a preliminary step while during evolution of the plant the automaton is continually evaluated to detect discrepancies between the actual and the nominal dynamics. In this way the fault detection module itself can be implemented on simpler hardware on board of the plant. Moreover, an implementation technique is presented that allows the use of the proposed fault detection method when the plant dynamics is given only by means of a graphical programming script. The great potential and practicality of the used method are demonstrated on a simulated takeoff manoeuvre of a battery-electrically driven aircraft.

We present an abstraction and refinement methodology for the automated controller synthesis to enforce general predefined specifications. The designed controllers require quantized (or symbolic) state information only and can be interfaced with the system via a static quantizer. Both features are particularly important with regard to any practical implementation of the designed controllers and, as we prove, are characterized by the existence of a feedback refinement relation between plant and abstraction. Feedback refinement relations are a novel concept introduced in this paper. Our work builds on a general notion of system with set-valued dynamics and possibly non-deterministic quantizers to permit the synthesis of controllers that robustly, and provably, enforce the specification in the presence of various types of uncertainties and disturbances. We identify a class of abstractions that is canonical in a well-defined sense, and provide a method to efficiently compute canonical abstractions. We demonstrate the practicality of our approach on two examples.

The practical impact of abstraction-based controller synthesis methods is currently limited by the immense computational effort for obtaining abstractions. In this note we focus on a recently proposed method to compute abstractions whose state space is a cover of the state space of the plant by congruent hyper-intervals. The problem of how to choose the size of the hyper-intervals so as to obtain computable and useful abstractions is unsolved. This note provides a twofold contribution towards a solution. Firstly, we present a functional to predict the computational effort for the abstraction to be computed. Secondly, we propose a method for choosing the aspect ratio of the hyper-intervals when their volume is fixed. More precisely, we propose to choose the aspect ratio so as to minimize a predicted number of transitions of the abstraction to be computed, in order to reduce the computational effort. To this end, we derive a functional to predict the number of transitions in dependence of the aspect ratio. The functional is to be minimized subject to suitable constraints. We characterize the unique solvability of the respective optimization problem and prove that it transforms, under appropriate assumptions, into an equivalent convex problem with strictly convex objective. The latter problem can then be globally solved using standard numerical methods. We demonstrate our approach on an example.

We consider an automated, algorithmic controller synthesis framework for perturbed nonlinear control systems to enforce complex specifications, in which an auxiliary transition system, also known as abstraction or symbolic model, is used as a finite substitute of the original control system in the controller design process. We specifically focus on reducing the computational effort to obtain abstractions, which is the most expensive step in the approach. To this end, we derive a functional to estimate the size of the abstraction, specifically, the number of transitions, and prove that after a suitable transformation the functional becomes strongly convex. Thus, the minimization of the estimated size of the abstraction is an unconstrained strongly convex optimization problem, which is straightforward to solve using standard methods. This permits us to use this functional as a heuristic to determine certain grid parameters for the construction of abstractions. We illustrate the benefits of the newly developed heuristic for two numerical examples.

Necessary and sufficient conditions for convexity and strong convexity, respectively, of connected sublevelsets that are defined by finitely many real-valued $C^{1,1}$-maps are presented. A novel characterization ofstrongly convex sets in terms of the so-called local quadratic support is proved. The results concerningstrong convexity are used to derive sufficient conditions for attainable sets ofcontinuous-time nonlinear systems to be strongly convex. An application of these conditions is a novel methodto overapproximate attainable sets when strong convexity is present.

We prove that strong structural controllability of a pair of structural matrices (A, B) can be verified in time linear in n + r + v, where A is square, n and r denote the number of columns of A and B, respectively, and v is the number of non-zero entries in (A, B). We also present an algorithm realizing this bound, which depends on a recent, high-level method to verify strong structural controllability and uses sparse matrix data structures. Linear time complexity is actually achieved by separately storing both the structural matrix (A, B) and its transpose, linking the two data structures through a third one, and a novel, efficient scheme to update all the data during the computations. We illustrate the performance of our algorithm using systems of various sizes and sparsity.

We present several novel results related to the concept of strong convexity, culminating in sufficient conditions for attainable sets of continuous-time nonlinear dynamical systems to be strongly convex. Based on these results, we propose a method to over-approximate attainable sets by intersections of supporting balls, which greatly improves upon the accuracy of previously proposed approximations based on supporting halfspaces. The latter advantage can be exploited, for example, when the method is used in algorithms that compute discrete abstractions of continuous plants. As we demonstrate by an example, the design of finite-state controllers can then be based on coarser state space quantizations, which directly translates into a reduced complexity of the controllers.

Strongly convex sets in Hilbert spaces are characterized by local properties. One quantity which is used for this purpose is a generalization of the modulus of convexity δΩ of a set Ω. We also show that limε→0δΩ(ε)/ε2 exists whenever Ω is closed and convex.