Reachability analysis of first-order definable pushdown systems

DOI10.4230/LIPICS.CSL.2015.244MaRDI QIDQ5351961zbMATH OpenFDO

Authors Lorenzo Clemente, Sławomir Lasota

Publication date 31 August 2017

Full work available at URL https://arxiv.org/abs/1504.02651

zbMATH Keywords

automata theorypushdown systemssaturation techniquesets with atoms

Mathematics Subject Classification ID

Model theory of denumerable and separable structures (03C15) Automata and formal grammars in connection with logical questions (03D05) Formal languages and automata (68Q45)

Recommendations

• Reachability analysis of pushdown automata: Application to model-checking
• Reachability analysis of communicating pushdown systems
• Reachability problem for weak multi-pushdown automata
• Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems
• Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems

Cited in

(10)

• Reactive synthesis from visibly register pushdown automata
• Reachability relations of timed pushdown automata
• Decidability Border for Petri Nets with Data: WQO Dichotomy Conjecture
• Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems
• Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
• Data multi-pushdown automata
• On Reachability Analysis of Pushdown Systems with Transductions: Application to Boolean Programs with Call-by-Reference
• Solvability of orbit-finite systems of linear equations
• Orbit-finite linear programming
• Bidimensional linear recursive sequences and universality of unambiguous register automata

This page was built for publication: Reachability analysis of first-order definable pushdown systems

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