https://scholars.lib.ntu.edu.tw/handle/123456789/630007
標題: | Towards a Grand Unification of Büchi Complementation Constructions | 作者: | Vardi, Moshe Y. Fogarty, Seth Li, Yong YIH-KUEN TSAY |
公開日期: | 2022 | 出版社: | Springer Science and Business Media Deutschland GmbH | 卷: | 13660 LNCS | 起(迄)頁: | 185-207 | 來源出版物: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 摘要: | The complementation construction for nondeterministic word automata has numerous applications in formal verification. In particular, the language-containment problem, to which many verification problems are reduced, involves complementation. For automata on finite words, which correspond to safety properties, complementation is typically done by determinization using the subset construction. For Büchi automata on infinite words, which are required for the modeling of liveness properties, optimal complementation constructions are quite complicated, as the subset construction is not sufficient. Over the years, three different constructions have been developed for Büchi complementation, based on congruence relations (via Ramsey analysis), progress ranks, and profiles. In this work we unify the three constructions, by showing how profiles can also yield both optimal congruence relations and progress ranks. |
URI: | https://scholars.lib.ntu.edu.tw/handle/123456789/630007 | ISBN: | 978-3-031-22336-5 978-3-031-22337-2 |
ISSN: | 03029743 | DOI: | 10.1007/978-3-031-22337-2_9 |
顯示於: | 資訊管理學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。