Computing measures of weak-MSO definable sets of trees
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917155241459712 |
|---|---|
| author | Niwiński, Damian Przybyłko, Marcin Skrzypczak, Michał |
| author_facet | Niwiński, Damian Przybyłko, Marcin Skrzypczak, Michał |
| contents | This work addresses the problem of computing measures of recognisable sets of infinite trees. An algorithm is provided to compute the probability measure of a tree language recognisable by a weak alternating automaton, or equivalently definable in weak monadic second-order logic. The measure is the uniform coin-flipping measure or more generally it is generated by a~branching stochastic process. The class of tree languages in consideration, although smaller than all regular tree languages, comprises in particular the languages definable in the alternation-free mu-calculus or in temporal logic CTL. Thus, the new algorithm may enhance the toolbox of probabilistic model checking. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_13479 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Computing measures of weak-MSO definable sets of trees Niwiński, Damian Przybyłko, Marcin Skrzypczak, Michał Formal Languages and Automata Theory This work addresses the problem of computing measures of recognisable sets of infinite trees. An algorithm is provided to compute the probability measure of a tree language recognisable by a weak alternating automaton, or equivalently definable in weak monadic second-order logic. The measure is the uniform coin-flipping measure or more generally it is generated by a~branching stochastic process. The class of tree languages in consideration, although smaller than all regular tree languages, comprises in particular the languages definable in the alternation-free mu-calculus or in temporal logic CTL. Thus, the new algorithm may enhance the toolbox of probabilistic model checking. |
| title | Computing measures of weak-MSO definable sets of trees |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2410.13479 |