Prof. Martin Fränzle
Biography
Prof. Martin Fränzle holds a position as full professor for hybrid discrete-continuous systems at the Department of Computing Science at the Carl von Ossietzky Universität Oldenburg, Germany. His research interests are in modelling, verification, and synthesis of reactive, real-time, and hybrid dynamics in embedded and cyber-physical systems. He has worked on the semantics of high-level modelling and specification languages and on decision problems and their application to verifying and synthesizing real-time and hybrid discrete-continuous systems including settings subject to stochastic disturbances. The complexity barrier rapidly hit by such automated verification and synthesis procedures has been attacked through extending bounded model checking to very expressive temporal logics, branching-time abstractions, and by developing SAT-modulo-theory techniques for arithmetic constraint solving and tailoring them to the specific formulae structures arising in different verification domains and in synthesis. Furthermore, SAT-modulo-theory techniques for arithmetic constraint solving have been extended to the undecidable domain of arithmetic constraints involving transcendental functions and ordinary differential equations as well as to stochastic variants facilitating the fully symbolic analysis of probabilistic hybrid systems. Another major line of research deals with robust notions of system correctness, i.e. with the construction of correctness certificates which remain valid under the ubiquitous kinds of disturbances like, e.g., manufacturing tolerances or incomplete information. Fundamental research on these topics has mostly been pursued within large collaborative research projects, like the Transregional Collaborative Research Center SFB-TR 14 AVACS (Automatic Verification and Analysis of Complex Systems) or recently the Research Training Group DFG GRK 1765 SCARE (System Correctness under Adverse Conditions).
Abstract
For a quarter of a century, hybrid automata and closely related models have served as a workhorse for capturing and formally analyzing the coupled dynamics of discrete and continuous components within cyber-physical systems (CPS). Despite continuous progress concerning scalability both in the continuous and the discrete state space as well as concerning the shapes of continuous dynamics covered, the underlying computational model increasingly shows its limitations. While extensions of hybrid automata to probabilistic or stochastic dynamics are available and see first experimental tool support, other limitations leading to bad alignment with the dynamics of the objects of discourse, namely CPS, have not really been addressed so far. Of particular importance are delays in feedback loops, as pertinent to networked CPS or systems of CPS, as well as a fundamental gap between all current hybrid-automata variants and concepts from metrology found in virtually all engineered control systems, namely state estimation under uncertainty.
In this series of lectures, we will explain hybrid automata models of various flavors (deterministic, non-deterministic, probabilistic, stochastic) and related automatic verification methods based on arithmetic constraint solving. From there on, we will proceed to models of cyber-physical systems involving delayed feedback as well as to models of cyber-physical systems counteracting measurement errors by means of optimal state estimation, a.k.a. filtering. We will demonstrate that even the most advanced traditional hybrid automata models cannot adequately encode the effects of these omnipresent features of CPS and will suggest corresponding models, thereby also shedding light on the germs of corresponding automatic verification procedures.
(It would be great if the attendees are able to have access to computers running Linux during lessons since the SMT solver iSAT, which runs under Linux only and could be downloaded from https://projects.avacs.org/projects/isat/, will be used.)