Background papers for the lectures of Prof. Vaandrager
Modeling and Verifying a Lego Car Using Hybrid I/O Automata
Hybrid I/O automata