A Nonarchimedian Discretization of Timed
Languages
We give a new discretization of behaviors
of timed automata. In this discretization, timed languages are
represented as sets of words containing action symbols, a clock tick
symbol 1,
and two delay symbols: a
negative delay and positive delay. Unlike the region construction, our
discretization commutes with intersection. We show that discretizations
of timed automata are, in general, context-sensitive languages and give
a class of automata that equals the class of languages that are
discretizations of timed automata,
and show that their emptiness problem is decidable.
“Proceedings of 1st International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS'03)”, Springer Verlag, Lecture Notes in Computer Science, vol. 2791, pages 168-181, 2003.