Local Checkability in Dynamic Networks

In this work we study local checkability of network properties considering inconsistency throughout the verification process. We use disappearing and appearing edges to model inconsistency and prover-verifier-pairs (PVPs) for verification. We say that a network property N is locally checkable under inconsistency if there exists a PVP for a specified inconsistency. In such a PVP, a prover P assigns a label to each vertex of an initial graph Gi. A distributed time constant verifier V computes Yes on every vertex of the altered graph Ga, if Ga has the property N and was labeled by P, and No on at least one vertex of Ga if Ga does not fulfill N.

For s-t-reachability, we present an optimal 2-bit-label PVP considering one disappearing edge and an upper bound of O(log n) bits as label size for one appearing edge. For cyclicity, we prove that no general PVP can be found considering disappearing edges, as well as an upper bound of O(n2 log n) bits as the label size for one appearing edge. Furthermore, we show that no PVP can be found for s-t-reachability nor general cyclicity that can consider multiple inconsistencies.