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.

翻译：标记转移系统可从模态逻辑与互模拟两个角度进行研究。亨内西-米尔纳定理将这两个概念联系起来，证明两个状态互模拟当且仅当它们满足相同的模态逻辑公式。近年来，分离性作为互模拟的对偶概念被深入研究，并衍生出亨内西-米尔纳定理的对偶形式：两个状态分离当且仅当存在可区分它们的模态公式。本文提出亨内西-米尔纳定理的“定向”版本，用于刻画一个状态的理论包含于另一个状态理论的情形。为此我们引入仅允许有限使用否定的“正向模态逻辑”。同时，我们定义了定向互模拟与定向分离的概念，并证明在此正向模态逻辑中，状态 $s$ 的理论包含于状态 $t$ 的理论当且仅当 $s$ 与 $t$ 定向互模拟。从分离性角度，我们证明 $s$ 与 $t$ 定向分离当且仅当 $s$ 的理论不包含于 $t$ 的理论。定向版亨内西-米尔纳定理可推导出原始定理。特别地，我们以分支互模拟及带Until算子的亨内西-米尔纳逻辑（HMLU）为案例进行研究。我们提出“定向分支互模拟”（及定向分支分离）与“带Until算子的正向亨内西-米尔纳逻辑（PHMLU）”，并证明定向版亨内西-米尔纳定理。在此过程中，我们证明每个HMLU公式都等价于正向HMLU公式的布尔组合，这是一个非常重要的非平凡结果。由此产生了一个表达能力相同但更易于推理的HMLU子逻辑。