Reachability analysis, in general, is a fundamental method that supports formally-correct synthesis, robust model predictive control, set-based observers, fault detection, invariant computation, and conformance checking, to name but a few. In many of these applications, one requires to compute a reachable set starting within a previously computed reachable set. While it was previously required to re-compute the entire reachable set, we demonstrate that one can leverage the dependencies of states within the previously computed set. As a result, we almost instantly obtain an over-approximative subset of a previously computed reachable set by evaluating analytical maps. The advantages of our novel method are demonstrated for falsification of systems, optimization over reachable sets, and synthesizing safe maneuver automata. In all of these applications, the computation time is reduced significantly.

Reachability analysis is one of the most important methods for formal verification of hybrid systems. The main difficulty for hybrid system reachability analysis is to calculate the intersection between reachable set and guard sets. While there exist several approaches for guard sets defined by hyperplanes or polytopes, only few methods are able to handle nonlinear guard sets. In this work we present a novel approach to tightly enclose the intersections of reachable sets with nonlinear guard sets. One major advantage of our method is its polynomial complexity with respect to the system dimension, which makes it applicable for high-dimensional systems. Furthermore, our approach can be combined with different reachability algorithms for continuous systems due to its modular design. We demonstrate the advantages of our novel approach compared to existing methods with numerical examples.

Hybrid automata are an emerging formalism used to model sampled-data control Cyber-Physical Systems (CPS), and analyze their behavior using reachability analysis. This is because hybrid automata provide a richer and more flexible modeling framework, compared to traditional approaches. However, modern state-of-the-art tools struggle to analyze such systems, due to the computational complexity of the reachability algorithm, and due to the introduced overapproximation error. These shortcomings are largely attributed (but not limited) to the aggregation of sets.

In this paper we propose a subspace identification approach for decomposed aggregation in the reachability analysis of hybrid automata with linear dynamics. Our key contribution is the observation that the choice of a good subspace basis does not only depend on the sets being aggregated, but also on the continuous-time dynamics of an automaton. With this observation in mind, we present a dynamics-aware sub-space identification algorithm that we use to construct tight decomposed convex hulls for the aggregated sets.

Our approach is evaluated on two practically relevant hybrid automata models of sampled-data CPS that have been shown to be difficult to analyze by modern state-of-the-art tools. Specifically, we show that for these models our approach can improve the accuracy of the reachable set by up-to 10 times when compared to standard Principal Component Analysis (PCA), for which finding a fixed point is not guaranteed. We also show that while the computational complexity is increased, a fixed-point is found earlier.

We introduce and study the concept of worst-case topological entropy of switched linear systems under arbitrary switching. It is shown that this quantity is equal to the minimal data rate (number of bits per second) required for the state observation of the switched linear system with any switching signal. A computable closed-form expression is presented for the worst-case topological entropy of switched linear systems. Finally, a practical coder-decoder, operating at a data rate arbitrarily close to the worst-case topological entropy, is described.

Our problem is to compute trajectories of a hybrid system that switches between stable affine ODEs, with switching triggered by hyperplane crossings. Instead of integrating over relatively short time steps, we propose to analytically calculate the affine ODE trajectories between switching times. Our algorithm computes the switching times themselves by Chebyshev interpolation of the analytic trajectory pieces, and polynomial root finding. We shrink the interpolation time intervals using bounds on the times needed by the affine ODE trajectories to enter certain Lyapunov sub-level sets. Based on the Chebfun package, we give a MATLAB implementation of our algorithm. We find that this implementation simulates Relay feedback systems as accurately and sometimes faster than conventional algorithms.

In this paper, we consider the problem of automatically designing a Rectified Linear Unit (ReLU) Neural Network (NN) architecture that is sufficient to implement the optimal Model Predictive Control (MPC) strategy for an LTI system with quadratic cost. Specifically, we propose AReN, an algorithm to generate Assured ReLU Architectures. AReN takes as input an LTI system with quadratic cost specification, and outputs a ReLU NN architecture with the assurance that there exist network weights that exactly implement the associated MPC controller. AReN thus offers new insight into the design of ReLU NN architectures for the control of LTI systems: instead of training a heuristically chosen NN architecture on data - or iterating over many architectures until a suitable one is found - AReN can suggest an adequate NN architecture before training begins. While several previous works were inspired by the fact that ReLU NN controllers and optimal MPC controllers are both Continuous, Piecewise-Linear (CPWL) functions, exploiting this similarity to design NN architectures with correctness guarantees has remained elusive. AReN achieves this using two novel features. First, we reinterpret a recent result about the implementation of CPWL functions via ReLU NNs to show that a CPWL function may be implemented by a ReLU architecture that is determined by the number of distinct affine regions in the function. Second, we show that we can efficiently over-approximate the number of affine regions in the optimal MPC controller without solving the MPC problem exactly. Together, these results connect the MPC problem to a ReLU NN implementation without explicitly solving the MPC: the result is a NN architecture that has the assurance that it can implement the MPC controller. We show through numerical results the effectiveness of AReN in designing an NN architecture.

Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions. However, a wide range of formulas are not monitorable under this approach, meaning that they have a prefix for which satisfaction and violation will always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category.

Recently, a robust semantics for LTL was introduced to capture different degrees by wich a property can be violated. In this paper we introduce a robust semantics for finite strings and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we discuss which properties that come naturally in LTL monitoring --- such as the realizability of all truth values --- can be transferred to the robust setting. Lastly, we show that LTL formulas with robust semantics can be monitored by deterministic automata and report on a prototype implementation.

In this paper, we introduce tools to verify the satisfaction of temporal logic specifications using the until operator for hybrid dynamical systems. Hybrid dynamical systems are given in terms of differential and difference inclusions, which capture the continuous and discrete dynamics (or events), respectively. For such systems, conditional invariance and eventual conditional invariance are employed to characterize dynamical properties associated with the until operators. Sufficient conditions for the satisfaction of temporal logic specifications involving the until operator are provided by guaranteeing properties of the data defining the systems and the existence of barrier functions or Lyapunov-like functions. Examples illustrate the results throughout the paper.

Cyber-physical system applications such as autonomous vehicles, wearable devices, and avionic systems generate a large volume of time-series data. Designers often look for tools to help classify and categorize the data. Traditional machine learning techniques for time-series data offer several solutions to solve these problems; however, the artifacts trained by these algorithms often lack interpretability. On the other hand, temporal logic, such as Signal Temporal Logic (STL) have been successfully used in the formal methods community as specifications of time-series behaviors. In this work, we propose a new technique to automatically learn temporal logic formulas that are able to classify real-valued time-series data. Previous work on learning STL formulas from data either assumes a formula-template to be given by the user, or assumes some special fragment of STL that enables exploring the formula structure in a systematic fashion. In our technique, we relax these assumptions, and provide a way to systematically explore the space of all STL formulas. As the space of all STL formulas is very large, and contains many semantically equivalent formulas, we suggest a technique to heuristically prune the space of formulas considered. Finally, we illustrate our technique on various case studies from the automotive and transportation domains.

Nondeterminism occurs naturally in Petri nets whenever multiple events are enabled at the same time. Traditionally, it is resolved at specification time using probability weights and priorities. In this paper, we focus on model checking for hybrid Petri nets with an arbitrary but finite number of stochastic firings (HPnGs) while preserving the inherent nondeterminism as a first-class modelling and analysis feature. We present two algorithms to compute optimal non-prophetic and prophetic schedulers. The former can be applied to all HPnG models while the latter is only applicable if information on the firing times of general transitions is specifically encoded in the model. Both algorithms make use of recent work on the parametric location tree, which symbolically unfolds the state space of an HPnG. A running example illustrates the approach and confirms the feasibility of the presented algorithm.

For exhaustive formal verification, industrial-scale cyber-physical systems (CPSs) are often too large and complex, and lightweight alternatives (e.g., monitoring and testing) have attracted the attention of both industrial practitioners and academic researchers. Falsification is one popular testing method of CPSs utilizing stochastic optimization. In state-of-the-art falsification methods, the result of the previous falsification trials is discarded, and we always try to falsify without any prior knowledge. To concisely memorize such prior information on the CPS model and exploit it, we employ Black-box checking (BBC), which is a combination of automata learning and model checking. Moreover, we enhance BBC using the robust semantics of STL formulas, which is the essential gadget in falsification. Our experiment results suggest that our robustness-guided BBC outperforms a state-of-the-art falsification tool.

The use of Neural Network (NN)-based controllers has attracted significant attention in recent years. Yet, due to the complexity and non-linearity of such NN-based cyber-physical systems (CPS), existing verification techniques that employ exhaustive state-space search, face significant scalability challenges; this effectively limits their use for analysis of real-world CPS. In this work, we focus on the use of Statistical Model Checking (SMC) for verifying complex NN-controlled CPS. Using an SMC approach based on Clopper-Pearson confidence levels, we verify from samples specifications that are captured by Signal Temporal Logic (STL) formulas. Specifically, we consider three CPS benchmarks with varying levels of plant and controller complexity, as well as the type of considered STL properties - reachability property for a mountain car, safety property for a bipedal robot, and control performance of the closed-loop magnet levitation system. On these benchmarks, we show that SMC methods can be successfully used to provide high-assurance for learning-based CPS.

Neural networks present a useful framework for learning complex dynamics, and are increasingly being considered as components to closed loop predictive control algorithms. However, if they are to be utilized in such safety-critical advisory settings, they must be provably "conformant" to the governing scientific (biological, chemical, physical) laws which underlie the modeled process. Unfortunately, this is not easily guaranteed as neural network models are prone to learn patterns which are artifacts of the conditions under which the training data is collected, which may not necessarily conform to underlying physiological laws.

In this work, we utilize a formal range-propagation based approach for checking whether neural network models for predicting future blood glucose levels of individuals with type-1 diabetes are monotonic in terms of their insulin inputs. These networks are increasingly part of closed loop predictive control algorithms for "artificial pancreas" devices which automate control of insulin delivery for individuals with type-1 diabetes. Our approach considers a key property that blood glucose levels must be monotonically decreasing with increasing insulin inputs to the model. Multiple representative neural network models for blood glucose prediction are trained and tested on real patient data, and conformance is tested through our verification approach. We observe that standard approaches to training networks result in models which violate the core relationship between insulin inputs and glucose levels, despite having high prediction accuracy. We propose an approach that can learn conformant models without much loss in accuracy.

We consider the policy synthesis problem for continuous-state controlled Markov processes evolving in discrete time, when the specification is given as a Büchi condition (visit a set of states infinitely often). We decompose computation of the maximal probability of satisfying the Büchi condition into two steps. The first step is to compute the maximal qualitative winning set, from where the Büchi condition can be enforced with probability one. The second step is to find the maximal probability of reaching the already computed qualitative winning set. In contrast with finite-state models, we show that such a computation only gives a lower bound on the maximal probability where the gap can be non-zero.

In this paper we focus on approximating the qualitative winning set, while pointing out that the existing approaches for unbounded reachability computation can solve the second step. We provide an abstraction-based technique to approximate the qualitative winning set by simultaneously using an over- and under-approximation of the probabilistic transition relation. Since we are interested in qualitative properties, the abstraction is non-probabilistic; instead, the probabilistic transitions are assumed to be under the control of a (fair) adversary. Thus, we reduce the original policy synthesis problem to a Büchi game under a fairness assumption and characterize upper and lower bounds on winning sets as nested fixed point expressions in the μ-calculus. This characterization immediately provides a symbolic algorithm scheme. Further, a winning strategy computed on the abstract game can be refined to a policy on the controlled Markov process.

We describe a concrete abstraction procedure and demonstrate our algorithm on two case studies. We show that our techniques are able to provide tight approximations to the qualitative winning set for the Van der Pol oscillator and a 3-d Dubins' vehicle.

We consider abstraction-based design of output-feedback controllers for dynamical systems with a finite set of inputs and outputs against specifications in linear-time temporal logic. The usual procedure for abstraction-based controller design (ABCD) first constructs a finite-state abstraction of the underlying dynamical system, and second, uses reactive synthesis techniques to compute an abstract state-feedback controller on the abstraction. In this context, our contribution is two-fold: (I) we define a suitable relation between the original system and its abstraction which characterizes the soundness and completeness conditions for an abstract state-feedback controller to be refined to a concrete output-feedback controller for the original system, and (II) we provide an algorithm to compute a sound finite-state abstraction fulfilling this relation.

Our relation generalizes feedback-refinement relations from ABCD with state-feedback. Our algorithm for constructing sound finite-state abstractions is inspired by the simultaneous reachability and bisimulation minimization algorithm of Lee and Yannakakis. We lift their idea to the computation of an observation-equivalent system and show how sound abstractions can be obtained by stopping this algorithm at any point. Additionally, our new algorithm produces a realization of the topological closure of the input/output behavior of the original system if it is finite-state realizable.

We develop an assume-guarantee framework for control of large scale linear (time-varying) systems from finite-time reach and avoid or infinite-time invariance specifications. The contracts describe the admissible set of states and controls for individual subsystems. A set of contracts compose correctly if mutual assumptions and guarantees match in a way that we formalize. We propose a rich parameterization of contracts such that the set of parameters that compose correctly is convex. Moreover, we design a potential function of parameters that describes the distance of contracts from a correct composition. Thus, the verification and synthesis for the aggregate system are broken to solving small convex programs for individual subsystems, where correctness is ultimately achieved in a compositional way. Illustrative examples demonstrate the scalability of our method.

Decision tree learning is a popular classification technique most commonly used in machine learning applications. Recent work has shown that decision trees can be used to represent provably-correct controllers concisely. Compared to representations using lookup tables or binary decision diagrams, decision trees are smaller and more explainable. We present dtControl, an easily extensible tool for representing memoryless controllers as decision trees. We give a comprehensive evaluation of various decision tree learning algorithms applied to 10 case studies arising out of correct-by-construction controller synthesis. These algorithms include two new techniques, one for using arbitrary linear binary classifiers in the decision tree learning, and one novel approach for determinizing controllers during the decision tree construction. In particular the latter turns out to be extremely efficient, yielding decision trees with a single-digit number of decision nodes on 5 of the case studies.

Hybrid Systems are systems having a mixed discrete and continuous behaviour that cannot be characterized faithfully using either only discrete or only continuous models. A good framework for hybrid systems should support their compositional description and analysis, since commonly systems are specified by a composition of smaller subsystems, to cope with the complexity of their monolithic representation. Moreover, since the reachability problem for hybrid systems is undecidable, one should investigate the conditions that guarantee approximate computability of composition, when only approximations to the exact problem data are available.

In this paper, we propose an automata-based formalism (HIOA) for hybrid systems that is compositional and for which the evolution can be computed approximately. The main results are that the composition of compatible HIOA yields a pre-HIOA; a dominance result on the composition of HIOA by which we can replace any component in a composition by another one that exhibits the same external behaviour without affecting the behaviour of the composition; finally, the key result that the composition of two compatible upper(lower)-semicontinuous HIOA is a computable upper(lower)-semicontinuous pre-HIOA, which entails that the evolution of the composition is upper(lower)-semicomputable. A discussion on how compositionality/computability are handled in state-of-art libraries for reachability analysis closes the paper.

Whereas classical control theory provides many methods for designing continuous-time feedback controllers, nowadays control algorithms are implemented on digital platforms and have to be designed in sampled time. Approaches to sampled-time control design are based on either discretization of the plant enabling discrete-time controller synthesis, or various redesign methods converting a continuous-time controller into a sampled-time approximation, providing comparable closed-loop system properties. The simplest of redesign approaches, typically used in practice, is the emulation of continuous-time feedback by sufficiently fast sampling. In spite of its simplicity, emulation gives rise to an important problem: does emulation at a sufficiently high rate (or, equivalently, with a small sampling time) preserve the stability of the closed-loop system? In this paper, we address this problem for the case of exponential stability (local or global). Even for linear systems, the problem of stability preservation becomes non-trivial when sampling is aperiodic. For nonlinear systems, viability of emulation approach is usually proved only under quite restrictive assumptions on the plant and the controller, which, as will be shown, in fact be discarded.

Modeling languages and tools based on Differential Algebraic Equations (DAE) bring several specific issues that do not exist with modeling languages based on Ordinary Differential Equations. The main problem is the determination of the differentiation index and latent equations. Prior to generating simulation code and calling solvers, the compilation of a model requires a structural analysis step, which reduces the differentiation index to a level acceptable by numerical solvers.

The Modelica language, among others, allows hybrid models with multiple modes, mode-dependent dynamics and state-dependent mode switching. These Multimode DAE (mDAE) systems are much harder to deal with. The main difficulties are (i) the combinatorial explosion of the number of modes, and (ii) the correct handling of mode switchings.

The focus of this paper is on the first issue, namely: How can one perform a structural analysis of an mDAE in all possible modes, without enumerating these modes? A structural analysis algorithm for mDAE systems is presented, based on an implicit representation of their varying structure. It generalizes J. Pryce's Σ-method to the multimode case and uses Binary Decision Diagrams (BDD) to represent the mode-dependent structure of an mDAE. The algorithm determines, as a function of the mode, the set of latent equations, the leading variables and the state vector. This is then used to compute a conditional block dependency graph of the system, that can be used to generate efficient simulation code with a mode-dependent scheduling of the blocks of equations.

Motivated by the safety problem, several definitions of reachability maps, for hybrid dynamical systems, are introduced. It is well established that, under certain conditions, the solutions to continuous-time systems depend continuously with respect to initial conditions. In such setting, the reachability maps considered in this paper are locally Lipschitz (in the Lipschitz sense for set-valued maps) when the right-hand side of the continuous-time system is locally Lipschitz. However, guaranteeing similar properties for reachability maps for hybrid systems is much more challenging. Examples of hybrid systems for which the reachability maps do not depend nicely with respect to their arguments, in the Lipschitz sense, are introduced. With such pathological cases properly identified, sufficient conditions involving the data defining a hybrid system assuring Lipschitzness of the reachability maps are formulated. As an application, the proposed conditions are shown to be useful to significantly improve an existing converse theorem for safety given in terms of barrier functions. Namely, for a class of safe hybrid systems, we show that safety is equivalent to the existence of a locally Lipschitz barrier function. Examples throughout the paper illustrate the results.

In this paper, we provide a compositional framework for synthesizing hybrid controllers for interconnected discrete-time control systems enforcing specifications expressed by co-Büchi automata. In particular, we first decompose the given specification to simpler reachability tasks based on automata representing the complements of original co-Büchi automata. Then, we provide a systematic approach to solve those simpler reachability tasks by computing cor-responding control barrier functions. We show that such control barrier functions can be constructed compositionally by assuming some small-gain type conditions and composing so-called local control barrier functions computed for subsystems. We provide two systematic techniques to search for local control barrier functions for subsystems based on the sum-of-squares optimization program and counter-example guided inductive synthesis approach. Finally, we illustrate the effectiveness of our results through two large-scale case studies.

In this paper we revisit the problem of computing controlled invariant sets for controllable discrete-time linear systems and present a novel hierarchy for their computation. The key insight is to lift the problem to a higher dimensional space where the maximal controlled invariant set can be computed exactly and in closed-form for the lifted system. By projecting this set into the original space we obtain a controlled invariant set that is a subset of the maximal controlled invariant set for the original system. Building upon this insight we describe in this paper a hierarchy of spaces where the original problem can be lifted into so as to obtain a sequence of increasing controlled invariant sets. The algorithm that results from the proposed hierarchy does not rely on iterative computations. We illustrate the performance of the proposed method on a variety of scenarios exemplifying its appeal.

We propose a method to control linear time-varying (LTV) discrete-time systems subject to bounded process disturbances and measurable outputs with bounded noise, and polyhedral constraints over system inputs and states. We search over control policies that map the history of measurable outputs to the current control input. We solve the problem in two stages. First, using the original system, we build a linear system that predicts future observations using the past observations. The bounded errors are characterized using zonotopes. Next, we propose control laws based on affine maps of such output prediction errors, and show that controllers can be synthesized using convex linear/quadratic programs. Furthermore, we can add constraints on trajectories and guarantee their satisfaction for all allowable sequences of observation noise and process disturbances. Our method does not require any assumptions about system controllability and observability. The controller design does not directly take into account the state-space dynamics, and its implementation does not require an observer. Instead, partial observability is often sufficient to design a correct controller. We provide the polytopic representation of observability errors and reachable sets in the form of zonotopes. Illustrative examples are included.

This paper presents an approach of safety verification based on neural networks for continuous dynamical systems which are modeled as a system of ordinary differential equations. We adopt the deductive verification methods based on barrier certificates. These are functions over the states of the dynamical system with certain constraints the existence of which entails the safety of the system under consideration. We propose to represent the barrier function by neural networks and provide a comprehensive synthesis framework. In particular, we devise a new type of activation functions, i.e., Bent-ReLU, for the neural networks; we provide sampling based approaches to generate training sets and formulate the loss functions for neural network training which can capture the essence of barrier certificate; we also present practical methods to check a learnt candidate barrier certificate against the criteria of barrier certificates as a formal guarantee. We implement our approaches via proof-of-concept experiments with encouraging results.

We consider the pressing question of how to model, verify, and ensure that autonomous systems meet certain obligations (like the obligation to respect traffic laws), and refrain from impermissible behavior (like recklessly changing lanes). Temporal logics are heavily used in autonomous system design; however, as we illustrate here, temporal (alethic) logics alone are inappropriate for reasoning about obligations of autonomous systems. This paper proposes the use of Dominance Act Utilitarianism (DAU), a deontic logic of agency, to encode and reason about obligations of autonomous systems. We use DAU to analyze Intel's Responsibility-Sensitive Safety (RSS) proposal as a real-world case study. We demonstrate that DAU can express well-posed RSS rules, formally derive undesirable consequences of these rules, illustrate how DAU could help design systems that have specific obligations, and how to model-check DAU obligations.

Many vehicle accidents result from collision with foreign objects. Automatic and provably safe collision avoidance systems are thus of prime importance to the automobile industry. Previous work on formally verifying car collision avoidance maneuvers typically only focuses on braking-only or swerving-only maneuvers. In this work, we study combined braking and swerving maneuvers and establish formally verified conditions under which safety from collision is ensured. One major constrain in performing such joint maneuvers is that a vehicle's tires have limited traction which can be used either for braking or swerving. So in essence, a combined maneuver can trade off braking ability for turning when it is advantageous to do so and vice-versa. In this work, we study the full continuous range of combined maneuvers, from maximal turning with little braking to maximal braking with little turning.

We use a unicycle model with Ackermann's steering for the car's motion, and the circle of traction forces to model the trade-off between braking and swerving. Resulting vehicle kinematics are formulated as a hybrid program in differential dynamic logic dL. We use the automated theorem prover KeYmaera X to formally verify the correctness of the collision avoidance property. This verification provides a mathematical guarantee that a given maneuver can prevent the car from collision with obstacles under certain conditions. The employed method is generic with a purely symbolic model and, thus, can be applied to verify other types of collision avoidance systems exhibiting richer behaviour.

This paper describes a verification case study on an autonomous racing car with a neural network (NN) controller. Although several verification approaches have been recently proposed, they have only been evaluated on low-dimensional systems or systems with constrained environments. To explore the limits of existing approaches, we present a challenging benchmark in which the NN takes raw LiDAR measurements as input and outputs steering for the car. We train a dozen NNs using reinforcement learning (RL) and show that the state of the art in verification can handle systems with around 40 LiDAR rays. Furthermore, we perform real experiments to investigate the benefits and limitations of verification with respect to the sim2real gap, i.e., the difference between a system's modeled and real performance. We identify cases, similar to the modeled environment, in which verification is strongly correlated with safe behavior. Finally, we illustrate LiDAR fault patterns that can be used to develop robust and safe RL algorithms.

Ant Colony algorithms are a set of biologically inspired algorithms used commonly to solve distributed optimization problems. Convergence has been proven in the context of optimization processes, but these proofs are not applicable in the framework of robotic control. In order to use Ant Colony algorithms to control robotic swarms, we present in this work more general results that prove asymptotic convergence of a multi-agent Ant Colony swarm moving in a weighted graph.

Decision tree learning is a popular classification technique most commonly used in machine learning applications. Recent work has shown that decision trees can be used to represent provably-correct controllers concisely. Compared to representations using lookup tables or binary decision diagrams, decision tree representations are smaller and more explainable. We present dtControl, an easily extensible tool offering a wide variety of algorithms for representing memoryless controllers as decision trees. We highlight that the trees produced by dtControl are often very concise with a single-digit number of decision nodes. This demo is based on our tool paper [1].

Large-scale stochastic systems have recently received significant attentions due to their broad applications in various safety-critical systems such as traffic networks and self-driving cars. In this poster, we describe the software tool AMYTISS, implemented in C++/OpenCL, for designing correct-by-construction controllers for large-scale discrete-time stochastic systems. This tool is employed to (i) build finite Markov decision processes (MDPs) as finite abstractions of given original systems, and (ii) synthesize controllers for the constructed finite MDPs satisfying bounded-time safety, reachability, and reach-avoid specifications. In AMYTISS, scalable parallel algorithms are designed such that they support the parallel execution within CPUs, GPUs and hardware accelerators (HWAs). Unlike all existing tools for stochastic systems, AMYTISS can utilize high-performance computing (HPC) platforms and cloud-computing services to mitigate the effects of the state-explosion problem, which is always present in analyzing large-scale stochastic systems. We benchmark AMYTISS against the most recent tools in the literature using several physical case studies including robot examples, room temperature and road traffic networks. We also apply our algorithms to a 3-dimensional autonomous vehicle and a 7-dimensional nonlinear model of a BMW 320i car by synthesizing autonomous parking controllers.

Related works. There exist a limited number of software tools on the verification and synthesis of stochastic systems with different classes of models. SReachTools [1] performs the stochastic reachability analysis for linear, potentially time-varying, discrete-time stochastic systems. FAUST² [2] generates formal abstractions for continuous-space discrete-time stochastic processes, and performs the verification and synthesis for safety and reachability specifications. However, FAUST² is originally implemented in MATLAB and handles finite-horizon specifications. StocHy [3] deals with a class of discrete-time stochastic hybrid systems, constructs finite abstractions, and performs the verification and synthesis for both finite- and infinite-horizon safety and reachability specifications. AMYTISS differs from FAUST² and StocHy in two main directions. First, AMYTISS implements novel parallel algorithms and data structures targeting HPC platforms to reduce the undesirable effects of the state-explosion problem. Accordingly, it is able to perform the parallel execution in different heterogeneous computing platforms including CPUs, GPUs and hardware accelerators (HWAs). Whereas, FAUST² and StocHy can only run serially in one CPU, and consequently, they are limited to small systems. Additionally, AMYTISS can handle the abstraction construction and controller synthesis for two and a halfplayer games (e.g., stochastic systems with bounded disturbances), whereas FAUST² and StocHy only handle one and a halfplayer games (disturbance-free systems).

Unlike all existing tools, AMYTISS offers highly scalable, distributed execution of parallel algorithms utilizing all available processing elements (PEs) in any heterogeneous computing platform. To the best of our knowledge, AMYTISS is the only tool of its kind for continuous-space stochastic systems that is able to utilize simultaneously all types of compute units (CUs).

A comparison between AMYTISS, FAUST² and StocHy based on their native features is provide in Table 1.

Main Contribution. AMYTISS is an open-source and self-contained tool and requires only a modern C++ compiler. It supports three major operating systems: Windows, Linux and Mac OS. The source of AMYTISS and detailed instructions on its building and running can be found in:

https://github.com/mkhaled87/pFaces-AMYTISS

The main merits of this work are:

(1) We propose a novel data-parallel algorithm for constructing finite MDPs from discrete-time stochastic systems and storing them in efficient distributed data containers.

(2) We propose parallel algorithms for synthesizing discrete controllers using the constructed MDPs to satisfy safety, reachability, or reach-avoid specifications. More specifically, we introduce novel parallel algorithms for the iterative computation of Bellman equation in the standard dynamic programming [4].

(3) Unlike the existing tools in the literature, AMYTISS accepts bounded disturbances and natively supports both additive and multiplicative noises with different distributions including normal, uniform, exponential, and beta.

This paper introduces inter-triggering hybrid automata, a formalism to represent multi-agent systems where each agent is represented as a hybrid automaton and agents interact by triggering discrete transitions (jumps and resets) on their "neighboring" agents. Using this formalism, we define responsibility-sensitive safety as respecting one another's invariances while triggering jumps and resets. This allows us to make a formal connection between responsibility and robust controlled invariant sets for individual agents, therefore leading to a compositional verification framework for the safety of the overall multi-agent system. We discuss several advantages of this viewpoint and illustrate it on a highway driving example.

We consider the computation of resilient controllers for perturbed non-linear dynamical systems w.r.t. linear-time temporal logic specifications. We address this problem through the paradigm of Abstraction-Based Controller Design (ABCD) where a finite state abstraction of the perturbed system dynamics is constructed and utilized for controller synthesis. In this context, our contribution is twofold: (I) We construct abstractions which model the impact of occasional high disturbance spikes on the system via the so called disturbance edges. (II) We show that the application of resilient reactive synthesis techniques to these abstract models results in controllers which render the resulting closed loop system maximally resilient to these occasional high disturbance spikes. We have implemented this resilient ABCD workflow on top of SCOTS and showcase our method through multiple robot planning examples.