Efficient normalization of linear temporal logic

DOI10.1145/3651152MaRDI QIDQ6966601zbMATH OpenFDO

Authors Javier Esparza, Rubén Rubio, Salomon Sickert

Publication date 27 June 2025

Published in Journal of the ACM (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1145/3651152

zbMATH Keywords

normal formlinear temporal logicdeterministic automataweak alternating automata

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 747023 (Why is no real title available?)
• scientific article; zbMATH DE number 1479635 (Why is no real title available?)
• scientific article; zbMATH DE number 1759492 (Why is no real title available?)
• scientific article; zbMATH DE number 3999901 (Why is no real title available?)
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• A Syntactical Proof of the Canonical Reactivity Form for Past Linear Temporal Logic
• A Unified Translation of Linear Temporal Logic to ω-Automata
• A combinatorial approach to the theory of ω-automata
• A simple rewrite system for the normalization of linear temporal logic
• Alternating finite automata on -words
• Alternation
• An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
• An automata-theoretic approach to linear temporal logic
• Characterization of temporal property classes
• Completing the temporal picture
• Determinization and limit-determinization of Emerson-Lei automata
• First-order definable languages
• From Spot 2.0 to Spot 2.10: What’s New?
• Implementation and Application of Automata
• Mathematical Foundations of Computer Science 2003
• On complementing nondeterministic Büchi automata
• On the Krohn-Rhodes cascaded decomposition theorem
• On the translation of automata to linear temporal logic
• Owl: a library for \(\omega \)-words, automata, and LTL
• Practical applications of the alternating cycle decomposition
• Revisiting separation: algorithms and complexity
• Temporal logic and fair discrete systems
• The temporal semantics of concurrent programs
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Verification of reactive systems. Formal methods and algorithms.
• Weak Second‐Order Arithmetic and Finite Automata
• Weak alternating automata are not that weak

Cited in

(1)

• Validity of contextual formulas

This page was built for publication: Efficient normalization of linear temporal logic

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