Recursion schemes, the MSO logic, and the \textsf{U} quantifier

MaRDI QIDQ5109508zbMATH OpenFDO

Authors Paweł Parys

Publication date 12 May 2020

Full work available at URL https://arxiv.org/abs/1810.04763, https://lmcs.episciences.org/6111

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Recursion schemes and the WMSO+U logic
• Weak \(\text{MSO}+U\) over infinite trees
• The Caucal hierarchy: interpretations in the (W)MSO+\(\mathsf{U}\) logic
• scientific article; zbMATH DE number 6829362
• Weak MSO+U with path quantifiers over infinite trees

Cites work

• A model for behavioural properties of higher-order programs
• A Note on Decidable Separability by Piecewise Testable Languages
• A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes
• A type-directed abstraction refinement approach to higher-order model checking
• A unified approach to boundedness properties in MSO
• Collapsible pushdown automata and labeled recursion schemes, equivalence, safety and effective selection
• Collapsible pushdown automata and recursion schemes
• Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
• Computer Science Logic
• scientific article; zbMATH DE number 6513118 (Why is no real title available?)
• scientific article; zbMATH DE number 2087432 (Why is no real title available?)
• Indexed Grammars—An Extension of Context-Free Grammars
• IO vs OI in higher-order recursion schemes
• Krivine machines and higher-order schemes
• Logical theories and compatible operations
• Model checking higher-order programs
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• New algorithm for weak monadic second-order logic on inductive structures
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• Ordered tree-pushdown systems
• Recursion schemes and the WMSO+U logic
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Simply typed fixpoint calculus and collapsible pushdown automata
• The Complexity of the Diagonal Problem for Recursion Schemes
• The Complexity of Tree Automata and Logics of Programs
• The diagonal problem for higher-order recursion schemes is decidable
• The first order properties of products of algebraic systems
• The IO- and OI-hierarchies
• The monadic theory of order
• The topological complexity of MSO+U and related automata models
• Unboundedness and downward closures of higher-order pushdown automata
• Using models to model-check recursive schemes
• Weak MSO with the unbounding quantifier

Cited in

(3)

• The Caucal hierarchy: interpretations in the (W)MSO+\(\mathsf{U}\) logic
• Cost Automata, Safe Schemes, and Downward Closures
• Extending the WMSO+U logic with quantification over tuples

Describes a project that uses

Uses Software

• TravMC2

This page was built for publication: Recursion schemes, the MSO logic, and the \textsf{U} quantifier

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