On the parameterized complexity of freezing dynamics

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 decision problem, called 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 model checking problem when the three parameters are bounded, hence showing that the problem is in NC. Moreover, we show that the problem is in XP on the parameters tree-width and maximum degree. 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 graph with sufficiently large treewidth.