A Unifying Framework for Deciding Synchronizability

Benedikt Bollig (1) , Cinzia Di Giusto (2) , Alain Finkel (1, 3) , Laetitia Laversa (2) , Etienne Lozes (2) , Amrita Suresh (1, 4)

1 LMF - Laboratoire Méthodes Formelles
2 I3S - Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis
3 IUF - Institut universitaire de France
4 CHROMA - Robots coopératifs et adaptés à la présence humaine en environnements dynamiques

Several notions of synchronizability of a message-passing system have been introduced in the literature. Roughly, a system is called synchronizable if every execution can be rescheduled so that it meets certain criteria, e.g., a channel bound. We provide a framework, based on MSO logic and (special) tree-width, that unifies existing definitions, explains their good properties, and allows one to easily derive other, more general definitions and decidability results for synchronizability.

Mots clés: communicating finite-state machines; message sequence charts; synchronizability; MSO logic; special tree-width

Domaines: Théorie et langage formel [cs.FL]

Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, et al.. A Unifying Framework for Deciding Synchronizability. CONCUR 2021 - 32nd International Conference on Concurrency Theory, Aug 2021, Paris, France. pp.1-33. ⟨hal-03278370⟩