Linear temporal logic -- from infinite to finite horizon

DOI10.1007/978-3-030-88885-5_1zbMath1497.03035OpenAlexW3205916232MaRDI QIDQ2147173

Lucas M. Tabajara, Moshe Y. Vardi

Publication date: 22 June 2022

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Logic in computer science (03B70) Temporal logic (03B44)

Uses Software

• MONA
• Acacia+
• Strix
• Unbeast
• BoSy

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Synthesis of Reactive(1) designs
• Automata, logics, and infinite games. A guide to current research
• First-order vs. second-order encodings for \textsc{ltl}\(_f\)-to-automata translation
• Beyond Hyper-Minimisation--Minimising DBAs and DPAs is NP-Complete
• Unbeast: Symbolic Bounded Synthesis
• Formally Reasoning About Quality
• Encodings of Bounded Synthesis
• Exponential Determinization for ω‐Automata with a Strong Fairness Acceptance Condition
• Bounded Synthesis
• Infinite Games
• Structural Synthesis for GXW Specifications
• Deciding parity games in quasipolynomial time
• Deterministic generators and games for Ltl fragments
• High-Quality Synthesis Against Stochastic Environments
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Automata-Theoretic Model Checking Revisited
• Implementation and Application of Automata