Time Domains in Hybrid Systems Modeling
Abstract:
Hybrid systems modeling languages like Simulink/Stateflow or Modelica allow for combining discrete- and continuous-time dynamics with intricate interactions between them. A key issue is the faithful simulation and analysis of hybrid systems models, based on a rigorous mathematical semantics of the modeling language.
Choosing an appropriate model of time is the first and decisive step towards the definition of such semantics. In this talk we will compare two time domains:
(i) The Super-Dense Time, first proposed by A. Pnueli to reconcile software behavior where computations are deemed instantaneous with the synchronous nature of physics;
(ii)The Non-Standard Time, that offers the capability to analyze hybrid systems behavior either at a macroscopic time-scale, under the usual smoothness assumptions, or at an infinitesimal time-scale, whenever a non-smooth behavior is expected.
We will compare the merits of the two time domains with respect to (i) their expressiveness and (ii) their use in the mathematical semantics of modeling languages. Several questions will be of interest: Are the semantics compositional? Does they require smoothness assumptions? Can they cope with Zeno or chattering behavior? Are they useful to prove the soundness of model analyses or transformations? Do they help the generation of correct simulation code? We will illustrate our talk with the study of the Zélus modeling language, a Lustre-like synchronous language extended with hierarchical automata and Ordinary Differential Equations (ODEs).
This talk is based on a joint work by A. Benveniste (Inria), T. Bourke (Inria), B. Caillaud (Inria), B. Pagano (Ansys) and M. Pouzet (ENS Paris / Inria).