{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T08:15:03Z","timestamp":1761725703256,"version":"build-2065373602"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,7,23]]},"abstract":"<jats:p>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 &amp;quot;directed&amp;quot; versions of Hennessy-Milner theorems that characterize when the theory of one state is included in the other. For this we introduce &amp;quot;positive modal logics&amp;quot; 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 &amp;quot;directed branching bisimulation&amp;quot; (and directed branching apartness) and &amp;quot;Positive Hennessy-Milner Logic with Until&amp;quot; (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.<\/jats:p>","DOI":"10.46298\/lmcs-21(4:14)2025","type":"journal-article","created":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T01:10:07Z","timestamp":1761700207000},"source":"Crossref","is-referenced-by-count":0,"title":["Positive Hennessy-Milner Logic for Branching Bisimulation"],"prefix":"10.46298","volume":"Volume 21, Issue 4","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[]},{"given":"Komi","family":"Golov","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2025,10,28]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/arxiv.org\/pdf\/2210.07380v6","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/arxiv.org\/pdf\/2210.07380v6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T01:10:07Z","timestamp":1761700207000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/14633"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,28]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-21(4:14)2025","relation":{"has-preprint":[{"id-type":"arxiv","id":"2210.07380v4","asserted-by":"subject"},{"id-type":"arxiv","id":"2210.07380v3","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2210.07380","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2210.07380","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,28]]},"article-number":"14633"}}