Generalizing LCL Complexity Gaps to Unbounded Degree via Monadic Second-Order Properties

Abstract

The last decade of research on the LOCAL model has seen tremendous progress in understanding locally checkable labeling (LCL) problems, culminating in an almost complete classification of the possible complexities LCL problems can exhibit. In particular, on undirected trees, Chang and Pettie showed that there is no LCL problem with complexity between ω(log n) and n^o(1) [Yi-Jun Chang and Seth Pettie, 2017] and Chang showed that, for every positive integer k, there is no LCL problem with complexity between ω(n^{1/(k+1)}) and o(n^{1/k}) [Yi-Jun Chang, 2020]; additionally, which side of each gap a problem is found on is decidable.
While the class of LCL problems - which, roughly speaking, consists of problems for which the correctness of a solution can be described by a finite set of allowed node configurations, which in turn can be locally verified by a constant-time algorithm - includes many important problems, it has one major restriction: problems can be defined only on bounded degree graphs, which consequently restricts all the classification and gap results mentioned above.
In this work, we propose a generalization of LCL problems to unbounded degree using Presburger monadic second-order (PMSO) formulas; more specifically, we consider what we call Local PMSO (LPMSO) problems, i.e., problems whose correct solutions are both finitely described by a PMSO formula and locally verifiable by a LOCAL algorithm in constant time - this class contains many of the important problems studied in the LOCAL model but defines them on unbounded degree graphs. As our main result we prove that, on unbounded degree rooted trees, the aforementioned ω(log n)-n^{o(1)} and ω(n^{1/(k+1)})-o(n^{1/k}) complexity gaps (and their decidability) extend to the class of LPMSO problems.
We obtain our gap results by proving two theorems that may be of independent interest:  
1) We show that computing just a solution of an LPMSO problem is asymptotically as hard as computing both a solution and a certificate for its correctness, if the certification is based on the minimal automaton verifying the PMSO formula. 
2) By modifying the minimal verification automaton slightly, we create a so-called rational multiset tree automaton whose run on the input rooted tree encodes both a solution and a certificate for its correctness; then we show that computing a run of any rational multiset tree automaton on a rooted tree is asymptotically equivalent to solving the same problem on a rooted tree whose degree is bound by a constant depending only on the problem description.