Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus

DOI10.1007/978-3-642-02930-1_19MaRDI QIDQ5902152zbMATH OpenOpenAlexFDO

Authors

Publication date 14 July 2009

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1109.5267

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Complexity of model checking recursion schemes for fragments of the modal mu-calculus
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• Practical alternating parity tree automata model checking of higher-order recursion schemes
• Model checking higher-order programs
• Using models to model-check recursive schemes

Cited in

(9)

• Some results on complexity of -calculus evaluation in the black-box model
• Modeling and verification of infinite systems with resources
• The mu-calculus and Model Checking
• scientific article; zbMATH DE number 1059247 (Why is no real title available?)
• Recursion schemes, the MSO logic, and the \textsf{U} quantifier
• On the expressive power of higher-order pushdown systems
• Complexity of model checking recursion schemes for fragments of the modal mu-calculus
• On higher-order reachability games vs may reachability
• The complexity of monadic recursion schemes: Exponential time bounds

This page was built for publication: Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5902152)