From LTL to deterministic automata. A safraless compositional approach

DOI10.1007/s10703-016-0259-2zbMath1368.68233arXiv1402.3388OpenAlexW2557837928MaRDI QIDQ2363815

Salomon Sickert, Jan Křetínský, Javier Esparza

Publication date: 26 July 2017

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1402.3388

zbMATH Keywords

verificationautomata theorytemporal logic

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 (13)

From LTL to deterministic automata. A safraless compositional approach ⋮ Model Checking Probabilistic Systems ⋮ Safraless LTL synthesis considering maximal realizability ⋮ Index appearance record with preorders ⋮ Markov chains and unambiguous automata ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis ⋮ Index Appearance Record for Transforming Rabin Automata into Parity Automata ⋮ Optimal Translation of LTL to Limit Deterministic Automata ⋮ A weakness measure for GR(1) formulae ⋮ A weakness measure for GR(1) formulae ⋮ Back to the future: a fresh look at linear temporal logic

Uses Software

• PRISM
• Isabelle/HOL
• Isabelle/Isar
• SPIN
• Isar
• SPOT
• BEEM
• LTL2BA
• ltl2dstar
• Rabinizer
• Archive Formal Proofs
• LTL_to_DRA
• CAVA LTL Modelchecker

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
• Reasoning about infinite computations
• Isabelle/HOL. A proof assistant for higher-order logic
• From LTL to deterministic automata. A safraless compositional approach
• Comparison of LTL to Deterministic Rabin Automata Translators
• LTL to Büchi Automata Translation: Fast and More Deterministic
• Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata
• On-the-Fly Stuttering in the Construction of Deterministic ω-Automata
• On the Merits of Temporal Testers
• Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
• Safraless Procedures for Timed Specifications
• Tighter Bounds for the Determinisation of Büchi Automata
• Rabinizer: Small Deterministic Automata for LTL(F,G)
• Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
• Manipulating LTL Formulas Using Spot 1.0
• Rabinizer 2: Small Deterministic Automata for LTL ∖ GU
• Deterministic generators and games for Ltl fragments
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Safraless Compositional Synthesis

This page was built for publication: From LTL to deterministic automata. A safraless compositional approach