PADEC - Coq Library

Library Padec.KDomSet.KDomSet_termination_tree_topology

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

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

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import FoldRight.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Self_Stabilization.
From Padec Require Import P_Q_Termination.
From Padec Require Import Tree_topology.
From Padec Require Import KDomSet_algo_tree_topology.

Open Scope Z_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Termination for K-Dominating Set Algorithm

Roadmap

1) Define Potential of a node: 0 if not enabled, else tree depth signature: node->env -> nat

NB: depth for root == 1

2) Proof: if a node becomes enabled, one of its child has moved

3) Proof (down path induction + 2)): if a node becomes enabled, one of its descendant has become disabled

assumption: downpaths are finite (to be proved elsewhere)

4) Proof: there is always a node whose activation has changed (potential of this node passed from >0 to 0) (induction on down path)

5) Using 3) and multiset theorem (P_Q_Termination.v) concludes that the algorithm terminates

=> Use results from P_Q_Termination

proof of local criterion: see 3)
proof of global criterion: see 4)

Section KDomSet_Termination.

Channel and Network definitions

  Context {Chans: Channels}
          {Net: Network}
          {DTN: Down_Tree_Network Net}
          {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

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

  Notation Algo := KDom_algo.
  Notation Env := (Env (Net := Net) (Algo := KDom_algo)).

  Existing Instance KDom_Stable.
  Existing Instance KDom_RO_assumption.

  Notation alphas_ :=
    (fun (env: Env) n => alphas (children_states (env n) (local_env env n))).

  Notation new_alpha_ := (fun env n => new_alpha (alphas_ env n)).

  Section Potential_Definition.

Potential of a node:

0 if not enabled, else depth of the node in the spanning tree.

    Definition potential (env: Env) (n: Node): nat :=
      if enabled_b env n then 1 + Depth n else 0.

    Instance potential_compat: Proper pequiv potential.

  End Potential_Definition.

Results for one step of execution

  Section With_Step.

    Variable (env env': Env)
             (step: Step env' env)
             (hassume: Assume env).

Read Only are constant values

    Lemma children_c_same:
      forall n, equivlistA equiv (children_c (env n))
                           (children_c (env' n)).

    Lemma is_root_same:
      forall n, is_root (env n) == is_root (env' n).

    Lemma alpha_same:
      forall n, env n == env' n <-> alpha (env n) = alpha (env' n).

    Lemma alpha_change:
      forall n, ~ env n == env' n <-> alpha (env n) <> alpha (env' n).

New alphas only depends on children moves

    Lemma alphas_only_depends_on_children:
        forall (n: Node),
          (forall (child: Node), isParent n child -> env child = env' child )
          -> equivlistA equiv (alphas_ env n) (alphas_ env' n).

New alpha only depends on children moves

      Lemma new_alpha_only_depends_on_children:
        forall (n: Node),
          (forall (child: Node), isParent n child -> env child = env' child )
          -> new_alpha_ env n = new_alpha_ env' n.

When a node that was disabled becomes enabled, one of its child has actually moved.

      Lemma enabled_child_has_moved:
        forall (n: Node),
          enabled_b env n = false -> enabled_b env' n = true ->
          exists (child: Node ),
            isParent n child /\ ~ env child == env' child.

When a node has actually moved while none of its children moved, it is no more enabled at next configuration.

      Lemma node_has_moved_but_no_child:
        forall n, ~ env n == env' n ->
                  (forall child, isParent n child ->
                                 env child = env' child ) ->
                  enabled_b env' n = false.

When a node has moved, but is still enabled at next configuration, it has a child that actually also moved.

      Lemma node_has_moved:
        forall n,
          ~ env n == env' n -> enabled_b env' n = true ->
          exists child ,
            isParent n child /\ ~ env child == env' child.

When a node actually moved, it is down-linked (in the spanning tree) to a node which was enabled and became disabled.

      Lemma moving_node_has_disabled_desc:
        forall (n: Node),
          ~ env n == env' n ->
          exists (descendant: Node ),
            isAncestor n descendant /\
            enabled_b env descendant = true /\
            enabled_b env' descendant = false.

When a node that was disabled becomes enabled at next configuration, it is down-linked (in the spanning tree) to a node which was enabled and becomes disabled.

      Lemma new_enabled_node_has_disabled_descendant:
        forall (n: Node),
          enabled_b env n = false -> enabled_b env' n = true ->
          exists (descendant: Node ),
            isAncestor n descendant /\
            enabled_b env descendant = true /\
            enabled_b env' descendant = false.

4) Proof:

there is always a node that becomes disabled after a step (potential of this node passed from >0 to 0) (induction on down path)

Within a valid step, there exists a node that was enabled but becomes disabled

Lemma one_disabled:
exists (n: Node ), enabled_b env n = true /\ enabled_b env' n = false.

5) Using 3) and multiset theorem (Termination.v, Wf_Algo_Multiset) conclude that the

algorithm terminates

proof of local criterion: see 3)
proof of global criterion: see 4)

Termination Criteria

      Section Potential_termination_criteria.

        Lemma diff_pot:
          forall n, potential env' n <> potential env n
                    <->
                    (enabled_b env n = false <-> enabled_b env' n = true ).

Local Criterion

        Lemma kHopDom_local_criterion:
          forall (n: Node),
            gt (potential env' n) (potential env n)
            -> exists (n': Node ),
                 potential env n' <> potential env' n'
                 /\
                 gt (potential env n') (potential env' n).

Global Criterion

        Lemma kHopDom_global_criterion:
          exists n , potential env' n <> potential env n.

      End Potential_termination_criteria.

  End With_Step.

  Section Termination.

    Lemma kDOM_termination: termination KDom_RO_assumption.

  End Termination.

End KDomSet_Termination.

Close Scope signature_scope.
Close Scope Z_scope.
Unset Implicit Arguments.