A type-based HFL model checking algorithm

DOI10.1007/978-3-030-34175-6_8MaRDI QIDQ6536312zbMATH OpenFDO

Authors Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada

Publication date 19 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-34175-6_8

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Higher-order program verification via HFL model checking
• Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• CONCUR 2004 - Concurrency Theory
• On the relationship between higher-order recursion schemes and higher-order fixpoint logic

Cites work

• A type-directed abstraction refinement approach to higher-order model checking
• A type-directed negation elimination
• Automata, logics, and infinite games. A guide to current research
• CONCUR 2004 - Concurrency Theory
• Higher-order program verification via HFL model checking
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• scientific article; zbMATH DE number 1500523 (Why is no real title available?)
• Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
• Model-checking process equivalences
• On the relationship between higher-order recursion schemes and higher-order fixpoint logic
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• The Complexity of Model Checking Higher-Order Fixpoint Logic

Cited in

(3)

• A probabilistic higher-order fixpoint logic
• Model checking timed recursive CTL
• An overview of the HFL model checking project

This page was built for publication: A type-based HFL model checking algorithm

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