Los autómatas temporizados de acción duracional (daTAs) son sistemas de transición de estados como los autómatas temporizados (TAs) que capturan información sobre la ejecución concurrente de acciones y sus duraciones utilizando una semántica basada en maximalidad. Dado que la semántica subyacente de los daTAs es infinita debido a la modelización del progreso del tiempo, las técnicas convencionales de verificación de modelos se vuelven imprácticas para sistemas especificados utilizando daTAs. Por lo tanto, se requiere una representación abstracta finita del comportamiento de un daTA para habilitar la verificación de modelos para tales especificaciones de sistemas.