On directed transformations of delay-insensitive specifications, alternations and dynamic nondeterminism

Delay-insensitive specifications model communicating processes that are embedded in a medium that introduces arbitrary and varying delays on the communication channels. In this paper we study transformations of such specifications. The transformations we study are directed. They are either contracting or expanding. The former are useful when trying to improve specifications, the latter when trying to find implementations. The theory we develop is inspired by transformations based on handshake protocols. We show how an implementation of such a protocol can be derived. We also show how the transformations can help when analyzing specifications containing unavoidable nondeterminism, which is closely related to unavoidable metastability