---
_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'
...