Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
DOI10.1007/3-540-45089-0_5zbMATH Open1279.68152OpenAlexW1521991348MaRDI QIDQ3559779FDOQ3559779
Authors: Carsten Fritz 
Publication date: 7 May 2010
Published in: Implementation and Application of Automata (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-45089-0_5
Recommendations
Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cited In (24)
- Applicability of fair simulation
- Automata theory and model checking
- Linear temporal logic with until and next, logical consecutions
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition
- Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
- From LTL to unambiguous Büchi automata via disambiguation of alternating automata
- Title not available (Why is that?)
- Transformation from PLTL to automata via NFGs
- Simulation relations for alternating Büchi automata
- From linear temporal logics to Büchi automata: the early and simple principle
- Title not available (Why is that?)
- Branching time logics \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha }\) with operations \textit{Until} and \textit{Since} based on bundles of integer numbers, logical consecutions, deciding algorithms
- Automata-Theoretic Model Checking Revisited
- Tool support for learning Büchi automata and linear temporal logic
- Temporal logic motion planning for dynamic robots
- GSTE is partitioned model checking
- Title not available (Why is that?)
- Almost linear Büchi automata
- Converting a Büchi alternating automaton to a usual nondeterministic one
- From LTL to deterministic automata. A safraless compositional approach
- Title not available (Why is that?)
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Multi-Valued Reasoning about Reactive Systems
This page was built for publication: Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3559779)
