ABSTRACT. We consider decision problems associated with the linear quadratic regulator (LQR) and linear quadratic Gaussian (LQG) control problems in continuous time. The decision problems ask, given the parameters of a problem and a threshold rational number r, is the optimal cost less than or equal to the threshold r? LQR and LQG are fundamental problems in the theory of linear systems and it is well known that optimal controllers for these problems have a closed form solution. However, since the closed form solutions involve transcendental functions, they can only be evaluated numerically. Thus, it is possible that numerical imprecisions prevent answering the decision problem no matter what precision is used for the computations. Indeed, the computability of these natural decision problems has remained open. We show that the problems are, in fact, decidable. The decidability is not relative to any limit on the numerical precision. Our proof uses the Lindemann-Weierstrass theorem from transcendental number theory to show that checking whether an exponential polynomial is less than or equal to a rational threshold is decidable. We show further that (conditional) decidability results for several open problems in linear systems theory can be obtained if one additionally assumes Schanuel's conjecture, a unifying conjecture in transcendental number theory.

ABSTRACT. A pedestrian road network is a complex non-linear dynamic system, and it is prone to severe accidents due to the congestion of spatio-temporal mass gathering. This paper proposes a hybrid framework of crowd dynamics modeling and model predictive control to ease the pressure of pedestrian road networks. The framework is integrated on the basis of a mature paradigm in the field of traffic signal control; the theory is yet new to pedestrian road networks except general traffic signals on the streets. The novelty also lies in its ability to simultaneously monitor both the discrete and continuous dynamics changes in the overall network. We verify the framework through comparison with simulation of manual control commands restored from real cases of a large-scale outdoor event. The results indicate that the proposed framework has a superior performance in keeping the balance in the overall distribution of large-scale crowd and reducing the risk of saturation in a pedestrian road network.

ABSTRACT. Planning in hybrid systems with both discrete and continuous control variables is important for dealing with real-world applications such as extra-planetary exploration and multi-vehicle transportation systems. Meanwhile, generating high-quality solutions given certain hybrid planning specifications is crucial to building high-performance hybrid systems. However, given hybrid planning is challenging in general, most methods use greedy search that is guided by various heuristics, which is neither complete or optimal and often falls into blind search towards an infinite-action plan. In this paper, we present a hybrid automaton planning formalism and propose an optimal approach that encodes this planning problem as a Mixed Integer Linear Program (MILP) by fixing the action number of automaton runs. By leveraging an efficient MILP optimizer, our method is able to generate provably optimal solutions for complex mixed discrete-continuous planning problems within a reasonable time. We demonstrate this by benchmarking our encoding against Scotty in the Mars exploration domains, air refueling domains, and the truck-and-drone delivery domains.

ABSTRACT. Complementarity problems, a class of mathematical optimization problems with orthogonality constraints, are widely used in many robotics tasks, such as locomotion and manipulation, due to their ability to model non-smooth phenomena such as contact dynamics. In this paper, we propose a method to analyze the stability of both linear and complementarity systems with neural network controllers. First, we introduce a method to represent neural networks with rectified linear unit (ReLU) activations as linear complementarity problems. Then, we show that systems with neural network controllers have an equivalent linear complementarity system (LCS) description. Using the LCS representation, we perform stability analysis on the closed-loop system and turn the stability verification problem into a linear matrix inequality (LMI) feasibility problem. We demonstrate the approach on several examples, including multi-contact problems and friction models with non-unique solutions.

ABSTRACT. This paper accompanies FOSSIL: a software tool for the synthesis of Lyapunov functions and of barrier certificates (or functions) for dynamical systems modelled as differential equations. Lyapunov functions are key for stability analysis, whereas barrier functions assert the safety of dynamical models. The tool has two core contributions on synthesis -- automation and soundness -- both of which are attained by means of an inductive, counter-example-based method. This methods exploits the flexibility of candidate functions generated by training neural network templates, the formal assertions provided by a verifier (namely, an SMT solver), and finally new procedures to ease the communication/exchange of information between the two mentioned components. We endow the tool with features of usability, scalability, and robustness -- all of which are showcased on benchmarks.

ABSTRACT. We propose a sampling-based approach to learn Lyapunov functions for a class of discrete-time autonomous hybrid systems that admit a mixed-integer representation. Such systems include autonomous piecewise affine systems, closed-loop dynamics of linear systems with model predictive controllers, piecewise affine/linear complementarity/mixed-logical dynamical system in feedback with a ReLU neural network controller, etc. The proposed method comprises an alternation between a learner and a verifier to find a valid Lyapunov function inside a convex set of Lyapunov function candidates. In each iteration, the learner uses a collection of state samples to select a Lyapunov function candidate through a convex program in the parameter space. The verifier then solves a mixed-integer quadratic program in the state space to either validate the proposed Lyapunov function candidate or reject it with a counterexample, i.e., a state where the Lyapunov condition fails. This counterexample is then added to the sample set of the learner to refine the set of Lyapunov function candidates. By designing the learner and the verifier according to the analytic center cutting-plane method from convex optimization, we show that when the set of Lyapunov functions is full-dimensional in the parameter space, our method finds a Lyapunov function in a finite number of steps. We demonstrate our stability analysis method on closed-loop MPC dynamical systems and a ReLU neural network controlled PWA system.

ABSTRACT. This paper studies topological entropy of switched nonlinear systems. We construct a general upper bound for the topological entropy in terms of an average of the asymptotic suprema of the measures of Jacobian matrices of individual modes, weighted by the corresponding active rates. A general lower bound is also established in terms of an active-rate-weighted average of the asymptotic infima of the traces of these Jacobian matrices. For switched systems with diagonal modes, we establish upper and lower bounds that only depend on the eigenvalues of Jacobian matrices, their relative order among individual modes, and the active rates. For both cases, we also establish upper bounds that are more conservative but require less information on the switching, with their relations illustrated by numerical examples of a switched Lotka--Volterra ecosystem model.

ABSTRACT. We introduce a new system for object-oriented distributed hybrid systems to verify object invariants and method contracts. In a hybrid setting, the object invariant must not only be the post-condition of a method, but also has to hold in the post-region of a method, because the state of the object evolves according to continuous dynamics. The post-region describes all reachable states after method termination before another process runs. This set can be approximated using lightweight analysis of the class structure. The system naturally generalizes rely-guarantee reasoning of discrete object-oriented languages to hybrid systems and carries over its compositionality to hybrid systems: only one dL-proof obligation is generated per method. By reasoning about the minimal size of the post-region, local Zeno behavior can also be analyzed. Our approach is implemented for the Hybrid Active Object language HABS.

ABSTRACT. Signal temporal logic (STL) was introduced for monitoring temporal properties of continuous-time signals for continuous and hybrid systems. Differential dynamic logic (dL) was introduced to reason about the end states of a hybrid program. Over the past decade, STL and its variants have significantly gained in popularity in the industry for monitoring purposes, while dL has gained in popularity for verification of hybrid systems. In this paper, we bridge the gap between the two different logics by introducing signal temporal dynamic logic (STdL) -- a dynamic logic that reasons about a subset of STL specifications over executions of hybrid systems. Our work demonstrates that STL can be used for deductive verification of hybrid systems. STdL significantly augments the expressiveness of dL by allowing reasoning about temporal properties in given time intervals. We provide a semantics and a proof calculus for STdL, along with a proof of soundness and relative completeness.

ABSTRACT. In the context of developing safe air transportation, our work is focused on understanding how Reinforcement Learning methods can improve the state of the art in traditional control, in nominal as well as non-nominal cases (motor and sensor failures, weather conditions etc.). The end goal is to train provably safe controllers, by improving both the training and the verification methods. In this paper, we explore this path for controlling the attitude of a quadcopter: we discuss theoretical as well as practical aspects of training neural nets for controlling a crazyflie 2.0 drone. In particular we describe thoroughly the choices in training algorithms, neural net architecture, hyperparameters, observation space etc. We also discuss the robustness of the obtained controllers, both to partial loss of power for one rotor and to wind gusts. Finally, we measure the performance of the approach by using a robust form of a signal temporal logic to quantitatively evaluate the vehicle's behavior.

ABSTRACT. Deploying deep reinforcement learning in safety-critical settings requires developing algorithms that obey hard constraints during exploration. This paper contributes a first approach toward enforcing formal safety constraints on end-to-end policies with visual inputs. Our approach draws on recent advances in object detection and automated reasoning for hybrid dynamical systems. The approach is evaluated on a novel benchmark that emphasizes the challenge of safely exploring in the presence of hard constraints. Our benchmark draws from several proposed problem sets for safe learning and includes problems that emphasize challenges such as reward signals that are not aligned with safety constraints. On each of these benchmark problems, our algorithm completely avoids unsafe behavior while remaining competitive at optimizing for as much reward as is safe. We also present a new method of enforcing safety constraints by modifying the environment instead of the training algorithm. We prove that any policy is safe in this environment wrapper, allowing unconstrained policies to be learned, and that the wrapper preserves expected rewards from the original environment.

ABSTRACT. In this paper we study the problem of synthesizing optimal control policies for uncertain continuous-time nonlinear systems from syntactically co-safe linear temporal logic (scLTL) formulas. We formulate this problem as a sequence of reach-avoid optimal control sub-problems. We show that the resulting hybrid optimal control policy guarantees the satisfaction of a given scLTL formula by constructing a barrier certificate. Since solving each optimal control problem may be computationally intractable, we take a learning-based approach to approximately solve this sequence of optimal control problems online without requiring full knowledge of the system dynamics. Using Lyapunov-based tools, we develop sufficient conditions under which our approximate solution maintains correctness. Finally, we demonstrate the efficacy of the developed method with a numerical example.