Vincent Danos
(University of Edinburgh)
Equilibrium and Termination

We present a reduction of the Post correspondence problem to the question of whether a continuous-time Markov chain has an equilibrium. It follows that whether a computable CTMC is dissipative (ie does not have an equilibrium) is undecidable, and more generally equilibrium can be seen as a form of sequential termination. We generalize this idea to a class of reversible communicating processes. Transition rates are derived from a formal notion of energy which increases exponentially with the size of the local history of a process. This second construction can be seen as a concurrent version of the Metropolis-Hastings algorithm.