Positive Hennessy-Milner Logic for Branching Bisimulation
Herman Geuvers, Komi Golov
TL;DR
The paper introduces a directed version of the Hennessy–Milner correspondence by shifting to a positive modal logic and its directed variants of bisimulation and apartness. It defines PHML and PHMLU to enable theory inclusion rather than equality, and proves that, for branching bisimulation, Th$_\mathrm{P}(s) \subseteq$ Th$_\mathrm{P}(t)$ iff $s$ is directed branching bisimilar to $t$, with a dual result via directed branching apartness. A key technical achievement is showing that every HMLU formula is equivalent to a Boolean combination of PHMLU formulas, yielding an equivalent but easier-to-reason-about sublogic. The work also provides constructive procedures to translate between directed apartness proofs and distinguishing PHMLU formulas, and situates these results alongside existing notions of directed simulations and branching bisimulation in the literature. Overall, this directed framework tightens the connection between modal theory and process equivalences, and opens avenues for applying these ideas to other bisimulation notions and logics.
Abstract
Labelled transitions systems can be studied in terms of modal logic and in terms of bisimulation. These two notions are connected by Hennessy-Milner theorems, that show that two states are bisimilar precisely when they satisfy the same modal logic formulas. Recently, apartness has been studied as a dual to bisimulation, which also gives rise to a dual version of the Hennessy-Milner theorem: two states are apart precisely when there is a modal formula that distinguishes them. In this paper, we introduce "directed" versions of Hennessy-Milner theorems that characterize when the theory of one state is included in the other. For this we introduce "positive modal logics" that only allow a limited use of negation. Furthermore, we introduce directed notions of bisimulation and apartness, and then show that, for this positive modal logic, the theory of $s$ is included in the theory of $t$ precisely when $s$ is directed bisimilar to $t$. Or, in terms of apartness, we show that $s$ is directed apart from $t$ precisely when the theory of $s$ is not included in the theory of $t$. From the directed version of the Hennessy-Milner theorem, the original result follows. In particular, we study the case of branching bisimulation and Hennessy-Milner Logic with Until (HMLU) as a modal logic. We introduce "directed branching bisimulation" (and directed branching apartness) and "Positive Hennessy-Milner Logic with Until" (PHMLU) and we show the directed version of the Hennessy-Milner theorems. In the process, we show that every HMLU formula is equivalent to a Boolean combination of Positive HMLU formulas, which is a very non-trivial result. This gives rise to a sublogic of HMLU that is equally expressive but easier to reason about.