LTL to self-loop alternating automata with generic acceptance and back

DOI10.1016/J.TCS.2020.07.015MaRDI QIDQ2202003zbMATH OpenOpenAlexFDO

Authors František Blahoudek, Juraj Major, Jan Strejček

Publication date 17 September 2020

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2020.07.015

zbMATH Keywords

LTLalternating automataomega-automataLTL-to-automata translationltl3tela

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1796123
• LTL to Büchi automata translation: fast and more deterministic
• Verifying the LTL to Büchi automata translation via very weak alternating automata
• LTL to deterministic Emerson-Lei automata
• Concepts of Automata Construction from LTL

Cites work

• scientific article; zbMATH DE number 1670781 (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 1759609 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
• Generic emptiness check for fun and profit
• Implementation and Application of Automata
• LTL to Büchi automata translation: fast and more deterministic
• LTL to deterministic Emerson-Lei automata
• LTL to smaller self-loop alternating automata and back
• Manipulating LTL Formulas Using Spot 1.0
• Modalities for model checking: Branching time logic strikes back
• Model Checking Software
• Model Checking Software
• Owl: a library for \(\omega \)-words, automata, and LTL
• Parallel Explicit Model Checking for Generalized Büchi Automata
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(3)

• Practical “Paritizing” of Emerson-Lei Automata
• ltl3tela
• Mathematical Foundations of Computer Science 2003

Describes a project that uses

Uses Software

• SPIN
• SPOT
• BEEM
• LTL2BA
• Owl
• Delag

This page was built for publication: LTL to self-loop alternating automata with generic acceptance and back

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