PADEC - Coq Library

Library Padec.KDomSet.KDomSet_specification_tree_topology

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Import

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

Local Import

From Padec Require Import SetoidUtil.
From Padec Require Import RelationA.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Tree_topology.

Open Scope Z_scope.
Set Implicit Arguments.

Specification for a k-hop-dominating set algorithm

Section KDomSet_Specification.

Problem Definition

Let assume an algorithm and a positive number k

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

Assume the network endows a down spanning tree

  Context {DTN: Down_Tree_Network Net}.
  Notation Tree := (@DTN_topo _ _ DTN).
  Context {SPAN: is_spanning _ Tree}.

The parameter K itself (from K-Dominating-Set)

Context {k: Z}.

Some configuration of the system (made of the network and the algorithm) contains a k-hop-dominating set

if one can express a predicate on nodes: kDominator which identifies nodes to be in some k-hop-dominating set.

Precisely, for every node, it should be linked to a node in the k-hop-dominating set thanks to a path whose length is smaller than k.

Predicates which holds when the node is identified as in the k-hop-dominating set in the current configuration.

  Variable (kDominator: Env -> Node -> Prop).

  Definition is_neighbor_of (x y: Node): Prop :=
    exists (c: Channel ), peer x c == Some y \/ peer y c == Some x.
  Definition is_path := chain is_neighbor_of.

    Definition kDOM (env: Env): Prop :=
      forall (n: Node),
      exists (d: Node ), kDominator env d /\
                        exists path , (is_path d path n ) /\
                                     (Z_of_nat (length path) <= k)%Z.
End KDomSet_Specification.

Close Scope Z_scope.
Unset Implicit Arguments.