Note: This content is accessible to all versions of every browser. However, this browser does not seem to support current Web standards, preventing the display of our site's design details.


STORMED hybrid systems and games

We introduce the model STORMED hybrid systems. Unlike the simple continuous dynamics of rectangular hybrid automata, or the decoupled discrete and continuous dynamics of o-minimal hybrid automata, STORMED systems allow for continuous dynamics that are rich (described in an o-minimal theory) and non-trivial interaction between discrete and continuous dynamics (no string resets). However, despite that, we show that these systems admit a finite bisimulation quotient, which can be effectively constructed under certain conditions. Thus, STORMED systems can be verified against a variety of properties automatically. We show how STORMED systems can be used to approximately model and verify any (hybrid) system, even if the system itself is not STORMED. Next, we consider STORMED games from the aspect of designing controllers that decide when and which discrete transitions to take so that certain goals are met. We show that for a variety of correctness objectives, these controllers can be synthesized. We discuss applications of all these results.

Type of Seminar:
IfA Seminar
Vladimeros Vladimerou
Electrical & Computer Engineering, University of Illinois at Urbana-Champaign
Nov 03, 2008   14:00 /

ETL K 25
Contact Person:

Prof. John Lygeros
No downloadable files available.
Biographical Sketch:
Vladimeros Vladimerou is a PhD student at the Univ. of Illinois at Urbana-Champaign (ECE Dept).He is advised by Prof. Geir Dullerud (MechSE Dept) and Prof Mahesh Viswanathan (CS Dept). He received his BSc with honors as a Fulbright scholar in 2002 and his MSc in 2004 both in ECE from UIUC. He has been designing computer systems and controls for networked autonomous vehicles for various labs at the University of Illinois since 2001. His interests include autonomous systems, hybrid system design/verification, control of complex systems and formal methods, aiming towards the design and verification of cyberphysical systems with hard guarantees on performance.