Couplings and Probabilistic Bisimilarity

As shown by Jonsson and Larsen in 1991, probabilistic bisimilarity can be characterized in the terms of the existence of a coupling.  These couplings form a convex polytope. I will show that their result can be slightly sharpened by requiring the coupling to be a vertex of the polytope. The existence of such a vertex can be proved by means of a minor variation on Hitchcock's North West method which was proposed in 1941. Showing that this method proves the result amounts to proving a number of loop invariants. I am currently formalizing these loop invariants and proving them in the program verifier Dafny and will discuss my limited experience with this tool in this setting.