Alternating automata: Unifying truth and validity checking for temporal logics

DOI10.1007/3-540-63104-6_19zbMath1430.68156OpenAlexW1889008055MaRDI QIDQ5234701

Moshe Y. Vardi

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_19

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (6)

Logic programming approach to automata-based decision procedures ⋮ Model Theoretic Syntax and Parsing ⋮ Alternating automata and temporal logic normal forms ⋮ Temporal logics with language parameters ⋮ Incremental reasoning on monadic second-order logics with logic programming ⋮ Taming past LTL and flat counter systems

Uses Software

• CESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On equations for regular languages, finite automata, and sequential networks
• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• Alternating finite automata on \(\omega\)-words
• The complementation problem for Büchi automata with applications to temporal logic
• Automata-theoretic techniques for modal logics of programs
• Alternating automata on infinite trees
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Propositional dynamic logic of regular programs
• Reasoning about infinite computations
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Decision procedures and expressiveness in the temporal logic of branching time
• Weak alternating automata are not that weak
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Deciding full branching time logic
• The complexity of propositional linear temporal logics
• Alternation

This page was built for publication: Alternating automata: Unifying truth and validity checking for temporal logics