From LTL to Symbolically Represented Deterministic Automata

DOI10.1007/978-3-540-78163-9_24MaRDI QIDQ5452723zbMATH OpenOpenAlexFDO

Authors Andreas Morgenstern, Klaus Schneider

Publication date 4 April 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78163-9_24

Mathematics Subject Classification ID

Temporal logic (03B44) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Generating deterministic -automata for most LTL formulas by the breakpoint construction
• From LTL to deterministic automata. A safraless compositional approach
• scientific article; zbMATH DE number 7311251
• Experiments with deterministic -automata for formulas of linear temporal logic
• Implementation and Application of Automata

Cites work

• An efficient pre-determinization algorithm
• Deciding full branching time logic
• Experiments with deterministic -automata for formulas of linear temporal logic
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (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?)
• Implementation and Application of Automata
• Implementation and Application of Automata
• Improving automata generation for linear temporal logic by considering the automaton hierarchy
• On complementing nondeterministic Büchi automata
• Safraless Compositional Synthesis
• Solving Games Without Determinization
• Symbolic Implementation of Alternating Automata
• Unambiguous Büchi automata.

Cited in

(20)

• LTL semantic tableaux and alternating -automata via linear factors
• Determinization and limit-determinization of Emerson-Lei automata
• Limit deterministic and probabilistic automata for \(\mathrm{LTL}\backslash GU\)
• First-order vs. second-order encodings for \textsc{ltl}\(_f\)-to-automata translation
• From LTL to deterministic automata. A safraless compositional approach
• Functional encryption for inner product with full function privacy
• From LTL and limit-deterministic Büchi automata to deterministic parity automata
• Optimal Translation of LTL to Limit Deterministic Automata
• LTL to deterministic Emerson-Lei automata
• scientific article; zbMATH DE number 6527944 (Why is no real title available?)
• Generating deterministic -automata for most LTL formulas by the breakpoint construction
• The quest for a tight translation of Büchi to co-Büchi automata
• Optimal bounds in parametric LTL games
• scientific article; zbMATH DE number 139828 (Why is no real title available?)
• Limit-deterministic Büchi automata for linear temporal logic
• Specification and verification using temporal logics
• Implementation and Application of Automata
• First order Büchi automata and their application to verification of LTL specifications
• On the power of automata minimization in reactive synthesis
• Experiments with deterministic -automata for formulas of linear temporal logic

Describes a project that uses

Uses Software

• LTL2BA

This page was built for publication: From LTL to Symbolically Represented Deterministic Automata

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