Linear temporal logic -- from infinite to finite horizon

DOI10.1007/978-3-030-88885-5_1MaRDI QIDQ2147173zbMATHOpenAlexFDO

Authors 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) Temporal logic (03B44) Logic in computer science (03B70)

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

Cites work

• scientific article; zbMATH DE number 4179361 (Why is no real title available?)
• scientific article; zbMATH DE number 3930354 (Why is no real title available?)
• scientific article; zbMATH DE number 44695 (Why is no real title available?)
• scientific article; zbMATH DE number 3460178 (Why is no real title available?)
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 1555955 (Why is no real title available?)
• scientific article; zbMATH DE number 7455737 (Why is no real title available?)
• scientific article; zbMATH DE number 7455747 (Why is no real title available?)
• Automata, logics, and infinite games. A guide to current research
• Automata-Theoretic Model Checking Revisited
• Beyond hyper-minimisation -- minimising DBAs and DPAs is NP-complete
• Bounded Synthesis
• Deciding parity games in quasipolynomial time
• Deterministic generators and games for LTL fragments
• Encodings of bounded synthesis
• Exponential Determinization for ω‐Automata with a Strong Fairness Acceptance Condition
• First-order vs. second-order encodings for \textsc{ltl}\(_f\)-to-automata translation
• Formally reasoning about quality
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• High-Quality Synthesis Against Stochastic Environments
• Implementation and Application of Automata
• Infinite Games
• Structural Synthesis for GXW Specifications
• Synthesis of Reactive(1) designs
• Unbeast: Symbolic Bounded Synthesis

Cited in

(14)

• Algebraic Methodology and Software Technology
• Finite-trace and generalized-reactivity specifications in temporal synthesis
• Logical Consecutions in Intransitive Temporal Linear Logic of Finite Intervals
• scientific article; zbMATH DE number 2086407 (Why is no real title available?)
• Asymptotic behaviour in temporal logic
• Scalable anytime algorithms for learning fragments of linear temporal logic
• scientific article; zbMATH DE number 6174011 (Why is no real title available?)
• Linear future semantics and its implementation
• Nesting until and since in linear temporal logic
• Polymodal logic of the class of inductive linear time frames
• LTL on finite and process traces: complexity results and a practical reasoner
• Finite-trace linear temporal logic: coinductive completeness
• From Linear to Branching-Time Temporal Logics: Transfer of Semantics and Definability
• scientific article; zbMATH DE number 1956573 (Why is no real title available?)

Describes a project that uses

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)