Verifying Asynchronous Interactions via Communicating Session Automata

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 scalability empirically over large systems (using partial order reduction).