Preservation of LTL properties in desynchronized systems

The synchronous programming model is perfect for modeling, simulation, verification and implementation of reactive systems. While this paradigm can be directly implemented as hardware circuits, multithreaded software implementations are typically based on asynchronous threads. For this reason, an efficient multithreaded software implementation of a synchronous program requires a so-called desynchronization that could however potentially violate the already verified properties of the synchronous program. In this paper, we therefore present a theory to check whether properties verified for a synchronous system are preserved by a desynchronization. In particular, we prove a theorem based on directed-flow equivalence that specifies the requirements of delay relations among system variables that a desynchronization has to meet.