Talk "A dynamic logic for systems with predicate-based communication"

by Rolf Hennicker

Tue, 06 September 2022 at 12:30 pm in Lipari, Italy

Joint work with: Martin Wirsing

Abstract: Attribute-based broadcast communication is a novel paradigm for modelling interactions in collective systems. Used by several new languages (such as SCEL, CARMA, and AbC), it enables senders and groups of receivers to interact by considering predicates over their current attribute values. In these languages systems are modelled by the parallel composition of components, each component being equipped with a local process description. We complement this local view by a global requirements specification format that allows us to specify abstract properties, like safety and liveness, as well as allowed and forbidden interaction scenarios. We propose a first-order dynamic logic whose atomic actions are tailored to the needs of systems of collaborating components with multi-cast communication. As implementation language we consider (a variant of) the AbC calculus and show how our global ensemble specifications can be realised with local process declarations. Our correctness notion relates the semantics of global specifications to the labelled transition system semantics of AbC systems.