We consider the verification problem of invariance properties for timedsystems modeled by (extended) Timed Graphs with duration variables. This problem is in general caseundecidable. Nevertheless we give in this paper...We consider the verification problem of invariance properties for timedsystems modeled by (extended) Timed Graphs with duration variables. This problem is in general caseundecidable. Nevertheless we give in this paper a technique extending a given system into anotherone containing the initial computations as well as additional ones. Then we define a digitizationtechnique allowing the translation from the continuous case to the discrete one. Using thisdigitization, we show that to each real computation in the initial system corresponds a discretecomputation in the extended system. Then, we show that the extended system corresponds to a veryclose approximation of the initial one, allowing per consequent, a good analysis of invarianceproperties of the initial system.展开更多
文摘We consider the verification problem of invariance properties for timedsystems modeled by (extended) Timed Graphs with duration variables. This problem is in general caseundecidable. Nevertheless we give in this paper a technique extending a given system into anotherone containing the initial computations as well as additional ones. Then we define a digitizationtechnique allowing the translation from the continuous case to the discrete one. Using thisdigitization, we show that to each real computation in the initial system corresponds a discretecomputation in the extended system. Then, we show that the extended system corresponds to a veryclose approximation of the initial one, allowing per consequent, a good analysis of invarianceproperties of the initial system.
