Determinization and expressiveness of integer reset timed automata with silent transitions

Abstract

εIRTAare a subclass of timed automata with - moves (ε-TA). They are useful for modelling global sparse time base used in timetriggered architecture and distributed business processes. In a previous paper [1], the language inclusion problem L(A) L(B) was shown to be decidable when A is an ε-TA and B is an ε-IRTA. In this paper, we address the determinization, complementation and ε-removal questions for ε-IRTA. We introduce a new variant of timed automata called GRTA. We show that for every ε-IRTA we can effectively construct a language equivalent 1-clock, deterministic GRTA with periodic time guards (but having no ε moves). The construction gives rise to at most a double exponential blowup in the number of locations. Finally, we show that every GRTA with periodic guards can be reduced to a language equivalent ε-IRTA with at most double the number of locations. Thus, ε-IRTA, periodic GRTA, and deterministic 1-clock periodic GRTA have the same expressive power and that they are all expressively complete with respect to the regular d-languages. Equivalence of deterministic and nondeterministic automata also gives us that these automata are closed under the boolean operations. © Springer-Verlag Berlin Heidelberg 2009.