https://scholars.lib.ntu.edu.tw/handle/123456789/630007
Title: | Towards a Grand Unification of Büchi Complementation Constructions | Authors: | Vardi, Moshe Y. Fogarty, Seth Li, Yong YIH-KUEN TSAY |
Issue Date: | 2022 | Publisher: | Springer Science and Business Media Deutschland GmbH | Journal Volume: | 13660 LNCS | Start page/Pages: | 185-207 | Source: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Abstract: | 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 |
Appears in Collections: | 資訊管理學系 |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.