Seminars

Crossing the bridge between similar games PDF files
Jan-David Quesel, Research Assistant/Grad student, University of Oldenburg, Dept. of Computing Science

Fri 12/02/2011, 2:00 PM, GHC-6501

Abstract

Specifications and implementations of complex physical systems tend to differ as low level effects such as sampling are often ignored when high level models are created. Thus, the low level models are often not exact refinements of the high level specification. However, they are similar to those. To bridge the gap between those models, we study robust simulation relations for hybrid systems. We identify family of robust simulation relations that allow for certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of simulation a broad class of logical properties is preserved. The question whether two systems are in simulation relation can be reduced to a reach avoid problem for hybrid games. We provide a sufficient condition under which a winning strategy for these games exists.

Biography

Jan-David Quesel is a research assistant at the University of Oldenburg, Germany. In his diploma thesis (MSc), he developed, under supervision of Andre Platzer, KeYmaera, a theorem prover for hybrid systems based on the proof calculus for differential dynamic logic. Since June 2007, he is working for his PhD, under supervision of Ernst-Ruediger Olderog, on the topic of hybrid system similarity. His research interests range from the verification of hybrid and timed systems, semantics of those, and logics to theorem proving and model-checking.