Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata

DOI10.1007/3-540-45089-0_5zbMath1279.68152OpenAlexW1521991348MaRDI QIDQ3559779

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

Mathematics Subject Classification ID

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)

Related Items (15)

From LTL to deterministic automata. A safraless compositional approach ⋮ Applicability of fair simulation ⋮ Automata Theory and Model Checking ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL ⋮ GSTE is partitioned model checking ⋮ Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic ⋮ Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition ⋮ From linear temporal logics to Büchi automata: the early and simple principle ⋮ 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 ⋮ Linear temporal logic with until and next, logical consecutions ⋮ Transformation from PLTL to automata via NFGs ⋮ Automata-Theoretic Model Checking Revisited ⋮ Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking ⋮ Temporal logic motion planning for dynamic robots

This page was built for publication: Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata