| | |
| | |
Stat |
Members: 3643 Articles: 2'488'730 Articles rated: 2609
29 March 2024 |
|
| | | |
|
Article overview
| |
|
Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus | Noaki Kobayashi
; C.-H. Luke Ong
; | Date: |
24 Sep 2011 | Abstract: | Ong has shown that the modal mu-calculus model checking problem
(equivalently, the alternating parity tree automaton (APT) acceptance problem)
of possibly-infinite ranked trees generated by order-n recursion schemes is
n-EXPTIME complete. We consider two subclasses of APT and investigate the
complexity of the respective acceptance problems. The main results are that,
for APT with a single priority, the problem is still n-EXPTIME complete;
whereas, for APT with a disjunctive transition function, the problem is
(n-1)-EXPTIME complete. This study was motivated by Kobayashi’s recent work
showing that the resource usage verification of functional programs can be
reduced to the model checking of recursion schemes. As an application, we show
that the resource usage verification problem is (n-1)-EXPTIME complete. | Source: | arXiv, 1109.5267 | Services: | Forum | Review | PDF | Favorites |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser claudebot
|
| |
|
|
|
| News, job offers and information for researchers and scientists:
| |