Affiliations: Université Paris-Est, LACL (EA 4219), UPEC, 61 avenue du Général de Gaulle, 94010 Créteil Cedex, France. [email protected]
Note: [] Address for correspondence: Université Paris-Est, LACL (EA 4219), UPEC, 61 avenue du Général de Gaulle, 94010 Créteil Cedex, France
Abstract: We give a discretization of behaviors of timed automata, in which timed languages are represented as sets of words containing action symbols, a clock tick symbol 1, and two delay symbols δ− (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 over Σ ∪ {1, δ+, δ−}, and give a class of counter automata that accepts exactly the class of languages that are discretizations of timed automata, and show that its emptiness problem is decidable.
