Branching pomsets: Design, expressiveness and applications to choreographies

• Tipo: Artigo em Revista Científica Internacional
• Data: 2024

Autores

Edixhoven, L (Autor) Outra; Jongmans, SS (Autor) Outra; Proença, J (Autor) FCUP; Castellani, I (Autor) Outra

Revista

Título: Journal of Logical and Algebraic Methods in Programming

Vol. 136

ISSN: 2352-2208

Editora: Elsevier

Indexação

ISI Web of Knowledge - 0 Citações

Scopus - 0 Citações

Outras Informações

ID Authenticus: P-00Z-5HY

DOI: 10.1016/j.jlamp.2023.100919

Abstract (EN): 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 x 2 x 2 distinct pomsets to represent all possible branches of Alice's behaviour. This paper proposes an extension of pomsets, named branching pomsets, with a branching structure that can represent Alice's behaviour using 2 + 2 + 2 ordered actions. We compare the expressiveness of branching pomsets with that of several forms of event structures from the literature. We encode choreographies as branching pomsets and show that the pomset semantics of the encoded choreographies are bisimilar to their operational semantics. Furthermore, we define well-formedness conditions on branching pomsets, inspired by multiparty session types, and we prove that the well-formedness of a branching pomset is a sufficient condition for the realisability of the represented com-munication protocol. Finally, we present a prototype tool that implements our theory of branching pomsets, focusing on its applications to choreographies. (c) 2023 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 36