Stability of Real-Time Abstract State Machines under Desynchronization

In our paper TR-LACL-2008---02 (www.univ-paris12.fr/lacl/) we give sufficient conditions that permit to implement a real-time ASM with instantaneous actions (IA-ASM) by an ASM with delayed actions (DA-ASM) with approximate bisimulation of runs. The time is continuous and time constraints are linear inequalities with rational coefficients. As IA-ASM we consider ASM whose programs are blocks of ifguardthenblockOfUpdates. The implementation is an ASM of more general type. It works by 2 phases: backup phase memorizes the values of functions, and update phase makes the updates using the backed up values. Such an implementation implies shifts of time instants and, consequently, of the values of the real-valued functions. The approximation of runs (and, thus approximate bisimulation) is determined by 2 positive parameters , where bounds time shifts, and bounds the deviations of real-valued functions. We introduce a notion of -sturdy IA-ASM, and prove that the implementation of any such IA-ASM gives an DA-ASM with -approximately bisimular runs if the delay satisfies some constraints. An interesting point is that the sources of desynchronization that destroy the bisimulation are much more subtle and numerous than one can think a priori. Another conceptual consequence concerns the adequacy of the notion of IA-ASM that was introduced in Gurevich---Huggins (LNCS, vol. 1092, 1996), and later studied in Beauquier---Slissenko, (APAL, 113(1---3):13---52, 2002) for the specification of real-time system.