Recursion schemes and the WMSO+U logic

DOI10.4230/LIPICS.STACS.2018.53MaRDI QIDQ3304152zbMATH OpenOpenAlexFDO

Authors Paweł Parys

Publication date 5 August 2020

Full work available at URL https://doi.org/10.4230/LIPIcs.STACS.2018.53

zbMATH Keywords

boundednessintersection typeshigher-order recursion schemesWMSO+U logic

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Recommendations

• Weak \(\text{MSO}+U\) over infinite trees
• The Caucal hierarchy: interpretations in the (W)MSO+\(\mathsf{U}\) logic
• Weak MSO+U with path quantifiers over infinite trees
• scientific article; zbMATH DE number 6829362
• The diagonal problem for higher-order recursion schemes is decidable

Cites work

• scientific article; zbMATH DE number 6829362 (Why is no real title available?)
• scientific article; zbMATH DE number 2087432 (Why is no real title available?)
• A Note on Decidable Separability by Piecewise Testable Languages
• A model for behavioural properties of higher-order programs
• 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
• Computer Science Logic
• Indexed Grammars—An Extension of Context-Free Grammars
• Krivine machines and higher-order schemes
• Logical theories and compatible operations
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• Model checking higher-order programs
• Models of \(\lambda\)-calculus and the weak MSO logic
• New algorithm for weak monadic second-order logic on inductive structures
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Simply typed fixpoint calculus and collapsible pushdown automata
• The IO- and OI-hierarchies
• The diagonal problem for higher-order recursion schemes is decidable
• The first order properties of products of algebraic systems
• The monadic theory of order
• Unboundedness and downward closures of higher-order pushdown automata
• Using models to model-check recursive schemes
• Weak MSO with the unbounding quantifier
• Weak MSO+U with path quantifiers over infinite trees
• Weak \(\text{MSO}+U\) over infinite trees

Cited in

(5)

• scientific article; zbMATH DE number 7199579 (Why is no real title available?)
• On the termination problem for probabilistic higher-order recursive programs
• scientific article; zbMATH DE number 7526052 (Why is no real title available?)
• The Caucal hierarchy: interpretations in the (W)MSO+\(\mathsf{U}\) logic
• Weak \(\text{MSO}+U\) over infinite trees

Describes a project that uses

Uses Software

• TravMC2

This page was built for publication: Recursion schemes and the WMSO+U logic

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