Timed substitutions for regular signal-event languages |
| |
Authors: | Béatrice Bérard Paul Gastin Antoine Petit |
| |
Affiliation: | (1) LAMSADE, Université Paris Dauphine & CNRS, Place du Maréchal de Lattre de Tassigny, 75775 Paris Cedex 16, France;(2) LSV, ENS de Cachan & CNRS, 61 av. du Président Wilson, 94235 Cachan Cedex, France |
| |
Abstract: | In the classical framework of formal languages, a refinement operation is modeled by a substitution and an abstraction by
an inverse substitution. These mechanisms have been widely studied, because they describe 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 signal-event 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 construction working
on finite and infinite signal-event words and taking into account signal stuttering, unobservability of zero-duration τ-signals and Zeno runs. Note that if several constructions have been proposed in particular cases, it is the first time that
a general construction is provided. |
| |
Keywords: | Timed automata Signal-event word Substitution Refinement Abstraction |
本文献已被 SpringerLink 等数据库收录! |
|