Büchi complementation made tighter. (English) Zbl 1096.68081
Summary: The complementation problem 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 involves determinization. The \(2^{n}\) blow-up that is caused by the subset construction is justified by a tight lower bound. 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. From a theoretical point of view, the problem is considered solved since 1988, when Safra came up with a determinization construction for Büchi automata, leading to a \(2^{O(n \log n)}\) complementation construction, and Michel came up with a matching lower bound.
A careful analysis, however, of the exact blow-up in Safra’s and Michel’s bounds reveals an exponential gap in the constants hiding in the \(O(\;)\) notations: while the upper bound on the number of states in Safra’s complementary automaton is \(n^{2n}\), Michel’s lower bound involves only an \(n\)! blow up, which is roughly (\(n/e\))\(^{n}\). The exponential gap exists also in more recent complementation constructions. In particular, the upper bound on the number of states in the complementation construction of Kupferman and Vardi, which avoids determinization, is \((6n)^{n}\). This is in contrast with the case of automata on finite words, where the upper and lower bounds coincides.
In this work we describe an improved complementation construction for nondeterministic Büchi automata and analyze its complexity. We show that the new construction results in an automaton with at most \((0.96n)^{n}\) states. While this leaves the problem about the exact blow up open, the gap is now exponentially smaller. From a practical point of view, our solution enjoys the simplicity of the construction of Kupferman and Vardi, and results in much smaller automata.
A careful analysis, however, of the exact blow-up in Safra’s and Michel’s bounds reveals an exponential gap in the constants hiding in the \(O(\;)\) notations: while the upper bound on the number of states in Safra’s complementary automaton is \(n^{2n}\), Michel’s lower bound involves only an \(n\)! blow up, which is roughly (\(n/e\))\(^{n}\). The exponential gap exists also in more recent complementation constructions. In particular, the upper bound on the number of states in the complementation construction of Kupferman and Vardi, which avoids determinization, is \((6n)^{n}\). This is in contrast with the case of automata on finite words, where the upper and lower bounds coincides.
In this work we describe an improved complementation construction for nondeterministic Büchi automata and analyze its complexity. We show that the new construction results in an automaton with at most \((0.96n)^{n}\) states. While this leaves the problem about the exact blow up open, the gap is now exponentially smaller. From a practical point of view, our solution enjoys the simplicity of the construction of Kupferman and Vardi, and results in much smaller automata.
MSC:
| 68Q45 | Formal languages and automata |
References:
| [1] | DOI: 10.1016/0304-3975(93)90160-U · Zbl 0786.68071 · doi:10.1016/0304-3975(93)90160-U |
| [2] | DOI: 10.1006/inco.2001.3085 · Zbl 1009.68071 · doi:10.1006/inco.2001.3085 |
| [3] | DOI: 10.1109/32.588521 · doi:10.1109/32.588521 |
| [4] | DOI: 10.1145/377978.377993 · Zbl 1171.68551 · doi:10.1145/377978.377993 |
| [5] | Kurshan R. P., Computer Aided Verification of Coordinating Processes (1994) · Zbl 0822.68116 |
| [6] | DOI: 10.1007/3-540-44929-9_36 · doi:10.1007/3-540-44929-9_36 |
| [7] | DOI: 10.1016/0304-3975(87)90133-2 · Zbl 0636.68108 · doi:10.1016/0304-3975(87)90133-2 |
| [8] | Rabin M. O., IBM Journal of Research and Development 3 pp 115– |
| [9] | DOI: 10.1016/0304-3975(87)90008-9 · Zbl 0613.03015 · doi:10.1016/0304-3975(87)90008-9 |
| [10] | DOI: 10.1002/sapm1993893233 · Zbl 0784.11007 · doi:10.1002/sapm1993893233 |
| [11] | DOI: 10.1006/inco.1994.1092 · Zbl 0827.03009 · doi:10.1006/inco.1994.1092 |
| [12] | DOI: 10.1016/S0019-9958(83)80051-5 · Zbl 0534.03009 · doi:10.1016/S0019-9958(83)80051-5 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
