Technical Reports

Karine Altisen and Stavros Tripakis
Implementation of Timed Automata: An Issue of Semantics or Modeling? (2005)



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.

Contact | Site Map | Site powered by SPIP 3.0.25 + AHUNTSIC [CC License]

info visites 778634