Realisability of Global Models of Interaction
Ref: CISTER-TR-231207 Publication Date: 8, Dec, 2023
Realisability of Global Models of Interaction
Ref: CISTER-TR-231207 Publication Date: 8, Dec, 2023Abstract:
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.
Maurice H. ter Beek
José ProençaDocument:
View
DownloadICTAC - 20th International Colloquium on Theoretical Aspects of Computing.
Lima, Peru.
Record Date: 4, Dec, 2023