PADEC - Coq Library

Library Padec.BFS.BFS_specification

*Certified Round Complexity of Self-Stabilizing Algorithms*

Global Import

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.

Local Import

From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Graph_Diameter.
From Padec Require Import Tree_topology_ALT.

Open Scope nat_scope.
Open Scope signature.
Set Implicit Arguments.

Specification for a BFS Spanning Tree

Section BFS_Specification.

Assumptions

G = (V, E) connected, rooted (r), semi-anonymous,

Let assume an algorithm

Context {Chans: Channels} {Net: Network} {Algo: Algorithm}.

Notation R_Net := (fun n n' => exists c , is_channel n c n').

Problem Definition

Construct T, which is a spanning tree rooted at r (tree edges in T are oriented toward r, non root process has a unique neighbor in T, and a path in T links any node to r) + BFS (length of a path in T from p to r = distance in G from p to r)

The algorithm should compute a relation Par such that:

  Definition BFS_Spanning_Tree_spec (Root: Node)
             (Par: Env -> relation Node)
             (env: Env) :=
    is_root (Par env) Root /\
    is_spanning_tree (Par env) R_Net Root /\
    is_BFS (Par env) R_Net Root.

Proving specification is to prove that the algorithm is silent, self-stabilizing under the distributed unfair daemon and stabilizes to a configuration which satisfies BFS_Spanning_Tree_spec:

i.e., prove:

self_stabilization unfair_daemon (only_one BFS_Spannig_Tree_spec)

  Instance R_Net_compat: Proper pequiv R_Net.

  Instance BFS_Spanning_Tree_spec_compat:
    Proper pequiv BFS_Spanning_Tree_spec.

  Lemma BFS_Spanning_Tree_spec_dec:
    forall (R_Net_dec: forall p q, {R_Net p q } + {~R_Net p q }),
    forall r par (g: Env),
      Proper pequiv par -> Proper pequiv g ->
      (forall x y, {par g x y } + {~ par g x y }) ->
      {BFS_Spanning_Tree_spec r par g } +
      {~ BFS_Spanning_Tree_spec r par g }.

End BFS_Specification.

Close Scope nat_scope.
Close Scope signature.
Unset Implicit Arguments.