Branching Pomsets for choreographies – adding choices to pomsets

Last updated on May 21, 2024 2 min read
Slides (@DCC-Talks) Slides (@ICE'23 by Luc) Slides (@ICE'22 by Luc) JLAMP'23 paper ICE'22 paper Tool

– Slides for this presentation @ FCUP, Portugal–

Choreographic languages describe possible sequences of interactions among a set of agents. Typical models are based on languages or automata over sending and receiving actions. Pomsets provide a more compact alternative by using a partial order to explicitly represent causality and concurrency between these actions. However, pomsets offer no representation of choices, thus a set of pomsets is required to represent branching behaviour. For example, if an agent Alice can send one of two possible messages to Bob three times, one would need a set of 2 × 2 × 2 distinct pomsets to represent all possible branches of Alice’s behaviour. In this talk we propose an extension of pomsets, named branching pomsets, with a branching structure that can represent Alice’s behaviour using 2 + 2 + 2 ordered actions. We encode choreographies as branching pomsets and define well-formedness conditions on branching pomsets, inspired by multiparty session types, which are sufficient to show realisability of the represented communication protocol.

This is joint work with Luc Edixhoven, Sung-Shik Jongmans, and Ilaria Castellani.

José Proença
José Proença
Assistant Professor

José Proença is an Assistant Professor at Faculty of Science of the University of Porto, and a researcher at the Research Center in Real-Time & Embedded Computing Systems, ISEP, in Portugal. His core research targets coordination aspects and formal methods in the context of Cyber-Physical Systems. He is actively involved in a NextGenerationEU project and in 1 FCT project. He currently belongs to the steering committee of 2 international conferences in fundamental computer science, he chaired the program committee of 6 international research venues with edited proceedings, edited 2 journal volumes, and was the member of 19 program-committees of international venues.