The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

DOI10.3233/FI-2021-1996zbMath1478.68150MaRDI QIDQ4989164

Florian Bruse, Etienne Lozes, Martin Lange

Publication date: 21 May 2021

Published in: Fundamenta Informaticae (Search for Journal in Brave)

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• Propositional dynamic logic of context-free programs and fixpoint logic with chop
• Uniform inevitability is tree automaton ineffable
• Space-efficient fragments of higher-order fixpoint logic
• Bisimulation-invariant PTIME and higher-dimensional \(\mu\)-calculus
• Relationships between nondeterministic and deterministic tape complexities
• The expressive power of higher-order types or, life without CONS
• Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic
• Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
• Alternation
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• CONCUR 2004 - Concurrency Theory
• On the Computational Complexity of Algorithms
• On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic

This page was built for publication: The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic