On Timed Simulation Relations for Hybrid Systems and Compositionality

Timed and weak timed simulation relations are often used to show that operations on hybrid systems result in equivalent behavior or in conservative overapproximations. Given that systems are frequently designed and verified in a modular approach, it is desirable that this relationship is compositional, which is not the case for hybrid systems in general. We identify subclasses of linear hybrid automata that are compositional with respect to timed, respectively weak timed simulation.

• Type: Conference
• Year: 2006
• Where: FORMATS
• Authors: Goran Frehse
• Keywords: Formal Methods, FORMATS 2006, Hybrid Systems, Linear Hybrid Automata, Weak Timed Simulation