Alternating automata modulo first order theories

DOI10.1007/978-3-030-25543-5_3MaRDI QIDQ6154872zbMATH OpenFDO

Authors Radu Iosif, Xiao Xu

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-25543-5_3

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Formal languages and automata (68Q45)

Recommendations

• Abstraction refinement for emptiness checking of alternating data automata
• Fixed point guided abstraction refinement for alternating automata
• Fixpoint Guided Abstraction Refinement for Alternating Automata
• Safety alternating automata on data words
• Alternating automata: unifying truth and validity checking for temporal logics

Cited in

(3)

• First order Büchi automata and their application to verification of LTL specifications
• Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures
• Constraint automata on infinite data trees: from CTL\((\mathbb{Z})\text{CTL}^*(\mathbb{Z})\) to decision procedures

This page was built for publication: Alternating automata modulo first order theories

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