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.

 gzipped postscript file.