Sistema de transición

Máquina de estados que puede tener infinitos estados

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 está etiquetado y es posible una definición más simple que omite 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 con los grafos dirigidos . Se diferencian de los autómatas de estados finitos en varios aspectos:

• El conjunto de estados no es necesariamente finito, ni siquiera contable.
• El conjunto de transiciones no es necesariamente finito, ni siquiera contable.
• No se dan estados "iniciales" ni "finales".

Los sistemas de transición se pueden representar como gráficos dirigidos.

Definición formal

Formalmente, un sistema de transición es un par donde es un conjunto de estados y , la relación de transición , es un subconjunto de . Decimos que hay una transición de un estado a otro si y solo si , y la denotamos . ${\displaystyle (S,T)}$ ${\displaystyle S}$ ${\displaystyle T}$ ${\displaystyle S\times S}$ ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle (p,q)\in T}$ ${\displaystyle p\rightarrow q}$

Un sistema de transición etiquetado es una tupla donde es un conjunto de estados, es un conjunto de etiquetas y , la relación de transición etiquetada , es un subconjunto de . Decimos que hay una transición de un estado a otro con etiqueta s/f y la denotamos ${\displaystyle (S,\Lambda ,T)}$ ${\displaystyle S}$ ${\displaystyle \Lambda }$ ${\displaystyle T}$ ${\displaystyle S\times \Lambda \times S}$ ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle \alpha }$ ${\displaystyle (p,\alpha ,q)\in T}$

${\displaystyle p\xrightarrow {\alpha } q\,.}$

Las etiquetas pueden representar diferentes cosas según el lenguaje de interés. Los usos típicos de las etiquetas incluyen representar la entrada esperada, las condiciones que deben ser verdaderas para activar 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]

Casos especiales

• Si, para cualquier y dado , existe solo una única tupla en , entonces se dice que es determinista (para ). ${\displaystyle p}$ ${\displaystyle \alpha }$ ${\displaystyle (p,\alpha ,q)}$ ${\displaystyle T}$ ${\displaystyle \alpha }$ ${\displaystyle p}$
• Si, para cualquier y dado , existe al menos una tupla en , entonces se dice que es ejecutable (para ). ${\displaystyle p}$ ${\displaystyle \alpha }$ ${\displaystyle (p,\alpha ,q)}$ ${\displaystyle T}$ ${\displaystyle \alpha }$ ${\displaystyle p}$

Formulación de coalgebra

La definición formal puede reformularse de la siguiente manera. Los sistemas de transición de estado etiquetados con etiquetas de corresponden uno a uno con las funciones , donde es el funtor de conjunto potencia (covariante) . Bajo esta biyección se envía a , definido por ${\displaystyle S}$ ${\displaystyle \Lambda }$ ${\displaystyle S\to {\mathcal {P}}(\Lambda \times S)}$ ${\displaystyle {\mathcal {P}}}$ ${\displaystyle (S,\Lambda ,T)}$ ${\displaystyle \xi _{T}:S\to {\mathcal {P}}(\Lambda \times S)}$

${\displaystyle p\mapsto \{\,(\alpha ,q)\in \Lambda \times S\mid p\xrightarrow {\alpha } q\,\}}$.

En otras palabras, un sistema de transición de estados etiquetado es una coalgebra para el funtor . ${\displaystyle P(\Lambda \times {-})}$

Relación entre el sistema de transición etiquetado y no etiquetado

Existen muchas relaciones entre estos conceptos. Algunas son simples, como observar que un sistema de transición etiquetado, en el que el conjunto de etiquetas consta de un solo elemento, es equivalente a un sistema de transición no etiquetado. Sin embargo, no todas estas relaciones son igualmente triviales.

Comparación con sistemas de reescritura abstracta

Como objeto matemático, un sistema de transición sin etiquetas es idéntico a un sistema de reescritura abstracto (sin indexar) . Si consideramos la relación de reescritura como un conjunto indexado de relaciones, como hacen algunos autores, entonces un sistema de transición con etiquetas es equivalente a un sistema de reescritura abstracto, donde los índices son las 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 abstracto, el enfoque está 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 también una función de etiquetado adicional para los estados, lo que da como resultado una noción que abarca la de estructura de Kripke . ^[3]

Los lenguajes de acción son extensiones de los sistemas de transición, que agregan un conjunto de fluidos F , un conjunto de valores V y una función que asigna F × S a V . ^[4]

Véase también

• Relación binaria
• Relación ternaria
• Monoide de transición
• Monoide de transformación
• Acción de semigrupo
• Pedido anticipado de simulación
• Bisimulación
• Semántica operacional
• Estructura de Kripke
• Máquina de estados finitos
• Cálculo μ modal

Referencias

1. Robert M. Keller (julio de 1976) "Verificación formal de programas paralelos", Communications of the ACM , vol. 19 , n.° 7 , págs. 371–384.
2. 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.
3. Christel Baier ; Joost-Pieter Katoen (2008). Principios de verificación de modelos . La prensa del MIT. pag. 20.ISBN​ 978-0-262-02649-9.
4. Micheal Gelfond, Vladimir Lifschitz (1998) "Lenguajes de acción", Linköping Electronic Articles in Computer and Information Science , vol. 3 , nr. 16 .