A simulation condition for correct asynchronous implementation of synchronous design

We study the problem of "desynchronization", i.e., semantics-preserving "asynchronous implementation" of a "synchronous design". In a synchronous design, system components (which we model as input-output automata (I/O- automata)) communicate over synchronous channels and their combined behavior can be described using synchronous composition, whereas in an asynchronous implementation, communication among components occurs over asynchronous channels (which we also model as I/O-automata) and the behavior of an asynchronous implementation can be described using asynchronous composition. The presence of asynchronous communication can result in additional behavior that is not present under synchronous communication and can thus cause the semantics of a synchronous design to be not preserved under asynchronous implementation. We formalize the notion of system response to an input sequence and by using it, define a criterion for correct desynchronization. We define the simulation of I/O-automata, and argue that the simulation of the asynchronous implementation by a synchronous design is sufficient to guarantee the correctness of desynchronization. This is a new way of characterizing the correctness of desynchronization (as compared to the "iso-/endo-chrony" type conditions proposed in previous works). Under the practical assumption that the communication delay is bounded, the proposed simulation condition is algorithmically verifiable.