ABSTRACT. With the upcoming Industry 4.0, we are facing an increasing complexification of the engineered control systems, and at the same time a need for firm guarantees on optimality and safety of their control loop. Think of a plant controlled through a wireless control network, where resource constraints limit the amount of information available to the controller, while disruptions (either malicious, or intrinsic to wireless communications) may incur loss of information between the controller and the plant. With such nonstandard non-idealities, classical control theory is not able to provide exact algorithms with guarantees of performance.

I will argue that even though these new systems are far more complex than classical textbook models, advanced techniques from Mathematics, Optimization, or Computer Science sometimes allow the recovery of the powerful properties of usual control techniques. I will exemplify this on constrained switching systems, a particular class of hybrid systems. We will see that canonical problems like stability, controllability, or identifiability, may still be exactly solved, even with guarantees on the efficiency of the algorithm. I will focus on two algorithmic techniques that are particularly well suited for challenges in Hybrid Automata: Path-Complete Lyapunov functions and Chance-Constrained Optimization.

ABSTRACT. Controller synthesis techniques based on symbolic abstractions appeal by producing correct-by-design controllers, under intricate behavioural constraints. Yet, being relations between abstract states and inputs, such controllers are immense in size, which makes them futile for embedded platforms. Control-synthesis tools such as PESSOA, SCOTS, and CoSyMA tackle the problem by storing controllers as binary decision diagrams (BDDs). However, due to redundantly keeping multiple inputs per-state, the resulting controllers are still too large. In this work, we first show that choosing an optimal controller determinization is an NP-complete problem. Further, we consider the previously known controller determinization technique and discuss its weaknesses. We suggest several new approaches to the problem, based on greedy algorithms, symbolic regression, and (muli-terminal) BDDs. Finally, we empirically compare the techniques and show that some of the new algorithms can produce up to ≈ 85% smaller controllers than those obtained with the previous technique.

ABSTRACT. Motivated by the synthesis of controllers from high-level temporal specifications, we present two algorithms to compute dominant strategies for continuous two-player zero- sum games based on the Counter-Example Guided Inductive Synthesis (CEGIS) paradigm. In CEGIS, we iteratively propose candidate dominant strategies and find counterexamples. For scalability, past work has constrained the number of counterexamples used to generate new candidates, which leads to oscillations and incompleteness, even in very simple examples. The first algorithm combines Satisfiability Modulo Theory (SMT) solving with optimization to efficiently implement CEGIS. The second abstracts previously refuted strategies, while maintaining a finite counterexample set. We characterize sufficient conditions for soundness and termination, and show that both algorithms are sound and terminate. Additionally, the second approach can be made complete to within an arbitrary factor. We conclude by comparing across different variants of CEGIS.

ABSTRACT. Abstraction-based synthesis techniques are limited to systems with moderate size. Thus to contribute towards scalability of these techniques, in this paper we propose a compositional abstraction-based synthesis for cascade interconnected discrete-time control systems. Given a cascade interconnection of several components, we provide results on the compositional construction of finite abstractions based on the notion of approximate cascade composition. Then, we provide a compositional controller synthesis for cascade interconnection. Finally, we demonstrate the applicability and effectiveness of the results using a numerical example and compare it with different abstraction and controller synthesis schemes.

ABSTRACT. This paper presents a control synthesis algorithm for dynamical systems to satisfy specifications given in a fragment of linear temporal logic. It is based on an abstraction- refinement scheme with nonuniform partitions of the state space. A novel encoding of the resulting transition system is proposed that uses binary decision diagrams for efficiency. We discuss several factors affecting scalability and present some benchmark results demonstrating the effectiveness of the new encodings. These ideas are also being implemented on a publicly available prototype tool, ARCS, that we briefly introduce in the paper.

ABSTRACT. The goal of this paper is to study sufficient conditions to stabilize an autonomous discrete-time switched system, for which the switching law should belong to a constrained language characterized by a nondeterministic automaton. Based on a decomposition into strongly connected components of the automaton, it is shown that it suffices to consider only a nontrivial strongly connected component. Sufficient conditions are provided as a set of Linear Matrix Inequalities (LMIs) related to the automaton states and associated with a min-switching strategy. Equivalence with the periodic stabilization is investigated. A numerical example is provided to illustrate the main result.

ABSTRACT. In this paper, we discuss the problem of efficient fluid mixing which is tackled by means of (approximate) dynamic programming from a switched systems perspective. In current practice, typically pre-determined periodic mixing protocols are used. As we will show in this paper, feedback control can be used to improve mixing significantly. To make this control problem tractable, temporal and spatial discretization is used by means of the cell-mapping method on the original infinite-dimensional fluid models. This translates the original control problem into the design of a (sub)optimal switching law that determines discrete mixing actions for a discrete-time switched linear system. Exploiting this switched systems perspective, a novel feedback law for mixing fluids is proposed inspired by suboptimal rollout policies in dynamic programming contexts. By design, this feedback law for mixing guarantees a performance improvement over any given (open-loop) periodic mixing protocol. This new design methodology is validated by means of simulations for the benchmark journal bearing flow showing improved performance with respect to periodic mixing strategies.

ABSTRACT. The time scale theory is introduced to study the stability of a class of switched linear systems on non-uniform time domains, where the dynamical system commutes between a continuous-time linear subsystem and a discrete-time linear subsystem during a certain period of time. Without assuming that matrices are pairwise commuting, some conditions are derived to guarantee the exponential stability of the switched system by considering that the continuous-time subsystem is stable and the discrete-time subsystem can be stable or unstable. Some examples show the effectiveness of the proposed scheme.

ABSTRACT. Reachability analysis is a powerful tool which is being used extensively and efficiently for the analysis and control of dynamical systems, especially when linear systems and convex sets are involved. In this note, we investigate whether exact or approximate reachability operations can be performed efficiently for the affine–semialgebraic setting, that is when we are dealing with general affine dynamics and basic semialgebraic sets. We show that it is partially true, we pinpoint the underlying challenges when this is not possible and indicate some directions for this case.

ABSTRACT. Probabilistic algorithms for both decision and search problems can offer significant complexity improvements over deterministic algorithms. One major difference, however, is that they may output different solutions for different choices of randomness. This makes correctness amplification impossible for search algorithms and is less than desirable in setting where uniqueness of output is important such as generation of system wide cryptographic parameters or distributed setting where different sources of randomness are used. Pseudo-deterministic algorithms are a class of randomized search algorithms, which output a unique answer with high

probability. Intuitively, they are indistinguishable from deterministic algorithms by a polynomial time observer of their input/output behavior. In this talk I will describe what is known about pseudo-deterministic algorithms in the sequential, sub-linear and parallel setting. We will also describe an extension of pseudo-deterministic algorithms to interactive proofs for search problems where the verifier is guaranteed with high probability to output the same output on different executions, regardless of the prover strategies. Based on joint work with Goldreich, Ron, Grossman and Holden.

ABSTRACT. Building Automation Systems (BAS) are exemplars of Cyber-Physical Systems (CPS), incorporating digital control architectures over underlying continuous physical processes. We provide a modular model library for BAS drawn from expertise developed on a real BAS setup. The library allows to build models comprising either physical quantities or digital control modules. The structure, operation, and dynamics of the model can be complex, incorporating (i) stochasticity, (ii) non-linearities, (iii) numerous continuous variables or discrete states, (iv) various input and output signals, and (v) a large number of possible discrete configurations. The modular composition of BAS components can generate useful CPS benchmarks. We display this use by means of three realistic case studies, where corresponding models are built and engaged with different analysis goals. The benchmarks, the model library and associated data collected from the BAS setup at the University of Oxford, are kept on-line at https://github.com/ natchi92/BASBenchmarks

ABSTRACT. Component-driven proof automation (CDPA) exploits component structure to automate deductive verification of large-scale hybrid systems with non-trivial continuous dynamics. We use CDPA to implement a case study CoasterX, which is a toolchain for designing and verifying safety of 2-dimensional roller coaster track designs. Specifically, we verify velocity and acceleration bounds. CoasterX starts with a graphical front-end for point-and-click design of tracks. The CoasterX back-end then automatically specifies and verifies the track in differential dynamic logic (dL) with a custom procedure built in the KeYmaera X theorem prover. We show that the CDPA approach scales, testing real coasters of up to 56 components.

ABSTRACT. Arguments are presented in favor of modeling sewer systems and in particular Dutch sewer systems as a sampled data system with events. Basic limitations on controlling these systems when ignoring their hybrid nature are stated. The traditional control scheme for the Dutch systems is given as an example of event driven local control. Basic limitations on systems using a sampled data approach without an event driven component are derived. To provide context a brief description of a sampled data controller for a sewer system based on set-point tracking is given. This is followed by an explanation of how the absence of event driven control limits its effectiveness.

ABSTRACT. In this paper, we present extensions to Unmanned Systems Autonomy Services (UxAS) to handle mission specifications that require a synchronization of task execution. UxAS uses Process Algebra (PA) as a formal language to specify mission requirements for unmanned aerial vehicle (UAV) operations. However, the current implementation of PA in UxAS utilizes assigned semantics which does not guarantee the order of task completion and is unable to provide a mission planning required vehicle-synchronization. To enable the capability of UxAS in operating synchronized mission specifications, we introduce a notion of Synchronized Process Algebra (SPA) which extends PA by adding a synchronized composition operator to the syntax of PA. Such an operator allows us to specify the task’s duration and enforce the next task is executed after the previous one has terminated. Moreover, we provide a new service in UxAS, called Temporal Service (TS) to control the flow of the planning process with respect to timing specifications. We apply SPA and TS to specify and operate the mission specification of a forest fire rescue scenario required the synchronized arrivals of multiple UAVs.

ABSTRACT. The formal verification and controller synthesis for general Markov decision processes (gMDPs) that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximate abstractions. In this paper, we contribute to the state of the art of control synthesis for temporal logic properties by computing and quantifying a less conservative gridding of the continuous state space of linear stochastic dynamic systems and by giving a new approach for control synthesis and verification that is robust to the incurred approximation errors. The approximation errors are expressed as both deviations in the outputs of the gMDPs and in the probabilistic transitions.

ABSTRACT. This paper studies estimation of reach probability for a generalized stochastic hybrid system (GSHS). For diffusion processes a well-developed approach in reach probability estimation is to introduce a suitable factorization of the reach probability and then to estimate these factors through simulation of an Interacting Particle System (IPS). The theory of this IPS approach has been extended to arbitrary strong Markov processes, which includes GSHS executions. Because Monte Carlo simulation of GSHS particles involves sampling of Brownian motion as well as sampling of random discontinuities, the practical elaboration of the IPS approach for GSHS is not straightforward. The aim of this paper is to elaborate the IPS approach for GSHS by using complementary Monte Carlo sampling techniques. For a simple GSHS example, it is shown that and why the specific technique selected for sampling discontinuities can have a major influence on the effectiveness of IPS in reach probability estimation.

ABSTRACT. In this work, we propose a stratified sampling method to statistically check Probabilistic Computation Tree Logic (PCTL) formulas on discrete-time Markov chains with sequential probability ratio test. Distinct from previous statistical verification methods using independent Monte Carlo sampling, our algorithm uses stratified samples that are negatively correlated, thus give lower variance. The experiments demonstrate that the new algorithm uses a smaller number of samples for a given confidence level on several benchmark examples.

ABSTRACT. This work introduces a new abstraction technique for reducing the state space of large, discrete-time labelled Markov chains. The abstraction leverages the semantics of interval Markov decision processes and the existing notion of approximate probabilistic bisimulation. Whilst standard abstractions make use of abstract points that are taken from the state space of the concrete model and which serve as representatives for sets of concrete states, in this work the abstract structure is constructed considering abstract points that are not necessarily selected from the states of the concrete model, rather they are a function of these states. The resulting model presents a smaller one-step bisimulation error, when compared to a like-sized, standard Markov chain abstraction. We outline a method to perform probabilistic model checking, and show that the computational complexity of the new method is comparable to that of standard abstractions based on approximate probabilistic bisimulations.

ABSTRACT. In this paper, we introduce operators, semantics, and conditions that, when possible, are solution-independent to guarantee basic temporal logic specifications for hybrid dynamical systems. Employing sufficient conditions for forward invariance and finite time attractivity of sets for such systems, we derive such sufficient conditions for the satisfaction of formulas involving temporal operators and atomic propositions. Furthermore, we present how to certify formulas that have more than one operator. Academic examples illustrate the results throughout the paper.

ABSTRACT. We study the problem of computing input signals that produce system behaviors that falsify requirements written in temporal logic. We provide a method to automatically search for falsifying time varying uncertain inputs for nonlinear and possibly hybrid systems. The input to the system is parametrized using piecewise constant signals with varying switch times. By applying small perturbations to the system input in space and time, and by using gradient descent approach, we try to converge to the worst local system behavior. The experimental results on non-trivial benchmarks demonstrate that this local search can significantly improve the rate of finding falsifying counterexamples.

ABSTRACT. We introduce a new formalism of higher-dimensional timed automata, based on van Glabbeek’s higher-dimensional automata and Alur’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also show how to use tensor products to combat state-space explosion and how to extend the setting to higher-dimensional hybrid automata.

ABSTRACT. We consider the stability and the input-output analysis problems of a class of large-scale hybrid systems composed of continuous dynamics coupled with discrete dynamics defined over finite alphabets, e.g., deterministic finite state machines (DFSMs). This class of hybrid systems can be used to model physical systems controlled by software. For such classes of systems, we use a method based on dissipativity theory for compositional analysis that allows us to study stability, passivity and input-output norms. We show that the certificates of the method based on dissipativity theory can be computed by solving a set of semi-definite programs. Nonetheless, the formulation based on semi-definite programs become computationally intractable for relatively large number of discrete and continuous states. We demonstrate that, for systems with large number of states consisting of an interconnection of smaller hybrid systems, accelerated alternating method of multipliers can be used to carry out the computations in a scalable and distributed manner. The proposed methodology is illustrated by an example of a system with 60 continuous states and 18 discrete states.

ABSTRACT. In this work, we investigate some Razumikhin-type criteria for the uniform global practical asymptotic stability on arbitrary time domains, for time-varying dynamic equations. Using Lyapunov-type functions on time scales, we develop appropriate inequalities ensuring that trajectories decay to the neighborhood of the trivial solution asymptotically. Some numerical examples are discussed to illustrate our results.

ABSTRACT. It is well known that for switched systems the overall dynamics can be unstable despite stability of all individual modes. We show that this phenomenon can indeed occur for a linearized DAE model of power grids. By making certain topological assumptions on the power grid, we can ensure stability under arbitrary switching for the linearized DAE model.