Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic

DOI10.1007/978-3-540-75560-9_7MaRDI QIDQ3498457zbMATH OpenOpenAlexFDO

Authors Roland Axelsson, Martin Lange

Publication date 15 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75560-9_7

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Space-efficient fragments of higher-order fixpoint logic
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• The complexity of model-checking tail-recursive higher-order fixpoint logic
• Verification of non-regular program properties
• CONCUR 2004 - Concurrency Theory

Cites work

• Antichains: A New Algorithm for Checking Universality of Finite Automata
• BDD-based decision procedures for the modal logic K ★
• CONCUR 2004 - Concurrency Theory
• Experimental Evaluation of Classical Automata Constructions
• scientific article; zbMATH DE number 1304336 (Why is no real title available?)
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• Tools and Algorithms for the Construction and Analysis of Systems
• Uniform inevitability is tree automaton ineffable

Cited in

(10)

• Local higher-order fixpoint iteration
• Verification of non-regular program properties
• The Model Checking Problem for Prefix Classes of Second-Order Logic: A Survey
• Model-Checking First-Order Logic: Automata and Locality
• Model-checking process equivalences
• The complexity of model-checking tail-recursive higher-order fixpoint logic
• scientific article; zbMATH DE number 7455743 (Why is no real title available?)
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• Mathematical Foundations of Computer Science 2005
• A type-based HFL model checking algorithm

This page was built for publication: Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic

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