Hennessy-Milner Theorems for Topological Semantics of Modal Logic

Abstract

Bisimulation is the basic equivalence between models in modal logic. Although bisimulation implies modal equivalence, the converse does not hold in general. Hennessy–Milner-style theorems find various conditions under which the converse holds, e.g. finiteness. In Kripke semantics, the condition of finiteness can be improved to image-finiteness, i.e., a model may be infinite, but without infinite branching. The present paper proposes local finiteness as an analogue of this property for topological semantics, proves appropriate Hennessy–Milner theorem analogues, and shows how locally finite topologies, in fact, directly correspond to image-finite Kripke models.