Modular Analysis of Tree-Topology Models
Logic in Computer Science
2020-12-10 v1
Abstract
We investigate networks of automata that synchronise over common action labels. A graph synchronisation topology between the automata is defined in such a way that two automata are connected iff they can synchronise over an action. We show a very effective reduction of networks of automata with tree-like synchronisation topologies. The reduction preserves a certain form of reachability, but not safety. The procedure is implemented in an open-source tool.
Cite
@article{arxiv.2012.04739,
title = {Modular Analysis of Tree-Topology Models},
author = {Laure Petrucci and Michał Knapik},
journal= {arXiv preprint arXiv:2012.04739},
year = {2020}
}