On-the-Fly Stuttering in the Construction of Deterministic ω-Automata

DOI10.1007/978-3-540-76336-9_7zbMath1139.68366OpenAlexW1557490459MaRDI QIDQ3503894

Joachim Klein, Christel Baier

Publication date: 10 June 2008

Published in: Implementation and Application of Automata (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-76336-9_7

zbMATH Keywords

deterministicdeterminizationLTL\(\omega \)-automatonRabinstuttering

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (7)

From LTL to deterministic automata. A safraless compositional approach ⋮ Unnamed Item ⋮ New Optimizations and Heuristics for Determinization of Büchi Automata ⋮ Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis ⋮ Generic Emptiness Check for Fun and Profit ⋮ Quantitative Analysis under Fairness Constraints ⋮ Back to the future: a fresh look at linear temporal logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Stutter-invariant temporal properties are expressible without the next-time operator
• A note on a question of Peled and Wilke regarding stutter-invariant LTL
• A stubborn attack on state explosion
• Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic
• An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages
• Automata, logics, and infinite games. A guide to current research

This page was built for publication: On-the-Fly Stuttering in the Construction of Deterministic ω-Automata