On the impact of treewidth in the computational complexity of freezing dynamics

TL;DR

This paper explores how the treewidth and degree of a network's graph influence the computational complexity of problems related to freezing automata networks, providing both efficient algorithms and hardness results.

Contribution

It introduces a formal model checking framework for freezing automata networks and analyzes the complexity based on graph parameters, offering new algorithms and hardness proofs.

Findings

Efficient parallel algorithm for bounded treewidth and degree graphs.

Hardness results for polynomially growing treewidth graphs.

Complexity depends critically on treewidth and maximum degree.

Abstract

An automata network is a network of entities, each holding a state from a finite set and evolving according to a local update rule which depends only on its neighbors in the network's graph. It is freezing if there is an order on states such that the state evolution of any node is non-decreasing in any orbit. They are commonly used to model epidemic propagation, diffusion phenomena like bootstrap percolation or cristal growth. In this paper we establish how treewidth and maximum degree of the underlying graph are key parameters which influence the overall computational complexity of finite freezing automata networks. First, we define a general model checking formalism that captures many classical decision problems: prediction, nilpotency, predecessor, asynchronous reachability. Then, on one hand, we present an efficient parallel algorithm that solves the general model checking problem in NC for any graph with bounded degree and bounded treewidth. On the other hand, we show that these problems are hard in their respective classes when restricted to families of graph with polynomially growing treewidth. For prediction, predecessor and asynchronous reachability, we establish the hardness result with a fixed set-defiend update rule that is universally hard on any input graph of such families.