Contributo in atti di convegno, 2023, ENG, 10.1007/978-3-031-27481-7_9

Can we communicate? Using dynamic logic to verify team automata

ter Beek M.H.; Cledou G.; Hennicker R.; Proença J.

CNR-ISTI, Pisa, Italy; INESC TEC and University of Minho, Braga, Portugal; Ludwig-Maximilians-Universität Muenchen, Munich, Germany; Polytechnic Institute of Porto, Porto, Portugal

Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receivesmust be satisfied). Previouswork focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.

FM'23 - 25th International Symposium on Formal Methods, pp. 122–141, Lübeck, Germany, 6-10/3/2023

Keywords

Team automata, Synchronisation policies, Dynamic logic, Verification

CNR authors

Ter Beek Maurice Henri

CNR institutes

ISTI – Istituto di scienza e tecnologie dell'informazione "Alessandro Faedo"

ID: 478830

Year: 2023

Type: Contributo in atti di convegno

Creation: 2023-03-08 10:36:26.000

Last update: 2023-06-16 15:02:31.000

External IDs

CNR OAI-PMH: oai:it.cnr:prodotti:478830

DOI: 10.1007/978-3-031-27481-7_9

Scopus: 2-s2.0-85151057753

ISI Web of Science (WOS): 000999132100009