Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
From MaRDI portal
Publication:3559779
DOI10.1007/3-540-45089-0_5zbMath1279.68152OpenAlexW1521991348MaRDI QIDQ3559779
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
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
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
