Verifying asynchronous interactions via communicating session automata

DOI10.1007/978-3-030-25540-4_6arXiv1901.09606OpenAlexW2965154247MaRDI QIDQ6154577FDOQ6154577

Publication date: 16 February 2024

Published in: Computer Aided Verification (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1901.09606

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (5)

This page was built for publication: Verifying asynchronous interactions via communicating session automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6154577)