Ramsey-Based Inclusion Checking for Visibly Pushdown Automata

DOI10.1145/2774221zbMath1367.68169OpenAlexW2063384625MaRDI QIDQ5277899

Martin Lange, Oliver Friedmann, Felix Klaedtke

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2774221

zbMATH Keywords

verificationdecision problemsnested wordsvisibly pushdown languagesautomata over finite and infinite words

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Uses Software

• OCaml
• Antichains
• OpenNWA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Simulation relations for alternating Büchi automata
• The complementation problem for Büchi automata with applications to temporal logic
• Alternating automata on infinite trees
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Reasoning about infinite computations
• Improved Ramsey-Based Büchi Complementation
• Ramsey-Based Analysis of Parity Automata
• State of Büchi Complementation
• Advanced Ramsey-Based Büchi Automata Inclusion Testing
• Adding nesting structure to words
• Complementation, Disambiguation, and Determinization of Büchi Automata Unified
• When Simulation Meets Antichains
• Efficient Büchi Universality Checking
• The Büchi Complementation Saga
• Tighter Bounds for the Determinisation of Büchi Automata
• Büchi Complementation and Size-Change Termination
• Antichains for the Automata-Based Approach to Model-Checking
• Visibly Pushdown Automata: Universality and Inclusion via Antichains
• The size-change principle for program termination
• Nested interpolants
• Ramsey Goes Visibly Pushdown
• A Proof System for the Linear Time μ-Calculus
• The tree width of auxiliary storage
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Antichains: A New Algorithm for Checking Universality of Finite Automata

This page was built for publication: Ramsey-Based Inclusion Checking for Visibly Pushdown Automata