A type-based HFL model checking algorithm

DOI10.1007/978-3-030-34175-6_8zbMATH Open1542.68097MaRDI QIDQ6536312FDOQ6536312

Naoki Kobayashi, Youkichi Hosoi, Takeshi Tsukada

Publication date: 19 April 2024

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automata, logics, and infinite games. A guide to current research
• Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
• Model-checking process equivalences
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• CONCUR 2004 - Concurrency Theory
• A type-directed abstraction refinement approach to higher-order model checking
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• On the relationship between higher-order recursion schemes and higher-order fixpoint logic
• Higher-order program verification via HFL model checking

Cited In (2)

• An overview of the HFL model checking project
• Model checking timed recursive CTL

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)