Verification of Duration Systems Using an Approximation Approach

We consider the verification problem of invariance properties for timed systems modeled by (extended) Timed Graphs with duration variables. This problem is in general case undecidable. Nevertheless we give in this paper a technique extending a given system into another one containing the initial computations as well as additional ones. Then we define a digitization technique allowing the translation from the continuous case to the discrete one. Using this digitization, we show that to each real computation in the initial system corresponds a discrete computation in the extended system. Then, we show that the extended system corresponds to a very close approximation of the initial one, allowing per consequent, a good analysis of invariance properties of the initial system.