patternMinor
Seemingly non sequitur in proof
Viewed 0 times
sequiturseeminglyproofnon
Problem
I'm trying to understand a small proof in an article about computing lumpability on Markov chains. There is a small detail that I cannot understand, i.e. I don't think it follows from the argument.
The article is Simple $O(m\log{n})$ Time Markov Lumping written by Valmari & Franceschinis.
Given a weighted graph they define the notion of compatible partition of its nodes. Which is a partition $P$ such that for all $B, B' \in P$ and all $s_1, s_2 \in B$ we have that:
$$
W(s_1, B') = W(s_2, B')
$$
They describe an algorithm to compute the coarsest refinement of an initial partition that is compatible (the coarsest croip= compatible refinement of initial partition). The algorithm follows the idea of Paige and Tarjan to compute bisimulation: we take a block $S$ from the partition as a splitter and check whether some other block $B$ breaks the condition above, and if it does we split $B$ into $B_1, \ldots, B_k$ such that the $B_i$ satisfy the condition above when taking $B' = S$.
How exactly these checks are performed shouldn't be essential for the correctness of the algorithm. In the proof of correctness they prove the following lemma:
Lemma 2. Let $d_1, d_2$ be nodes of the graph. If the algorithm ever puts $d_1$ and $d_2$ into different blocks, then there is no
croip where $d_1$ and $d_2$ are in the same block.
The proof for when the algorithm separates $d_1$ and $d_2$ during its execution is the following:
Proof. We show that it is an invariant property of the main loop of the algorithm (that is, always valid on line 2*) that if
two states are in different blocks of the algorithm, then they are in
different blocks in every croip.
If $d_1$ and $d_2$ are in different blocks initially, then they are in
different blocks in $I$ and thus in every croip.
The case remains where lines 14 to 20 separate $d_1$ and $d_2$ to
different blocks.
This happens only if $W(d_1, S) \neq W(d_2, S)$. Let $P$
be an arbitrary croip. It follows from
The article is Simple $O(m\log{n})$ Time Markov Lumping written by Valmari & Franceschinis.
Given a weighted graph they define the notion of compatible partition of its nodes. Which is a partition $P$ such that for all $B, B' \in P$ and all $s_1, s_2 \in B$ we have that:
$$
W(s_1, B') = W(s_2, B')
$$
They describe an algorithm to compute the coarsest refinement of an initial partition that is compatible (the coarsest croip= compatible refinement of initial partition). The algorithm follows the idea of Paige and Tarjan to compute bisimulation: we take a block $S$ from the partition as a splitter and check whether some other block $B$ breaks the condition above, and if it does we split $B$ into $B_1, \ldots, B_k$ such that the $B_i$ satisfy the condition above when taking $B' = S$.
How exactly these checks are performed shouldn't be essential for the correctness of the algorithm. In the proof of correctness they prove the following lemma:
Lemma 2. Let $d_1, d_2$ be nodes of the graph. If the algorithm ever puts $d_1$ and $d_2$ into different blocks, then there is no
croip where $d_1$ and $d_2$ are in the same block.
The proof for when the algorithm separates $d_1$ and $d_2$ during its execution is the following:
Proof. We show that it is an invariant property of the main loop of the algorithm (that is, always valid on line 2*) that if
two states are in different blocks of the algorithm, then they are in
different blocks in every croip.
If $d_1$ and $d_2$ are in different blocks initially, then they are in
different blocks in $I$ and thus in every croip.
The case remains where lines 14 to 20 separate $d_1$ and $d_2$ to
different blocks.
This happens only if $W(d_1, S) \neq W(d_2, S)$. Let $P$
be an arbitrary croip. It follows from
Solution
The invariant states that if at some point of the algorithm, $d_1,d_2$ are in different blocks, then in every croip, $d_1,d_2$ are in different blocks. The contrapositive of the invariant states that if $d_1,d_2$ are in the same block of some croip, then they are always in the same block during the running of the algorithm.
Now consider a block $S$ of your algorithm and a block $T$ of an arbitrary croip. We want to show that either $T \subseteq S$ or $T \cap S = \emptyset$. If not, then take some $d_1 \in T \setminus S$ and some $d_2 \in T \cap S$. Since $d_1,d_2 \in T$, they are in the same block of some croip, and so the contrapositive of the invariant states that they are always in the same block during the running of the algorithm. But $d_1 \notin S$ while $d_2 \in S$, and we reach a contradiction. We conclude that either $T \subseteq S$ or $T \cap S = \emptyset$.
Now consider a block $S$ of your algorithm and a block $T$ of an arbitrary croip. We want to show that either $T \subseteq S$ or $T \cap S = \emptyset$. If not, then take some $d_1 \in T \setminus S$ and some $d_2 \in T \cap S$. Since $d_1,d_2 \in T$, they are in the same block of some croip, and so the contrapositive of the invariant states that they are always in the same block during the running of the algorithm. But $d_1 \notin S$ while $d_2 \in S$, and we reach a contradiction. We conclude that either $T \subseteq S$ or $T \cap S = \emptyset$.
Context
StackExchange Computer Science Q#42352, answer score: 2
Revisions (0)
No revisions yet.