On Implementations of Instantaneous Actions Real-Time ASM by ASM with Delays
                A.Slissenko (joint work with J.Cohen)
                Laboratory for Algorithmics, Complexity and Logic (LACL)
                          University Paris-East (Paris 12), France

We define a notion of implementation for real-time Abstract State
Machines (ASM) with instantaneous actions by machines with delayed
actions. The time is continuous or discrete, and time constraints are
metric. Instantaneous actions ASM is an abstraction convenient for the
verification but unrealistic from the viewpoint of implementation. It
is clear that not every machine of the first type can be implemented
by a machine of the second type. We describe sufficient conditions on
ASM that permit to construct such an implementation giving a set of
runs that is close to the set of runs of the initial instantaneous
actions ASM; the closeness will be defined. The problem of properties
preservation, when implementing ASM within this framework, is briefly
discussed. A more general problem of approximate bisimulation of ASMs
with delays under desynchronization will be also discussed.