Degeneralization algorithm for generation of Büchi automata based on contented situation

DOI10.1155/2015/516104MaRDI QIDQ327746zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Jun Qin, Mingshi Chen, Zheng Qin, Laixiang Shan

Publication date 19 October 2016

Published in Journal of Applied Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.1155/2015/516104

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Efficient approach of translating LTL formulae into Büchi automata
• scientific article; zbMATH DE number 1796123
• Model Checking Software
• scientific article; zbMATH DE number 1670781
• scientific article; zbMATH DE number 6401143

Cites work

• scientific article; zbMATH DE number 1973991 (Why is no real title available?)
• scientific article; zbMATH DE number 1487477 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• Alternation removal in Büchi automata
• Graph-Based Algorithms for Boolean Function Manipulation
• LTL to Büchi automata translation: fast and more deterministic
• Three SCC-based emptiness checks for generalized Büchi automata

Describes a project that uses

Uses Software

• lbtt
• LTL2BA
• SPOT
• SPIN

This page was built for publication: Degeneralization algorithm for generation of Büchi automata based on contented situation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q327746)