Compositionality of safe communication in systems of team automata

Ter Beek M. H., Hennicker R., Kleijn J.

Synchronisation policy  Compliance  Team Automata  Reactive components  Compositionality  Safe communication 

We study guarantees for safe communication in systems of systems composed of reactive components that communicate through synchronised execution of common actions. Systems are modelled as (extended) team automata, in which, in principle, any number of component automata can participate in the execution of a communicating action, either as a sender or as a receiver. We extend team automata with synchronisation type specifications, which determine specific synchronisation policies fine-tuned for particular application domains. On the other hand, synchronisation type specifications generate communication requirements for receptiveness and responsiveness. We propose a new, liberal version of requirement satisfaction which allows teams to execute arbitrary intermediate actions before being ready for the required communication, which is important in practice. Then we turn to the composition of systems and show that composition behaves well with respect to synchronisation type specifications. As a central result, we investigate criteria that ensure the preservation of local communication properties when (extended) team automata are composed. This is particularly challenging in the context of weak requirement satisfaction.

Source: ICTAC'20 - 17th International Colloquium on Theoretical Aspects of Computing, pp. 200–220, Macau, China, 30/11/2020-04/12/2020

Metrics