3
$\begingroup$

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 invariant that each block of $P$ is either disjoint with $S$ or a subset of $S$, because otherwise the algorithm would have separated two states that belong to the same block of a croip. Therefore, there are blocks $S_1 , \ldots, S_k$ in $P$ such that $S_1 \cup \cdots \cup S_k = S$. The fact $W(d_1, S) \neq W(d_2, S)$ implies that there is $1 \leq i \leq k$ such that $W(d_1 , S_i) \neq W(d_2, S_i )$. So $d_1$ and $d_2$ belong to different blocks in $P$.

I have a problem understanding the text in bold. To me: it's simply false. They justify it saying otherwise the algorithm would have separated two states that belong to the same block of a croip.

However:

  • we still haven't proved the algorithm correct, so I don't really see how the algorithm doing something should imply anything at this point
  • I don't get if the two states separated are $d_1$ and $d_2$ or if they are referencing other states

So, I see this as a non sequitur, which would invalidate the proof of this lemma and thus the whole correctness proof of the algorithm.

Given that the algorithm was developed to fix a wrong algorithm published previously from other authors, I believe Valmari and Franceschinis were very careful in the proofs, so I'm probably missing something trivial. Can anybody point out what I'm missing?


* The algorithm is simply a main loop that chooses a new splitter $S$ for each iteration and splits all the blocks in the partition and goes on.

$\endgroup$
2
$\begingroup$

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

$\endgroup$
  • $\begingroup$ I don't really see the contradiction. Given that we still haven't proved the invariant, I believe the conclusion should be: "But $d_1 \notin S$ while $d_2 \in S$ and hence the invariant doesn't hold", not "we have a contradiction and hence it holds". You cannot use the statement of the theorem you are trying to prove to create a contradiction. Could you clarify exactly what is in contradiction with which hypothesis? $\endgroup$ – Bakuriu May 10 '15 at 6:02
  • $\begingroup$ The only way in which I could make sense of that contradiction is if we were proving the invariant by induction and the contradiction could be about the inductive hypothesis. But to me the proof is not by induction and since the invariant is about all iterations of the algorithm it would have to be changed in order to prove it by induction on the number of iterations. After that, the reasoning may hold. $\endgroup$ – Bakuriu May 10 '15 at 6:39
  • $\begingroup$ I'm not sure you understand what an invariant is. An invariant is something that always holds. When you prove that an invariant holds, you always prove it by induction. Now I suggest you take a few days thinking about it, and only if you still don't understand, come back here. $\endgroup$ – Yuval Filmus May 10 '15 at 12:56
  • $\begingroup$ Yes I understand that. Simply I'm not used to proving something by induction without mentioning the base case nor when we apply the inductive hypothesis. It's just confusing. Instead of using that ambiguous sentence they should have simply said "otherwise we obtain a contradiction with the inductive hypothesis" and it would have been clear what they were saying. $\endgroup$ – Bakuriu May 10 '15 at 18:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.