Report
Positive Hennessy-Milner Logic for Branching Bisimulation
| العنوان: | Positive Hennessy-Milner Logic for Branching Bisimulation |
|---|---|
| المؤلفون: | Geuvers, Herman, Golov, Komi |
| سنة النشر: | 2022 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science, Computer Science - Formal Languages and Automata Theory |
| الوصف: | 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. Comment: 17 pages + appendices (22 pages total) |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2210.07380 |
| رقم الانضمام: | edsarx.2210.07380 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |