En informática teórica , un sistema de transición es un concepto utilizado en el estudio de la computación . Se utiliza para describir el comportamiento potencial de sistemas discretos . Consiste en estados y transiciones entre estados, que pueden etiquetarse con etiquetas elegidas de un conjunto; la misma etiqueta puede aparecer en más de una transición. Si el conjunto de etiquetas es un singleton , el sistema esencialmente no tiene etiquetas y es posible una definición más simple que omita las etiquetas.
Los sistemas de transición coinciden matemáticamente con los sistemas de reescritura abstracta (como se explica más adelante en este artículo) y los gráficos dirigidos . Se diferencian de los autómatas de estado finito de varias formas:
- El conjunto de estados no es necesariamente finito, ni siquiera contable.
- El conjunto de transiciones no es necesariamente finito, ni siquiera contable.
- No se proporcionan estados de "inicio" ni estados "finales".
Los sistemas de transición se pueden representar como gráficos dirigidos.
Definicion formal
Formalmente, un sistema de transición es un par ( S , →) donde S es un conjunto de estados y → es una relación de transiciones de estado (es decir, un subconjunto de S × S ). Una transición del estado p al estado q , es decir ( p , q ) ∈ →, se escribe como p → q .
Un sistema de transición etiquetado es una tupla ( S , Λ, →) donde S es un conjunto de estados, Λ es un conjunto de etiquetas y → es una relación de transiciones etiquetadas (es decir, un subconjunto de S × Λ × S ). ( p , α, q ) ∈ → se escribe como
y representa una transición del estado p al estado q con la etiqueta α. Las etiquetas pueden representar diferentes cosas según el idioma de interés. Los usos típicos de las etiquetas incluyen representar la entrada esperada, las condiciones que deben ser verdaderas para desencadenar la transición o las acciones realizadas durante la transición. Los sistemas de transiciones etiquetadas se introdujeron originalmente como sistemas de transición con nombre . [1]
Si, para cualquier p y α, existe solo una tupla ( p , α, q ) en →, entonces se dice que α es determinista (para p ). Si, para cualquier py α, existe al menos una tupla ( p , α, q ) en →, entonces se dice que α es ejecutable (para p ).
Esto puede reformularse en términos de teoría de categorías. Cada sistema de transición de estado etiquetadoes bijetivamente una función de al grupo de poder de indexado por Escrito como , definido por
- .
Por lo tanto, un sistema de transición de estado etiquetado es una F-coalgebra para el funtor.
Relación entre el sistema de transición etiquetado y no etiquetado
Hay muchas relaciones entre estos conceptos. Algunas son simples, como observar que un sistema de transición etiquetado donde el conjunto de etiquetas consta de un solo elemento es equivalente a un sistema de transición sin etiquetar. Sin embargo, no todas estas relaciones son igualmente triviales.
Comparación con los sistemas de reescritura abstracta
Como objeto matemático, un sistema de transición sin etiquetar es idéntico a un sistema de reescritura abstracta (no indexado) . Si consideramos la relación de reescritura como un conjunto indexado de relaciones, como hacen algunos autores, entonces un sistema de transición etiquetado es equivalente a un sistema de reescritura abstracto con los índices como etiquetas. Sin embargo, el enfoque del estudio y la terminología son diferentes. En un sistema de transición, uno está interesado en interpretar las etiquetas como acciones, mientras que en un sistema de reescritura abstracta la atención se centra en cómo los objetos pueden transformarse (reescribirse) en otros. [2]
Extensiones
En la verificación de modelos , a veces se define un sistema de transición para incluir una función de etiquetado adicional para los estados, lo que da como resultado una noción que abarca la estructura de Kripke . [3]
Idiomas de acción son extensiones de sistemas de transición, la adición de un conjunto de fluentes F , un conjunto de valores V , y una función que mapea F × S a V . [4]
Ver también
Referencias
- ^ Robert M. Keller (julio de 1976) " Verificación formal de programas paralelos ", Comunicaciones de la ACM , vol. 19 , nr. 7 , págs. 371–384.
- ^ Marc Bezem, JW Klop, Roel de Vrijer ("Terese"), Sistemas de reescritura de términos , Cambridge University Press, 2003, ISBN 0-521-39115-6 . págs. 7-8.
- ^ Christel Baier ; Joost-Pieter Katoen (2008). Principios de verificación de modelos . La prensa del MIT. pag. 20. ISBN 978-0-262-02649-9.
- ^ Micheal Gelfond, Vladimir Lifschitz (1998) "Lenguajes de acción", artículos electrónicos de Linköping en informática y ciencias de la información , vol. 3 , nr. 16 .