Document - Can we communicate? Using dynamic logic to verify team automata

2023

Conference article Open Access

Can we communicate? Using dynamic logic to verify team automata

Ter Beek M. H., Cledou G., Hennicker R., Proença J.

Team automata Synchronisation policies Dynamic logic Verification

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.

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

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:478830,
	title = {Can we communicate? Using dynamic logic to verify team automata},
	author = {Ter Beek M. H. and Cledou G. and Hennicker R. and Proença J.},
	doi = {10.1007/978-3-031-27481-7_9},
	booktitle = {FM'23 - 25th International Symposium on Formal Methods, pp. 122–141, Lübeck, Germany, 6-10/3/2023},
	year = {2023}
}