On Global Model Checking Trees Generated by Higher-Order Recursion Schemes

DOI10.1007/978-3-642-00596-1_9zbMath1234.68252OpenAlexW2155036983MaRDI QIDQ3617724

Luke Ong, Christopher H. Broadbent

Publication date: 31 March 2009

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-00596-1_9

zbMATH Keywords

model checkinggame semanticsrecursion schemeparity gamecollapsible pushdown automaton

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (5)

Recursion Schemes and the WMSO+U Logic ⋮ Cost Automata, Safe Schemes, and Downward Closures ⋮ Krivine machines and higher-order schemes ⋮ Krivine Machines and Higher-Order Schemes ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Note on winning positions on pushdown games with \(\omega\)-regular conditions
• The IO- and OI-hierarchies
• On full abstraction for PCF: I, II and III
• Positional Strategies for Higher-Order Pushdown Parity Games
• Bisimulation, modal logic and model checking games
• Computer Aided Verification
• Collapsible Pushdown Automata and Recursion Schemes
• Mathematical Foundations of Computer Science 2005

This page was built for publication: On Global Model Checking Trees Generated by Higher-Order Recursion Schemes