S | |
---|---|
[SBM14] | Ocan Sankur,
Patricia Bouyer, and
Nicolas Markey.
Shrinking Timed Automata.
Information and Computation 234:107-132. Elsevier, February 2014.
@article{icomp234()-SBM, author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas}, title = {Shrinking Timed Automata}, publisher = {Elsevier}, journal = {Information and Computation}, volume = {234}, pages = {107-132}, year = {2014}, month = feb, doi = {10.1016/j.ic.2014.01.002}, 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, non-blockingness and time-abstract simulation are preserved in implementation.}, } |
- 1
- 1
- 1