Retiming Techniques for Statecharts

. We consider a version of Statecharts having transitions with durations. We relate occurrences of transitions with a dense time domain and enforce a strong time semantics. We examine how durations associated with transitions can be changed while preserving behaviour (a retiming). We discuss also how a class of changes of the temporal feature of the environment (i.e. from non-discrete to discrete and vice-versa, shift, speed-up and slow-down) affect behaviour. 1 Introduction Statecharts (see [3]) are a graphical specification formalism that enriches statetransition diagrams with hierarchical structure on states and with graphical conventions for explicitly representing parallelism and communication among parallel components. Statecharts have been originally endowed with a step semantics that enforces a synchrony hypothesis (a number of variants of this semantics can be found in [4, 5, 10, 13, 14]). The environment prompts a statechart with events which are related to a discrete time d..