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.

翻译：标号迁移系统可从模态逻辑和互模拟两个角度进行研究。Hennessy-Milner定理将这两个概念联系起来，表明两个状态互模拟当且仅当它们满足相同的模态逻辑公式。近期，分离性作为互模拟的对偶概念被研究，并由此导出Hennessy-Milner定理的对偶版本：两个状态可分离当且仅当存在一个模态公式能够区分它们。本文引入Hennessy-Milner定理的“有向”版本，用于刻画一个状态的理论包含于另一个状态的理论的条件。为此，我们提出了仅允许有限使用否定的“正模态逻辑”。进一步，我们引入互模拟和分离性的有向概念，并证明：对于该正模态逻辑，状态s的理论包含于状态t的理论当且仅当s与t有向互模拟。从分离性角度而言，s与t有向分离当且仅当s的理论不包含于t的理论。由该有向Hennessy-Milner定理可自然推出原始结果。具体而言，我们研究了分支互模拟以及带Until的Hennessy-Milner逻辑（HMLU）作为模态逻辑的情形。我们提出“有向分支互模拟”（及有向分支分离性）与“带Until的正Hennessy-Milner逻辑”（PHMLU），并证明Hennessy-Milner定理的有向版本。在此过程中，我们证明每个HMLU公式等价于正HMLU公式的布尔组合——这一结果具有高度非平凡性。由此得到HMLU的一个子逻辑，其表达能力相同但更易于推理。