Un método de diseño de autómatas, guiado por invariantes

Abstract

En este trabajo se describe un método de diseño de Autómatas Finitos a partir del predicado de primer orden que define su conjunto de aceptación. El método se basa en construir lo que aquí se ha denominado un Conjunto de Invariantes de Estado Fuerte, cíef. Los invariantes son predicados sobre las cadenas de entrada, asociados a los estados. La construcción se realiza estudiando cómo se transforman los predicados al agregar un carácter a su argumento. Simultáneamente se introducen los estados de los cuales dichos predicados son invariantes y se define la función de transición. El método determina los estados finales y construye el inicial. Según las decisiones de diseño adoptadas se puede arribar a un Autómata Determinístico o No Determínistico. Aquí se definen los conjuntos de invariantes de Estado, se demuestran sus propiedades fundamentales y se caracteriza a aquellos que son ciefs. El método asegura la corrección de las construcciones. Se incluye su aplicación en varios casos de estudio.