Método Teórico de Autómatas

Técnica que reduce problemas de decisión lógicos a cuestiones sobre autómatas finitos o infinitos y las propiedades de lenguaje de los lenguajes que esos autómatas aceptan, empleando traducciones efectivas entre fórmulas/modelos y autómatas de modo que satisfacibilidad, validez o model‑checking se reducen a problemas de vacuidad, inclusión o aceptación de autómatas.