Past Event: Oden Institute Seminar

Statistical Validation and Principle-Based Simulation of High-Dimensional Hybrid Systems

Geir E. Dullerud , Professor, University of Illinois

Abstract

The presentation will focus on a simulation and 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, filtering problems and verification problems it is not possible to analytically obtain solutions for statistical properties of systems under study. In the first section 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 probabilistic verifying a certain hybrid system class, and applied this technique to an extensive benchmark problem with realistic dynamics. In the second part of the talk we will describe our recent work on numerical approaches to obtaining estimates of statistical properties of Markov processes, in particular mean-square estimation. 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. Also presented will be the HoTDeC multi-vehicle, which consists of indoor airborne and ground-based vehicles.