Coordination: Reo, Nets, and Logic

This article considers the coordination language Reo, a Petri net variant called zero-safe nets, and intuitionistic temporal linear logic (ITLL). The first part examines the semantics of the coordination language Reo in relation to zero-safe nets. Although the external presentations of the two models are quite different, the difference in underlying semantics is rather small. In fact, Reo connectors can be compositionally encoded into zero-safe nets. This means that the tools and techniques developed for Petri nets over the last 30 years, such as various extensions to the zero-safe nets model, such reconfigurable and dynamic nets, can be adapted to the Reo setting. The second part re-examines the idea of using linear logic as a basis for coordination languages. Specifically, we argue that intuitionistic temporal linear logic (ITLL) can encode the semantics of Reo and zero-safe nets, by encoding their notion of transaction. Moreover, by adapting the encoding and exploring the addit...

• Type: Conference
• Year: 2007
• Where: FMCO
• Authors: Dave Clarke
• Keywords: Coordination Language, Coordination Language Reo, FMCO 2007, Formal Methods, Zero-safe Nets