# Verifying Asynchronous Interactions via Communicating Session Automata

arXiv: https://arxiv.org/abs/1901.09606 · HTML: https://mlsanity.com/paper/1901.09606/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Jan 2019.

## Built on by (most cited first, 1 of 1)

- [A partial order view of message-passing communication models](https://mlsanity.com/paper/2210.13062/) (2022)

## Abstract (arXiv)

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.