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

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.

Mathematics Subject Classification ID

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

Cited In (7)

• Title not available (Why is that?)
• Cost Automata, Safe Schemes, and Downward Closures
• Recursion Schemes and the WMSO+U Logic
• Simply typed fixpoint calculus and collapsible pushdown automata
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Title not available (Why is that?)
• Functional programs as compressed data

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)