Recursion Schemes, the MSO Logic, and the U quantifier
We study the model-checking problem for recursion schemes: does the tree generated by a given higher-order recursion scheme satisfy a given logical sentence. The problem is known to be decidable for sentences of the MSO logic. We prove decidability for an extension of MSO in which we additionally ha...
| 出版年: | Logical Methods in Computer Science |
|---|---|
| 第一著者: | |
| フォーマット: | 論文 |
| 言語: | 英語 |
| 出版事項: |
Logical Methods in Computer Science e.V.
2020-02-01
|
| 主題: | |
| オンライン･アクセス: | https://lmcs.episciences.org/4885/pdf |
| 要約: | We study the model-checking problem for recursion schemes: does the tree
generated by a given higher-order recursion scheme satisfy a given logical
sentence. The problem is known to be decidable for sentences of the MSO logic.
We prove decidability for an extension of MSO in which we additionally have an
unbounding quantifier U, saying that a subformula is true for arbitrarily large
finite sets. This quantifier can be used only for subformulae in which all free
variables represent finite sets (while an unrestricted use of the quantifier
leads to undecidability). We also show that the logic has the properties of
reflection and effective selection for trees generated by recursion schemes. |
|---|---|
| ISSN: | 1860-5974 |