This is joint work with Anton Golov (RU) Labelled transitions systems can be studied both in terms of modal logic and in terms of bisimulation. These two notions are connected by so-called Hennessy-Milner theorems, that show that states are bisimilar precisely when they satisfy the same formulas in some modal logic, in other words, when they have the same theory according to this modal logic.

We introduce a directed version of such theorems, from which the original results follow. To this end, we introduce positive modal logics and directed notions of bisimulation, and then show that the theory of p in this positive logic is included in the theory of q precisely when p is directed bisimilar to q.

We develop these theories in two settings, that of Hennessy-Milner Logic and strong bisimulation, and that of Hennessy-Milner Logic with Until

(HMLU) and branching bisimulation. In the process, we show that every HMLU formula is equivalent to one satisfying a certain positivity property. This gives rise to a sublogic of HMLU that is equally expressive but easier to reason about.

By formulating our constructions in terms of apartness (the complement of bisimulation), we moreover find that all our directed Hennessy-Milner theorems can be proven by structural induction. This results in simpler proofs than one would obtain with traditional approaches.