Monotonic hybrid systems

AbstractMany physical events assume values that can be represented with functions that are monotonic with respect to time passing. This paper defines the class of Monotonic Hybrid Systems, namely Hybrid Systems where activities and assignments are monotonic functions.On the basis that, among Hybrid Systems, Integrator Systems (which are Hybrid Systems equipped with stopwatches) are the most expressive of the classes with a linear evolution law, and that Timed Systems (which are Hybrid Systems equipped with clocks) enjoy most of the decidable properties required, we compare Monotonic Hybrid Systems with the above classes, with respect to decidability, expressiveness and succinctness. We show that a subclass of Monotonic Hybrid Systems is equivalent to Integrator Systems and Timed Systems with discrete time assumption, but that it strictly contains them when assuming dense time. This has practical consequences both in the discrete and dense context when symbolic verification is not possible. We also show that Monotonic Hybrid Systems allow more succinct descriptions than those of Integrator and Timed Systems. This result shows that not only hierarchy, non-determinism and communication, as already noticed in Alur et al. (Proceedings of the HSCC 00, Lecture Notes in Computer Science, Springer, Berlin, 2000, pp. 6–19) and Grosu and Stauner (Formal Methods System Design) 21 (2002) 5), have an impact on succinctness, but also the shape of functions used in descriptions does.For a subclass of Monotonic Hybrid Systems for which reachability is decidable if the functions used are computable, we consider both the problem of verifying properties written in a suitable logic and also the relationship between dense time and discrete time assumptions in the framework of verification. The formalism and the results are illustrated by some examples