Events
Fall 2016

Logical Structures in Computation Seminar

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

Add to Calendar

Location: 

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.