Parameterized Verification of Communicating Automata under Context Bounds

Overview & Synopsis

We study the verification problem for parameterized communicating automata (PCA), in which processes synchronize via message passing. A given PCA can be run on any topology of bounded degree (such as pipelines, rings, or ranked trees), and communication may take place between any two processes that are adjacent in the topology. Parameterized verification asks if there is a topology from a given topology class that allows for an accepting run of the given PCA. In general, this problem is undecidable even for synchronous communication and simple pipeline topologies. We therefore consider context-bounded verification, which restricts the behavior of each single process. For several variants of context bounds, we show that parameterized verification over pipelines, rings, and ranked trees is decidable. Our approach is automata-theoretic and uniform. We introduce a notion of graph acceptor that identifies those topologies allowing for an accepting run. Depending on the given topology class, the topology acceptor can then be restricted, or adjusted, so that the verification problem reduces to checking emptiness of finite automata or tree automata.