Statistical Validation and Principle-Based Simulation of Complex Cyber-Controlled Systems

ABSTRACT: The talk will focus on simulation and a computational approach to verification of the hybrid mathematical models that are formed when combining physics-based models with discrete-transition models, such as those which model software algorithms. Namely, the mathematical models that arise when for instance considering Cyberphysical Systems, or the Internet of Things.

In many game theory and filtering problems it is not possible to analytically obtain solutions for statistical properties of systems under study, and in the first part of the talk we will describe our recent work on numerical approaches to obtaining estimates of these properties, and the application of the techniques developed to particle filtering. Monte Carlo simulation of Markov processes allows the numerical estimation of their statistical properties from an ensemble of sample system paths. We present methods for generating reduced-variance path ensembles for the tau-leaping discrete-time simulation algorithm, which allows mean stochastic process dynamics to be estimated with substantially smaller ensemble sizes. Our methods are based on antithetic and stratified sampling of Poisson random variates, and we provide a combination of analytical proofs and numerical evidence for their performance, which can frequently be a 2-3 orders of magnitude improvement over standard Monte Carlo. Application examples will be discussed.

The second part of the talk will concentrate on system verification, and will present a new verification algorithm for continuous-time stochastic hybrid systems, whose specifications are expressed in metric interval temporal logic (MITL), by deploying a novel model reduction method. By partitioning the state space of the hybrid system and computing the optimal transition rates between partitions, we provide a procedure to both reduce the system to a continuous-time Markov chain, and the associated specification formulas. We prove that the unreduced formulas hold (or do not) if the corresponding reduced formula on the Markov chain is robustly true (or false) under certain perturbations. In addition, a stochastic algorithm to complete the verification has been developed. We have extended the approach of this algorithm, and have developed a direct stochastic algorithm for probabilistically verifying a certain hybrid system class, and applied this technique to an extensive benchmark problem with realistic dynamics.

BIO: Geir E. Dullerud is the W. Grafton and Lillian B. Wilkins Professor in Mechanical Engineering at the University of Illinois at Urbana-Champaign. There he is also a member of the Coordinated Science Laboratory, where he is Director of the Decision and Control Laboratory (21 faculty); he is an Affiliate Professor of both Computer Science, and Electrical and Computer Engineering. He has held visiting positions in Electrical Engineering KTH, Stockholm (2013), and Aeronautics and Astronautics, Stanford University (2005-2006). Earlier he was on faculty in Applied Mathematics at the University of Waterloo (1996-1998), after being a Research Fellow at the California Institute of Technology (1994-1995), in the Control and Dynamical Systems Department. He has published two books: “A Course in Robust Control Theory”, Texts in Applied Mathematics, Springer, 2000, and “Control of Uncertain Sampled-data Systems”, Birkhauser 1996. His areas of current research interest include convex optimization in control, cyber-physical system security, cooperative robotics, stochastic simulation, and hybrid dynamical systems. In 1999 he received the CAREER Award from the National Science Foundation, and in 2005 the Xerox Faculty Research Award at UIUC. He is a Fellow of both IEEE (2008) and ASME (2011).

Co-hosted by Paul Bogdan