Modular Analysis of Tree-Topology Models

TL;DR

This paper introduces a method for simplifying networks of automata with tree-structured synchronization topologies, preserving reachability properties and implemented in an open-source tool.

Contribution

It presents a novel reduction technique for automata networks with tree-like synchronization that maintains reachability, enhancing analysis efficiency.

Findings

Effective reduction of tree-topology automata networks

Preserves reachability but not safety properties

Implemented in an open-source tool

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.