Equilibrium and Termination
Vincent Danos

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.