Verifying invariance properties of timed systems with duration variables

Abstract

We consider the verification problem of invariance properties for timed systems modeled by (extended) Timed Graphs with duration variables. While clocks of a Timed Graph can be seen as continuous (real valued) variables with rates 1 at each control location of the system, duration variables (also called integrators) are continuous variables having rates 0 or 1. The use of integrators allows to reason about the accumulated delays spent at some particular locations during some computation. We show that under some conditions, the verification problem of invariance properties is decidable for (closed) Timed Graphs with one integrator, the integrator can be tested and/or reset at any transition. For this, we use a new digitization technique and prove that every real computation of such systems has a valid digitization. Then, we show how to solve the verification problem in the case of a discrete time domain.