PADEC - Coq Library

Library Padec.KDomSet.KDomSet_termination

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 Graph_Diameter.
From Padec Require Import Tree_topology_ALT.
From Padec Require Import KDomSet_specification.
From Padec Require Import KDomSet_alpha.
From Padec Require Import KDomSet_common.

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}
          {KDP: KDomSet_parameters}
          {Graph_assumption: KDomSet_Assume}
          {Graph_network_assumption: Graph_Network_matching}.
  Let k_pos := k_pos.
  Existing Instance T_compat.
  Notation newAlpha alpha n := (NewAlpha k (lcA alpha n)).

  Section Potential_Definition.

Potential of a node:

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

Note that this definition requires that the spanning tree exists. This is the reason why termination cannot be shown without the assumption on safe configurations.

depth in the tree

Tools for depth

depth: Node -> nat (distance to Root)

    Definition compute_depth p: { d | is_dist (flip T) p Root d }.

    Definition depth: Node -> nat :=
      fun p => proj1_sig (compute_depth p).

    Lemma depth_is_dist: forall p, is_dist (flip T) p Root (depth p).

    Lemma depth_is_dist': forall p d,
        depth p = d <-> is_dist (flip T) p Root d.

    Lemma depth_Root: depth Root = 0%nat.

    Lemma depth_Root': forall p, depth p = 0%nat <-> p == Root.

    Global Instance depth_compat: Proper pequiv depth.

Potential of a node: 0 if not enabled, else depth

    Definition potential (alpha: Node -> Z) (n: Node): nat :=
      if Z.eq_dec (alpha n) (newAlpha alpha n) then 0%nat
      else S (depth n).

    Instance potential_compat: Proper fequiv potential.

  End Potential_Definition.

  Section Potential_Properties.

Any node which is down-linked to another has smaller depth than the first one.

    Lemma deeper_depth_step:
      forall (n: Node) (child: Node),
        T n child -> S (depth n) = depth child.

    Lemma deeper_depth:
      forall (p: list Node) (n: Node) (d: Node),
        is_path (flip T) d p n -> (depth n < depth d)%nat.

  End Potential_Properties.

Results for one step of execution

  Section With_Step.

    Variable (root: Node).

    Variable (alpha: Node -> Z) (alpha': Node -> Z).
    Variable (alpha_compat: Proper fequiv alpha)
             (alpha'_compat: Proper fequiv alpha')
             (step_ok: forall n, alpha' n = newAlpha alpha n \/
                                 alpha' n = alpha n)
             (progress: exists n , alpha n <> alpha' n).

New Children alphas only depends on children moves

    Lemma ChildrenAlphas_only_depends_on_children:
      forall (n: Node),
        (forall (child: Node), T n child -> alpha child = alpha' child )
        -> lcA alpha n == lcA alpha' n.

New Alphas only depends on children moves

    Lemma NewAlpha_only_depends_on_children:
      forall (n: Node),
        (forall (child: Node),
            T n child -> alpha child = alpha' child ) ->
        newAlpha alpha n = newAlpha alpha' n.

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

    Lemma enabled_child_has_moved:
      forall (n: Node) (H: ~ enabled_alpha alpha n)
             (H': enabled_alpha alpha' n),
      exists (child: Node ), T n child /\ alpha child <> alpha' 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, alpha n <> alpha' n
                -> (forall child, T n child -> alpha child = alpha' child )
                -> ~ enabled_alpha alpha' n.

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: Node),
        alpha n <> alpha' n -> enabled_alpha alpha' n ->
        exists (child: Node ), T n child /\ alpha child <> alpha' 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),
        alpha n <> alpha' n ->
        exists (descendant: Node ),
          (n == descendant \/ exists p , is_path (flip T) descendant p n ) /\
          (enabled_alpha alpha descendant ) /\
          ~ (enabled_alpha alpha' descendant ).

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_alpha alpha n -> enabled_alpha alpha' n ->
        exists (descendant: Node ),
          (exists p , is_path (flip T) descendant p n ) /\
          enabled_alpha alpha descendant /\ ~enabled_alpha alpha' descendant.

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_alpha alpha n
                        /\ ~ enabled_alpha alpha' n.

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 alpha' n <> potential alpha n
                    <->
                    (~enabled_alpha alpha n <-> enabled_alpha alpha' n ).

Local Criterion

        Lemma kHopDom_local_criterion:
          forall (n: Node),
            (potential alpha' n > potential alpha n)%nat
            -> exists (n': Node ),
              potential alpha n' <> potential alpha' n'
              /\ (potential alpha n' > potential alpha' n)%nat.

Global Criterion

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

      End Potential_termination_criteria.
  End With_Step.

End KDomSet_Termination.

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