text: Verifying that a network configuration satisfies a given boolean predicate is a fundamental problem in distributed computing. Many variations of this problem have been studied, for example, in the context of proof labeling schemes (PLS), locally checkable proofs (LCP), and non-deterministic local decision (NLD). In all of these contexts, verification time is assumed to be constant. Korman, Kutten and Masuzawa [PODC 2011] presented a proof-labeling scheme for MST, with poly-logarithmic verification time, and logarithmic memory at each vertex. In this paper we introduce the notion of a @math -PLS, which allows the verification procedure to run for super-constant time. Our work analyzes the tradeoffs of @math -PLS between time, label size, message length, and computation space. We construct a universal @math -PLS and prove that it uses the same amount of total communication as a known one-round universal PLS, and @math factor smaller labels. In addition, we provide a general technique to prove lower bounds for space-time tradeoffs of @math -PLS. We use this technique to show an optimal tradeoff for testing that a network is acyclic (cycle free). Our optimal @math -PLS for acyclicity uses label size and computation space @math . We further describe a recursive @math space verifier for acyclicity which does not assume previous knowledge of the run-time @math .
  @cite_15: A central theme in distributed network algorithms concerns understanding and coping with the issue of locality. Yet despite considerable progress, research efforts in this direction have not yet resulted in a solid basis in the form of a fundamental computational complexity theory for locality. Inspired by sequential complexity theory, we focus on a complexity theory for distributed decision problems. In the context of locality, solving a decision problem requires the processors to independently inspect their local neighborhoods and then collectively decide whether a given global input instance belongs to some specified language. We consider the standard LOCAL model of computation and define LD(t) (for local decision) as the class of decision problems that can be solved in t communication rounds. We first study the intriguing question of whether randomization helps in local distributed computing, and to what extent. Specifically, we define the corresponding randomized class BPLD(t,p,q), containing all languages for which there exists a randomized algorithm that runs in t rounds, accepts correct instances with probability at least p, and rejects incorrect ones with probability at least q. We show that p2 p q = 1 is a threshold for the containment of LD(t) in BPLD(t,p,q). More precisely, we show that there exists a language that does not belong to LD(t) for any t=o(n) but does belong to BPLD(0,p,q) for any p,q ∈ (0,1) such that p2 p q ≤ 1. On the other hand, we show that, restricted to hereditary languages, BPLD(t,p,q)=LD(O(t)), for any function t, and any p, q ∈ (0,1) such that p2 p q > 1. In addition, we investigate the impact of nondeterminism on local decision, and establish several structural results inspired by classical computational complexity theory. Specifically, we show that nondeterminism does help, but that this help is limited, as there exist languages that cannot be decided locally nondeterministically. Perhaps surprisingly, it turns out that it is the combination of randomization with nondeterminism that enables to decide all languages in constant time. Finally, we introduce the notion of local reduction, and establish a couple of completeness results.
summary: The question of what properties can be verified using a constant verification time was studied in @cite_15 , and several complexity classes were presented, including LD---local decision---which includes all properties that can be decided using constant number of rounds and no additional information, and NLD---non-deterministic local decision---which includes all properties that can be decided in a constant number of rounds with additional information in the form of a certificate given to each vertex. While NLD and PLS are closely related, they differ in that NLD certificates are independent of vertex identifiers. Since PLS labels may depend on vertex identifiers, there is a PLS for every sequentially decidable property on ID based networks, while not all sequentially decidable properties are in NLD. Our lower bounds in Subsections and allow labels to depend on unique vertex identifiers, so our arguments give identical lower bounds for certificate sizes in the weaker NLD model. Nonetheless, the schemes for @math in Subsections and do not require unique identifiers.