Verification of context-free timed systems using linear hybrid observers

Abstract

We address the verification problem of infinite timed systems. We consider context-free timed systems defined as a generalization of the (regular) timed graphs [ACDg0]. Then, we propose decision procedures for the verification of invariance properties of these systems, expressed by means of observation variables. These variables record relevant informations about the computations of the observed system. They are permanently updated along these computations without any interference with the behaviour of the system. Observation variables are either additional clocks (timers), nonbounded integer variables (accumulators), or constant slope continuous (real valued) variables (integrators).