Karine Altisen and
Stavros Tripakis
Implementation of Timed Automata: An Issue of Semantics or Modeling? (2005)
Implementation of Timed Automata: An Issue of Semantics or Modeling? (2005)
TR-2005-12.pdf
Keywords:
Abstract: In this paper we study to what extent implementation of timed automata can be achieved using the standard semantics and ap- propriate modeling, instead of introducing new semantics. We propose an implementation methodology which allows to transform a timed automa- ton into a program and to check whether the execution of this program on a given platform satisfies a desired property. This is done by model- ing the program and the execution platform, respectively, as an untimed automaton and a collection of timed automata. We also study the prob- lem of property preservation, in particular when moving to a better execution platform. We show that some subtleties arise regarding the definition of better, in particular for digital clocks. The fundamental issue is that faster clocks result in better sampling and therefore can introduce more behaviors.
