Extending Esterel by Asynchronous Concurrency1

Synchronous languages like Esterel and PURR have been introduced to support the development of concurrent reactive systems. These languages have an easily understood semantics that lends itself well for efficient imple-mentations and also for a formal verification of the designs. We show how to enrich Esterel or PURR by two important features, namely asynchronous concurrency and nondeterminism. These features are important for (1) describing asynchronous systems and (2) for using PURR as a modeling language. We introduce the new constructs on the basis of a compilation oriented transition semantics of a core portion of PURR