A higher order modal fixed point logic

DOI10.1007/978-3-540-28644-8_33MaRDI QIDQ5311496zbMATH OpenOpenAlexFDO

Authors Mahesh Viswanathan, Ramesh Viswanathan

Publication date 23 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b100113

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Space-efficient fragments of higher-order fixpoint logic
• The complexity of model-checking tail-recursive higher-order fixpoint logic
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• Alternating parity Krivine automata
• Mathematical Foundations of Computer Science 2005

Cited in

(35)

• Temporal logic with recursion
• Local higher-order fixpoint iteration
• Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking
• Fixed points of formulas with double modalities
• Alternating parity Krivine automata
• Verification of non-regular program properties
• Capturing bisimulation-invariant complexity classes with higher-order modal fixpoint logic
• A Fixpoint Semantics for Ordered Logic
• Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
• scientific article; zbMATH DE number 1795986 (Why is no real title available?)
• Model-checking process equivalences
• The complexity of model-checking tail-recursive higher-order fixpoint logic
• A type-directed negation elimination
• Alternation is strict for higher-order modal fixpoint logic
• scientific article; zbMATH DE number 7455743 (Why is no real title available?)
• A probabilistic higher-order fixpoint logic
• On higher-order logical grounds
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• Three notes on the complexity of model checking fixpoint logic with chop
• Propositional dynamic logic for higher-order functional programs
• Temporal Logic with Recursion.
• The tail-recursive fragment of timed recursive CTL
• On higher-order reachability games vs may reachability
• Temporal logics with language parameters
• Capturing bisimulation-invariant exponential-time complexity classes
• Temporal verification of programs via first-order fixpoint logic
• A type-based HFL model checking algorithm
• Model checking timed recursive CTL
• Separating the expressive power of propositional dynamic and modal fixpoint logics
• An overview of the HFL model checking project
• Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
• A cyclic proof system for HFL\(_\mathbb{N}\)
• A probabilistic higher-order fixpoint logic
• On the relationship between Dijkstra monads and higher-order fixpoint logic
• Modelling higher-order dual nondeterminacy

This page was built for publication: A higher order modal fixed point logic

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