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 alphabet size, 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 specification checking problem that captures many classical decision problems such as prediction, nilpotency, predecessor, asynchronous reachability. Then, we present a fast-parallel algorithm that solves the general problem when the three parameters are bounded, hence showing that the problem is in NC. Finally, we show that these problems are hard from two different perspectives. First, the general problem is W[2]-hard when taking either treewidth or alphabet as single parameter and fixing the others. Second, the classical problems are hard in their respective classes when restricted to families of graphs with sufficiently large treewidth.