https://scholars.lib.ntu.edu.tw/handle/123456789/607929
標題: | Congruence Relations for Büchi Automata | 作者: | Li Y YIH-KUEN TSAY Turrini A Vardi M.Y Zhang L. |
關鍵字: | Formal verification;Asymptotically optimal;Buchi automata;Deterministic finite automata;Number of state;Finite automata | 公開日期: | 2021 | 卷: | 13047 LNCS | 起(迄)頁: | 465-482 | 來源出版物: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 摘要: | We revisit congruence relations for Büchi automata, which play a central role in automata-based formal verification. The size of the classical congruence relation is in 3O(n2), where n is the number of states of the given Büchi automaton. We present improved congruence relations that can be exponentially coarser than the classical one. We further give asymptotically optimal congruence relations of size 2 O ( n log n ). Based on these optimal congruence relations, we obtain an optimal translation from a Büchi automaton to a family of deterministic finite automata (FDFA), which can be made to accept either the original language or its complement. To the best of our knowledge, our construction is the first direct and optimal translation from Büchi automata to FDFAs. |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-85119882008&doi=10.1007%2f978-3-030-90870-6_25&partnerID=40&md5=9e4575b38de3c5724f99d22d5951719e https://scholars.lib.ntu.edu.tw/handle/123456789/607929 |
ISSN: | 03029743 | DOI: | 10.1007/978-3-030-90870-6_25 |
顯示於: | 資訊管理學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。