A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes

DOI10.1007/978-3-642-19805-2_18zbMATH Open1326.68187OpenAlexW1549097197MaRDI QIDQ3000614FDOQ3000614

Authors Naoki Kobayashi 

Publication date 19 May 2011

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19805-2_18

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A type-directed abstraction refinement approach to higher-order model checking
• A traversal-based algorithm for higher-order model checking
• A ZDD-Based Efficient Higher-Order Model Checking Algorithm
• Practical alternating parity tree automata model checking of higher-order recursion schemes
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.

Cited in

(8)

• Cost Automata, Safe Schemes, and Downward Closures
• scientific article; zbMATH DE number 7199579 (Why is no real title available?)
• scientific article; zbMATH DE number 1406216 (Why is no real title available?)
• Recursion schemes and the WMSO+U logic
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Functional programs as compressed data
• Simply typed fixpoint calculus and collapsible pushdown automata
• A traversal-based algorithm for higher-order model checking

Describes a project that uses

Uses Software

• BLAST
• SLAM

This page was built for publication: A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes

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