Experiments with deterministic -automata for formulas of linear temporal logic
From MaRDI portal
Publication:860862
DOI10.1016/J.TCS.2006.07.022zbMATH Open1153.03016OpenAlexW2087107980MaRDI QIDQ860862FDOQ860862
Authors: Joachim Klein, Christel Baier 
Publication date: 9 January 2007
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2006.07.022
Recommendations
- Implementation and Application of Automata
- Generating deterministic \(\omega\)-automata for most LTL formulas by the breakpoint construction
- From LTL to Symbolically Represented Deterministic Automata
- From LTL to deterministic automata. A safraless compositional approach
- scientific article; zbMATH DE number 1786477
Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Temporal logic (03B44)
Cites Work
- Automata, logics, and infinite games. A guide to current research
- Three Partition Refinement Algorithms
- Implementation and Application of Automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Deciding full branching time logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
- Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
- Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
- Title not available (Why is that?)
- Efficient minimization of deterministic weak \(\omega\)-automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (25)
- From LTL to Symbolically Represented Deterministic Automata
- Exponential Determinization for ω‐Automata with a Strong Fairness Acceptance Condition
- Owl: a library for \(\omega \)-words, automata, and LTL
- Minimal counterexamples for linear-time probabilistic verification
- On the power of automata minimization in reactive synthesis
- Generating deterministic \(\omega\)-automata for most LTL formulas by the breakpoint construction
- LTL semantic tableaux and alternating \(\omega\)-automata via linear factors
- Functional encryption for inner product with full function privacy
- State of Büchi complementation
- Back to the future: a fresh look at linear temporal logic
- An improved construction of deterministic omega-automaton using derivatives
- GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
- Generic emptiness check for fun and profit
- LTL to deterministic Emerson-Lei automata
- On-the-Fly Stuttering in the Construction of Deterministic ω-Automata
- Markov chains and unambiguous automata
- Semantic labelling and learning for parity game solving in LTL synthesis
- Index appearance record for transforming Rabin automata into parity automata
- An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages
- Title not available (Why is that?)
- Title not available (Why is that?)
- Index appearance record with preorders
- Optimal Translation of LTL to Limit Deterministic Automata
- Implementation and Application of Automata
- From LTL to deterministic automata. A safraless compositional approach
Uses Software
This page was built for publication: Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q860862)
