From linear temporal logics to Büchi automata: the early and simple principle

DOI10.1007/978-3-030-91384-7_2zbMath1522.68287OpenAlexW4205130856MaRDI QIDQ6041188

Moshe Y. Vardi, Yih-Kuen Tsay

Publication date: 26 May 2023

Published in: Model Checking, Synthesis, and Learning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-91384-7_2

zbMATH Keywords

Büchi automatalinear temporal logicLTLalternating automatatwo-way automataomega-automataPTLautomata-theoretic approachvery weak automata

Mathematics Subject Classification ID

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

Related Items

Model checking, synthesis, and learning

Cites Work

• Assumption/guarantee specifications in linear-time temporal logic
• Alternating finite automata on \(\omega\)-words
• Automata, logics, and infinite games. A guide to current research
• Temporal logic can be more expressive
• Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
• Concepts of Automata Construction from LTL
• Mathematical Foundations of Computer Science 2003
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item