ABSTRACT. We consider the problem of extracting safe environments and controllers for reach-avoid objectives for systems with known state and control spaces, but unknown dynamics. In a given environment, a common approach is to synthesize a controller from an abstraction or a model of the system (potentially learned from data). However, in many situations, the relationship between the dynamics of the model and the actual system is not known; and hence it is difficult to provide safety guarantees for the system. In such cases, the Standard Simulation Metric (SSM), defined as the worst-case norm distance between the model and the system output trajectories, can be used to modify a reach-avoid specification for the system into a more stringent specification for the abstraction. Nevertheless, the obtained distance, and hence the modified specification, can be quite conservative. This limits the set of environments for which a safe controller can be obtained. We propose SPEC, a specification-centric simulation metric, which overcomes these limitations by computing this distance using only the trajectories that violate the specification for the system. We show that modifying a reach-avoid specification with SPEC allows us to synthesize a safe controller for a larger set of environments compared to SSM. Case studies using simulators for quadrotors and autonomous cars illustrate the ad- vantages of the proposed metric for determining safe environment sets and controllers.

ABSTRACT. Weakly-hard systems are real-time systems that can tolerate occasional missed deadlines. Compared with traditional systems with hard deadline constraints, they provide more scheduling flexibility, and thus expands the design space for system configuration and reconfiguration. The central question for such a system is precisely to what degree it can tolerate deadline misses while still meeting its functional requirements. In this paper, we provide a formal treatment to the verification problem of a general class of weakly-hard systems. We discuss relaxation and over-approximation techniques for managing the complexity of reachability analysis, and develop upon these algorithms for verifying the safety of weakly-hard systems. Experiments demonstrate the effectiveness of our approach in understanding the impact of and selecting among different weakly hard constraints.

ABSTRACT. In the first part of this paper, we solve the problem of verifying the stability of an interconnection of embedded control systems under a timing contract which specifies the time instants at which some operations in each subsystem are performed such as sampling, actuation, or control input computation. In our approach, we reformulate each subsystem into an impulsive system and then derive a small gain condition on the stability of the interconnection using reachability analysis. In the second part of the paper, we consider the problem of synthesizing a set of timing contracts that guarantee the stability of the interconnected embedded control system by exploiting the monotonicity of stability with respect to timing contract parameters. Linear and nonlinear examples are provided allowing us to compare our results with existing techniques and to show the effectiveness of our approach.

ABSTRACT. Robust Linear Temporal Logic (rLTL) was crafted to incorporate the notion of robustness into Linear-time Temporal Logic (LTL) specifications. Technically, robustness was formalized in the logic rLTL via 5 different truth values and it led to an increase in the time complexity of the associated model checking problem. In general, model checking an rLTL formula relies on constructing a general- ized Büchi automaton of size 5^{|φ|} where |φ| denotes the length of an rLTL formula φ. It was recently shown that the size of this automa- ton can be reduced to 3^{|φ|} (and even smaller) when the formulas to be model checked come from a fragment of rLTL. In this paper, we introduce Evrostos, the first tool for model checking formulas in this fragment. We also present several empirical studies, based on models and LTL formulas reported in the literature, confirming that rLTL model checking for the aforementioned fragment incurs in a time overhead that makes the verification of rLTL practical.

ABSTRACT. This paper presents TIRA, a Matlab library gathering several methods for the computation of interval over-approximations of the reachable sets for both continuous- and discrete-time nonlinear systems. Unlike other existing tools, the main strength of interval-based reachability analysis is its simplicity and scalability, rather than the accuracy of the over-approximations. The current implementation of TIRA contains five reachability methods covering wide classes of nonlinear systems, handled with the classical monotonicity approach as well as more recent results relying on contraction/growth bounds and monotonicity concepts. TIRA's architecture features a central function working as a hub between the user-defined reachability problem and the library of available reachability methods. This design choice offers an increased extensibility of the library, where users can define their own method in a separate function and then simply add the function call in the hub function.

ABSTRACT. In this paper we study how to formulate the optimal control problem for a piecewise-affine dynamical system as a mixed-integer program. Problems of this form arise typically in hybrid Model Predictive Control (MPC), where at every time step an open-loop optimal control sequence is computed via numerical optimization and applied to the system in a moving horizon fashion. Not surprisingly, the efficiency in the formulation of the underlying mathematical program has a crucial influence on computation times, and hence on the applicability of hybrid MPC to high-dimensional systems. We leverage on modern concepts and results from the fields of mixed-integer and disjunctive programming to conduct a comprehensive analysis of this formulation problem: among the outcomes enabled by this novel perspective is the derivation of multiple highly-efficient formulations of the control problem, each of which represents a different tradeoff between the two most important features of a mixed-integer program, the size and the strength. First in theory, then through a numerical example, we show how all the proposed methods outperform the traditional approach employed in MPC, enabling the solution of larger-scale problems.

ABSTRACT. This work targets the development of a scalable abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on linear-time specifications, both over finite and infinite time horizons. The framework constructs a finite abstraction as an interval Markov decision process (IMDP). Then, a strategy maximizing the satisfaction probability of the given specification is synthesized over the IMDP and mapped to the underlying SHS. In contrast to existing formal approaches, by and large limited to finite-time properties and relying on conservative over-approximations, we show that the exact abstraction error is computed as a solution of convex optimization problems, and embedded into the IMDP abstraction: this allows for the quantification of the exact abstraction errors for finite- and infinite-horizon specifications, which is later used in the synthesis step. This mitigates the known state-space explosion problem: our experimental validation shows improved scalability compared to existing approaches.

ABSTRACT. The correctness of control software in many safety-critical applications such as autonomous vehicles is crucial. One technique to achieve correct control software is called "symbolic control", where complex systems are approximated by finite-state abstractions. Then, using those abstractions, provably-correct digital controllers are algorithmically synthesized for concrete systems, satisfying complex high-level requirements. Unfortunately, the complexity of synthesizing such controllers grows exponentially in the number of state variables. However, if distributed implementations are considered, high-performance computing platforms can be leveraged to mitigate the effects of the state-explosion problem.

We propose pFaces, an extensible software-ecosystem, to accelerate symbolic control techniques. It facilitates designing parallel algorithms and supervises their executions to utilize available computing resources. To demonstrate its capabilities, novel parallel algorithms are designed for abstraction-based controller synthesis. Then, they are implemented inside pFaces and dispatched, for parallel execution, in different heterogeneous computing platforms, including CPUs, GPUs and Hardware Accelerators (HWAs). Results show remarkable reduction in the computation time by several orders of magnitudes as number of processing elements (PEs) increases, which outperforms easily all the existing tools.