Olivier Roux and Vlad Rusu. Deciding time-bounded properties of Electre programs with stopwtach automata. In International Workshop on Hybrid Systems and Autonomous Control (WHSAC'94), Ithaca (New York, USA), pp 405-415,1994. LNCS 999.

  Abstract. We present the automatic verification of time-bounded properties of programs written in the reactive language Electre. For this, Electre programs are translated into so-called stopwatch automata, automata with chronometers to measure time. Properties are expressed in the logic TCTL and model-checking algorithms are used to verify those properties on Electre stopwtach automata. We show that bounded TCTL is decidable on stopwatch automata.