A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2019
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909725429334016 |
|---|---|
| author | Jansen, David N. Groote, Jan Friso Keiren, Jeroen J. A. Wijs, Anton |
| author_facet | Jansen, David N. Groote, Jan Friso Keiren, Jeroen J. A. Wijs, Anton |
| contents | Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than all algorithms for other weak behavioural equivalences, especially weak bisimilarity. With $m$ the number of transitions and $n$ the number of states, the classic $O(m n)$ algorithm was recently replaced by an $O(m (\log \lvert \mathit{Act}\rvert + \log n))$ algorithm, which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari. This results in a simpler algorithm with complexity $O(m \log n)$. Benchmarks show that this new algorithm is also faster and often far more memory efficient than its predecessors. This makes it the best option for branching bisimulation minimisation and preprocessing for weak bisimulation of LTSs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1909_10824 |
| institution | arXiv |
| publishDate | 2019 |
| record_format | arxiv |
| spellingShingle | A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems Jansen, David N. Groote, Jan Friso Keiren, Jeroen J. A. Wijs, Anton Logic in Computer Science Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than all algorithms for other weak behavioural equivalences, especially weak bisimilarity. With $m$ the number of transitions and $n$ the number of states, the classic $O(m n)$ algorithm was recently replaced by an $O(m (\log \lvert \mathit{Act}\rvert + \log n))$ algorithm, which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari. This results in a simpler algorithm with complexity $O(m \log n)$. Benchmarks show that this new algorithm is also faster and often far more memory efficient than its predecessors. This makes it the best option for branching bisimulation minimisation and preprocessing for weak bisimulation of LTSs. |
| title | A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/1909.10824 |