
2 H. GEUVERS AND K. GOLOV
the notion of branching bisimulation has been developed, which ignores the silent steps while
taking into account their branching behavior. Branching bisimulation has been studied a lot
as it is the finest equivalence in the well-known “van Glabbeek spectrum” [
vG93
]. Various
algorithms have been developed for checking branching bisimulation and various tools have
been developed that verify branching bisimulation for large systems [GV90, JGKW20].
There is a well-known connection between notions of bisimulation and various modal
logics, first discovered by Hennessy and Milner [
HM85
] for strong bisimulation, and then
extended to weak and branching bisimulation by De Nicola and Vaandrager [
dNV95
]. Let
↔
be a bisimilarity relation, and let
Th
(
s
) be the set of formulas in some modal logic that
are true in
s
. A Hennessy-Milner theorem is a theorem relating the bisimulation and the
logic by showing that two states are bisimilar precisely when their theories coincide:
s↔t⇐⇒ Th(s) = Th(t).
Hennessy and Milner proved such a theorem for Hennessy-Milner Logic and strong
bisimulation, while De Nicola and Vaandrager extended this to Hennessy-Milner Logic
1
and
weak bisimulation, and Hennessy-Milner Logic with Until and branching bisimulation.
In this paper, we explore what a directed variant of such a theorem would look like by
considering what form of “directed bisimulation” relation corresponds to inclusion of theories.
Hennessy-Milner logics typically have negation, so if the theory of one state is included in
the other, then they are equal. As a consequence, Hennessy-Milner logics typically do not
permit non-trivial inclusions of theories, so we must first replace the logic with a positive
version. Writing
→
for our new relation and
ThP
(
s
) for the theory of
s
in this new, positive,
logic, we prove the property
s→t⇐⇒ ThP(s)⊆ThP(t).(0.1)
Our constructions ensure that
s↔t
precisely when
s→t
and
t→s
, and that
ThP
(
s
) =
ThP
(
t
) precisely when
Th
(
s
) =
Th
(
t
). The undirected Hennessy-Milner theorem
is thus an immediate consequence of our directed variant.
Our proof of Equation (0.1) uses the notion of apartness, which is the dual notion of
bisimulation, studied previously by Geuvers and Jacobs [
GJ21
]. Two states are bisimilar
precisely when they are not apart. The property we prove is thus
s#> t ⇐⇒ ∃φ. φ ∈ThP(s)−ThP(t),(0.2)
where φis called the distinguishing formula.
Unlike bisimulation, apartness is an inductive notion, meaning that we can perform our
proofs by an induction on the derivation of an apartness. It turns out that the structure of
this derivation closely mirrors the distinguishing formula, making the proof straightforward.
This was previously shown by Geuvers in relation to strong and weak bisimulation in [
Geu22
],
but a straightforward inductive proof does not work in the branching setting when the logic
includes an until operator.
In this paper we study the directed constructions for branching bisimulation. Concretely,
we define and study (Section 2) a logic PHMLU of Positive Hennessy-Milner Logic with
Until formulas (Subsection 2.1), as well as a directed branching bisimulation relation
→db
(Subsection 2.2) and a directed branching apartness relation
#>db
(Subsection 2.3). We
then show that Equation (0.2) (for PHMLU and branching apartness) holds, and from that
we conclude that Equation (0.1) holds as well. There are differences between HMLU and
1This involved modifying the semantics to account for silent steps.