Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2407.12677 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915135339102208 |
|---|---|
| author | Colcombet, Thomas Doumane, Amina Kuperberg, Denis |
| author_facet | Colcombet, Thomas Doumane, Amina Kuperberg, Denis |
| contents | We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal mu-calculus, a question that had remained open for several decades. The proof goes by translating the question to an algebraic framework, and showing that the languages of regular trees that are recognized by finitary tree algebras whose sorts zero and one are finite are the regular ones, ie. the ones expressible in mu-calculus. This corresponds for trees to a weak form of the key translation of Wilke algebras to omega-semigroup over infinite words, and was also a missing piece in the algebraic theory of regular languages of infinite trees for twenty years. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_12677 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Tree algebras and bisimulation-invariant MSO on finite graphs Colcombet, Thomas Doumane, Amina Kuperberg, Denis Logic in Computer Science We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal mu-calculus, a question that had remained open for several decades. The proof goes by translating the question to an algebraic framework, and showing that the languages of regular trees that are recognized by finitary tree algebras whose sorts zero and one are finite are the regular ones, ie. the ones expressible in mu-calculus. This corresponds for trees to a weak form of the key translation of Wilke algebras to omega-semigroup over infinite words, and was also a missing piece in the algebraic theory of regular languages of infinite trees for twenty years. |
| title | Tree algebras and bisimulation-invariant MSO on finite graphs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.12677 |