Document - Realisability of global models of interaction

2023

Conference article Open Access

Realisability of global models of interaction

Ter Beek M. H., Hennicker R., Proença J.

Global interaction model Interaction-based system Communicating components Team automata Choreography automata Bisimulation equivalence

We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems--one per agent--which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations.

Source: ICTAC'23 - 20th International Colloquium on Theoretical Aspects of Computing, pp. 236–255, Lima, Perù, 4-8/12/2023

Publisher: Springer, Berlin, DEU

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:489003,
	title = {Realisability of global models of interaction},
	author = {Ter Beek M. H. and Hennicker R. and Proença J.},
	publisher = {Springer, Berlin, DEU},
	doi = {10.1007/978-3-031-47963-2_15},
	booktitle = {ICTAC'23 - 20th International Colloquium on Theoretical Aspects of Computing, pp. 236–255, Lima, Perù, 4-8/12/2023},
	year = {2023}
}