Monotonic hybrid systems

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.