Detalhes
Nome
José Paiva ProençaCargo
Investigador Colaborador ExternoDesde
01 março 2013
Nacionalidade
PortugalCentro
Laboratório de Software ConfiávelContactos
+351253604440
jose.p.proenca@inesctec.pt
2024
Autores
Edixhoven, L; Jongmans, SS; Proença, J; Castellani, I;
Publicação
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
Abstract
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/).
2023
Autores
Proença, J; Edixhoven, L;
Publicação
Coordination Models and Languages - 25th IFIP WG 6.1 International Conference, COORDINATION 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings
Abstract
2023
Autores
ter Beek, MH; Cledou, G; Hennicker, R; Proenca, J;
Publicação
FORMAL METHODS, FM 2023
Abstract
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receivesmust be satisfied). Previouswork focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.
2023
Autores
Proença, J; Pereira, D; Nandi, GS; Borrami, S; Melchert, J;
Publicação
Proceedings of the First Workshop on Trends in Configurable Systems Analysis, TiCSA@ETAPS 2023, Paris, France, 23rd April 2023.
Abstract
[No abstract available]
2023
Autores
Spilere Nandi, G; Pereira, D; Proença, J; Tovar, E; Rodriguez, A; Garrido, P;
Publicação
Open Research Europe
Abstract
The access to the final selection minute is only available to applicants.
Please check the confirmation e-mail of your application to obtain the access code.