Can We Communicate? Using Dynamic Logic to Verify Team Automata

Beek, Maurice H. ter ; Cledou, Guillermina ; Hennicker, Rolf und Proença, José (2023): Can We Communicate? Using Dynamic Logic to Verify Team Automata. 25th International Symposium on Formal Methods (FM), Lubeck, Germany, 06. - 10. März 2023. Chechik, Marsha; Katoen, Joost-Pieter und Leucker, Martin (Hrsg.): In: Formal Methods, Lecture Notes in Computer Science Bd. 14000 Cham: Springer. S. 122-141

Abstract

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 receives must be satisfied). Previous work 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.

• Dokumententyp: Konferenzbeitrag (Paper)
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISBN: 978-3-031-27480-0 ; 978-3-031-27481-7
• ISSN: 0302-9743
• Ort: Cham
• Sprache: Englisch