Some IC3 people at Cornell have been looking at this in the context of smart contracts: http://www.initc3.org/files/Gyges.pdf