Abstract
We present a temporal framework suitable for the specificationand 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 similarto the one usually found in discrete time temporal logics and can be safely and effectively
used in specifications aswell 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, thewell-known thermostat example.
[read the copyright and download the pdf file] [DOI]