Coq Library
Tools

#### Global Imports

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

#### Local Imports

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

# Termination for K-Dominating Set Algorithm

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)).

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).

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.
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.
When a node actually moved, it is down-linked (in the spanning tree) to a node which was enabled and became disabled.
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.

### 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

### 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)

Local Criterion

## 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.