Title: Verifying Asynchronous Interactions via Communicating Session Automata,
Abstract: The relationship between communicating automata and session types is the
cornerstone of many diverse theories and tools, including type checking, code
generation, and runtime verification. A serious limitation of session types is
that, while endpoint programs interact asynchronously, the underlying property
which guarantees safety of session types is too synchronous: it requires a
one-to-one synchronisation between send and receive actions. This paper
proposes a sound procedure to verify properties of communicating session
automata (CSA), i.e., communicating automata that correspond to 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 proposed in the literature. 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-exhaustive systems soundly and completely characterise systems
where each automaton behaves uniformly for any bound greater or equal to k. We
show that checking k-MC is PSPACE-complete, but can be done efficiently over
large systems by using partial order reduction techniques. We demonstrate that
several examples from the literature are k-MC, but not synchronous compatible.