LTL to Büchi Automata Translation: Fast and More Deterministic

DOI10.1007/978-3-642-28756-5_8zbMath1352.68142arXiv1201.0682OpenAlexW1754034137MaRDI QIDQ2894268

Tomáš Babiak, Jan Strejček, Vojtěch Řehák, Mojmír Křetínský

Publication date: 29 June 2012

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

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

From LTL to deterministic automata. A safraless compositional approach, Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning, LTL receding horizon control for finite deterministic systems, Translating Testing Theories for Concurrent Systems, Efficient approach of translating LTL formulae into Büchi automata, From LTL to unambiguous Büchi automata via disambiguation of alternating automata, Degeneralization algorithm for generation of Büchi automata based on contented situation, Automata-driven partial order reduction and guided search for LTL model checking, Safraless LTL synthesis considering maximal realizability, Linear temporal logic for hybrid dynamical systems: characterizations and sufficient conditions, LTL to self-loop alternating automata with generic acceptance and back, Encodings of Bounded Synthesis, Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\), Unnamed Item, A weakness measure for GR(1) formulae, On the Relationship between LTL Normal Forms and Büchi Automata