Linear temporal logic -- from infinite to finite horizon

DOI10.1007/978-3-030-88885-5_1zbMATH Open1497.03035OpenAlexW3205916232MaRDI QIDQ2147173FDOQ2147173

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

Recommendations

• LTL goal specifications revisited
• Finite-trace linear temporal logic: coinductive completeness
• LTL on finite and process traces: complexity results and a practical reasoner
• A finitary-language semantics for propositional linear temporal logic
• Computer Science Logic

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (11)

• Logical Consecutions in Intransitive Temporal Linear Logic of Finite Intervals
• Title not available (Why is that?)
• Title not available (Why is that?)
• Nesting until and since in linear temporal logic
• Asymptotic behaviour in temporal logic
• Polymodal logic of the class of inductive linear time frames
• Algebraic Methodology and Software Technology
• From Linear to Branching-Time Temporal Logics: Transfer of Semantics and Definability
• Finite-trace linear temporal logic: coinductive completeness
• Linear future semantics and its implementation
• Title not available (Why is that?)

Uses Software

• MONA
• Acacia+
• Strix
• Unbeast
• BoSy

This page was built for publication: Linear temporal logic -- from infinite to finite horizon

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