An Operational Semantics for Hybrid Systems Involving Behavioral Abstraction

We discuss the challenges of building a simulation framework for hybrid systems, in particular the well-known Zeno effect and correct composition of models idealised by abstracting irrelevant behavioural details (e.g. the bounce dynamics of a bouncing ball or the process of fuse melting in an electrical circuit). We ar-gue that the cornerstone of addressing these challenges is the definition of a semantic framework with an ap-propriate underlying model of time. Using two simple examples, we illustrate the prop-erties of such a model and explain why existing models are not sufficient. Finally, we propose a new Zeno-free semantic model that allows mixing discrete and con-tinuous behaviour in a rigorous way and provides for the compositional behavioural abstraction. Although it is based on non-standard analysis, we explain how our semantic model can be used to de-velop hybrid system simulators