Interpreting Reo Circuits as PDL models

Abstract

Reo is a coordination-based language with the proposal of connecting different systems and interfaces. It aims to develop communication between different systems with a high level of abstraction and without many restrictions. PDL is a multimodal logic tailored to reason about programs. It is proved to be sound, complete, decidable and has a simple Kripke semantics. This work intends to provide an interpretation of Reo circuits as PDL models. These are the first steps towards providing a dynamic logic tailored to reason directly about Reo circuits.