Fall 2016

Logical Structures in Computation Seminar

Oct 19, 2016 4:00 pm – 5:00 pm 

Add to Calendar


Calvin Lab Rm 116

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.