--- _id: '4406' abstract: - lang: eng text: We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone function on the lattice of antichains of state sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata. acknowledgement: This research was supported in part by the NSF grants CCR-0234690 and CCR-0225610, and the Belgian FNRS grant 2.4530.02 of the FRFC project “Centre Fédéré en Vérification.” alternative_title: - LNCS author: - first_name: Martin full_name: De Wulf, Martin last_name: De Wulf - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jean full_name: Raskin, Jean-François last_name: Raskin citation: ama: 'De Wulf M, Doyen L, Henzinger TA, Raskin J. Antichains: A new algorithm for checking universality of finite automata. In: Vol 4144. Springer; 2006:17-30. doi:10.1007/11817963_5' apa: 'De Wulf, M., Doyen, L., Henzinger, T. A., & Raskin, J. (2006). Antichains: A new algorithm for checking universality of finite automata (Vol. 4144, pp. 17–30). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/11817963_5' chicago: 'De Wulf, Martin, Laurent Doyen, Thomas A Henzinger, and Jean Raskin. “Antichains: A New Algorithm for Checking Universality of Finite Automata,” 4144:17–30. Springer, 2006. https://doi.org/10.1007/11817963_5.' ieee: 'M. De Wulf, L. Doyen, T. A. Henzinger, and J. Raskin, “Antichains: A new algorithm for checking universality of finite automata,” presented at the CAV: Computer Aided Verification, 2006, vol. 4144, pp. 17–30.' ista: 'De Wulf M, Doyen L, Henzinger TA, Raskin J. 2006. Antichains: A new algorithm for checking universality of finite automata. CAV: Computer Aided Verification, LNCS, vol. 4144, 17–30.' mla: 'De Wulf, Martin, et al. Antichains: A New Algorithm for Checking Universality of Finite Automata. Vol. 4144, Springer, 2006, pp. 17–30, doi:10.1007/11817963_5.' short: M. De Wulf, L. Doyen, T.A. Henzinger, J. Raskin, in:, Springer, 2006, pp. 17–30. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T12:08:41Z date_published: 2006-08-08T00:00:00Z date_updated: 2021-01-12T07:56:45Z day: '08' doi: 10.1007/11817963_5 extern: 1 intvolume: ' 4144' month: '08' page: 17 - 30 publication_status: published publisher: Springer publist_id: '326' quality_controlled: 0 status: public title: 'Antichains: A new algorithm for checking universality of finite automata' type: conference volume: 4144 year: '2006' ...