Skip to main content

Verifying Asynchronous Interactions via Communicating Session Automata

Lange, Julien, Yoshida, Nobuko (2019) Verifying Asynchronous Interactions via Communicating Session Automata. In: 31st International Conference on Computer-Aided Verification (CAV 2019). . Springer

PDF - Supplemental Material
Download (863kB) Preview
PDF - Author's Accepted Manuscript
Download (797kB) Preview
Official URL


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.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: verification, message passing concurrency, asynchrony, communicating automata, session types
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing
Depositing User: Julien Lange
Date Deposited: 21 May 2019 11:01 UTC
Last Modified: 23 Jul 2019 09:41 UTC
Resource URI: (The current URI for this page, for reference purposes)
Lange, Julien:
  • Depositors only (login required):


Downloads per month over past year