Automated Verification of Continuous Time Systems by Discrete Temporal Induction

We present a temporal framework suitable for the specification and verification of safety properties of real time hybrid systems. We show that, given suitable assumptions (like non Zenoness and left continuity) continuous time can be discretized by introducing a next operator that is similar to the one usually found in discrete time temporal logics and can be safely and effectively used in specifications as well as in verification. The proofs of properties can be conducted in a deductive style, and can be easily automated, especially when they are based on induction. We validate this approach by applying it to a simple hybrid system, the well-known thermostat example.