Efficient approach of translating LTL formulae into Büchi automata

DOI10.1007/s11704-015-4302-2zbMath1403.68130OpenAlexW1996949332MaRDI QIDQ1633083

Zheng Qin, Xiaomin Du, Lai-Xiang Shan

Publication date: 19 December 2018

Published in: Frontiers of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11704-015-4302-2

zbMATH Keywords

model checkingBüchi automataacceptance degreeon-the-fly de-generalization

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)

Uses Software

• SPIN
• CUDD
• BuDDy
• SPOT
• LTL2BA
• lbtt

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Three SCC-Based Emptiness Checks for Generalized Büchi Automata
• LTL to Büchi Automata Translation: Fast and More Deterministic
• Alternation Removal in Büchi Automata
• Graph-Based Algorithms for Boolean Function Manipulation
• Manipulating LTL Formulas Using Spot 1.0

This page was built for publication: Efficient approach of translating LTL formulae into Büchi automata