Nicolas Markey

Abstract

We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce parametric shrinking of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata both properties are preserved in implementation.

@inproceedings{fsttcs2011-SBM,
  author =              {Sankur, Ocan and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Shrinking Timed Automata},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  pages =               {90-102},
  year =                {2011},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2011.90},
  abstract =            {We define and study a new approach to the
                         implementability of timed automata, where the
                         semantics is perturbed by imprecisions and finite
                         frequency of the hardware. In order to circumvent
                         these effects, we introduce \emph{parametric
                         shrinking} of clock constraints, which corresponds
                         to tightening the guards. We propose symbolic
                         procedures to decide the existence of (and then
                         compute) parameters under which the shrunk version
                         of a given timed automaton is non-blocking and can
                         time-abstract simulate the exact semantics. We then
                         define an implementation semantics for timed
                         automata with a digital clock and positive reaction
                         times, and show that for shrinkable timed automata
                         both properties are preserved in implementation.},
}