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

DOI10.1007/978-3-540-75560-9_7zbMath1137.68429OpenAlexW1523208067MaRDI QIDQ3498457

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

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

Related Items

Unnamed Item ⋮ Model-checking process equivalences ⋮ The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic ⋮ Local higher-order fixpoint iteration

Cites Work

• Unnamed Item
• Uniform inevitability is tree automaton ineffable
• BDD-based decision procedures for the modal logic K ★
• Tools and Algorithms for the Construction and Analysis of Systems
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• CONCUR 2004 - Concurrency Theory
• Experimental Evaluation of Classical Automata Constructions
• Antichains: A New Algorithm for Checking Universality of Finite Automata