En informática , la enumeración del espacio de estados son métodos que consideran cada estado alcanzable del programa para determinar si un programa satisface una propiedad determinada. [1] A medida que los programas aumentan en tamaño y complejidad, el espacio de estados crece exponencialmente. El espacio de estados utilizado por estos métodos se puede reducir manteniendo sólo las partes del espacio de estados que son relevantes para el análisis. Sin embargo, el uso de técnicas de reducción de estado y memoria hace que el tiempo de ejecución sea un factor limitante importante. [2]