Verification of Duration Systems Using an Approximation Approach

We consider the verification problem of invariance properties for timedsystems modeled by (extended) Timed Graphs with duration variables. Thisproblem is in general case undecidable. Nevertheless we give in this paper atechnique extending a given system into another one containing the initialcomputations as well as additional ones. Then we define a digitizationtechnique allowing the translation from the continuous case to the discreteone. Using this digitization, we show that to each real computation in theinitial system corresponds a discrete computation in the extended system.Then, we show that the extended system corresponds to a very closeapproximation of the initial one, allowing per consequent, a good analysisof invariance properties of the initial system.