Verifying Asynchronous Interactions via Communicating Session Automata

TL;DR

This paper introduces a new asynchronous compatibility property for communicating session automata, enabling effective verification of multiparty interactions with bounded message exchanges, and demonstrates its practical efficiency.

Contribution

It proposes k-multiparty compatibility, decomposes it into k-safety and k-exhaustivity, and provides a PSPACE-complete checking procedure with empirical evaluation.

Findings

k-MC is a strict superset of synchronous compatibility.

Checking k-MC is PSPACE-complete.

Empirical results show scalability over large systems.

Abstract

This paper proposes a sound procedure to verify properties of communicating session automata (CSA), i.e., communicating automata that include multiparty session types. We introduce a new asynchronous compatibility property for CSA, called k-multiparty compatibility (k-MC), which is a strict superset of the synchronous multiparty compatibility used in theories and tools based on session types. It is decomposed into two bounded properties: (i) a condition called k-safety which guarantees that, within the bound, all sent messages can be received and each automaton can make a move; and (ii) a condition called k-exhaustivity which guarantees that all k-reachable send actions can be fired within the bound. We show that k-exhaustivity implies existential boundedness, and soundly and completely characterises systems where each automaton behaves equivalently under bounds greater than or equal to k. We show that checking k-MC is PSPACE-complete, and demonstrate its performance empirically over large systems using partial order reduction.