A Generic Dynamic Logic with Applications to Interaction-Based Systems

Day - Time: 24 January 2020, h.11:30

Place: Area della Ricerca CNR di Pisa - Room: C-29

Speakers

• Rolf Hennicker (Ludwig-Maximilians-Universität München, Munich, Germany)

Referent

Maurice Henri ter Beek

Abstract

We propose a generic dynamic logic with the usual diamond andbox modalities over structured actions. Instead of using regularexpressions of actions our logic is parameterised by the form ofthe actions which can be given by an arbitrary language forcomplex, structured actions. In particular, our logic can beinstantiated by languages that describe complex interactionsbetween system components. We study two instantiations of ourlogic for specifying global behaviours of interaction-basedsystems: one on the basis of global session types and the otherone using UML sequence diagrams. Moreover, we show that ourproposed generic logic, and hence all its instantiations, satisfybisimulation invariance and a Hennessy-Milner theorem.