Timed substitutions for regular signal-event languages

In the classical framework of formal languages, a refinement n is modeled by a substitution and an abstraction by an inverse substitution. These mechanisms have been widely studied, because they a change in the specification level, from an abstract view to a more concrete one, or conversely. For timed systems, there is up to now no uniform notion of substitution. In this paper, we study timed substitutions in the general framework of signal-event languages, where both signals and events are taken into account. We prove that regular signalevent languages are closed under substitution and inverse substitution. To obtain these results, we use in a crucial way a “well known” result: regular signal-event languages are closed under intersection. In fact, while this result is indeed easy for languages defined by Alur and Dill’s timed automata, it turns out that the construction is much more tricky when considering the most involved model of signal-event automata. We give here a const...

• Type: Journal
• Year: 2007
• Where: FMSD
• Authors: Béatrice Bérard, Paul Gastin, Antoine Petit
• Keywords: FMSD 2007, Formal Languages, Inverse Substitution, Signal-event Languages