Sistema de transición bien estructurado

En informática, específicamente en el campo de la verificación formal , los sistemas de transición bien estructurados (WSTS) son una clase general de sistemas de estados infinitos para los cuales muchos problemas de verificación son decidibles , debido a la existencia de una especie de orden entre los estados del sistema que es compatible con las transiciones del sistema. Los resultados de decidibilidad de WSTS se pueden aplicar a redes de Petri , sistemas de canales con pérdida y más.

Recuerde que un cuasi-ordenamiento bueno en un conjunto es un cuasi-ordenamiento (es decir, un preorden o relación binaria transitiva , reflexiva ) tal que cualquier secuencia infinita de elementos , de contiene un par creciente con . Se dice que el conjunto está bien cuasi-ordenado , o abreviadamente wqo .${\ estilo de visualización \ leq}$${\ estilo de visualización X}$ ${\displaystyle x_{0},x_{1},x_{2},\ldots}$${\ estilo de visualización X}$${\displaystyle x_{i}\leq x_{j}}$${\ estilo de visualización i <j}$${\ estilo de visualización X}$

Para nuestros propósitos, un sistema de transición es una estructura , donde es cualquier conjunto (sus elementos se denominan estados ) y (sus elementos se denominan transiciones ). En general, un sistema de transición puede tener una estructura adicional como estados iniciales, etiquetas en las transiciones, estados de aceptación, etc. (indicados por los puntos), pero no nos conciernen aquí.${\displaystyle {\mathcal {S}}=\langle S,\rightarrow,\cdots\rangle}$${\ estilo de visualización S}$${\displaystyle \rightarrow \subseteq S\times S}$

Un sistema de transición bien estructurado consiste en un sistema de transición , tal que${\displaystyle \langle S,\to ,\leq \rangle }$

Un sistema bien estructurado ^[1] es un sistema de transición con un conjunto de estados compuesto por un conjunto de estados de control finito , un conjunto de valores de datos , equipado con un preorden decidible que se extiende a los estados por , que está bien estructurado como se define anterior ( es monótono, es decir, compatible hacia arriba, con respecto a ) y además tiene un conjunto computable de mínimos para el conjunto de predecesores de cualquier subconjunto cerrado hacia arriba de .${\ estilo de visualización (S, \ a)}$${\ estilo de visualización S = Q \ veces D}$${\ estilo de visualización Q}$${\ estilo de visualización D}$${\displaystyle \leq \subseteq D\times D}$${\displaystyle (q,d)\leq (q',d')\Leftrightarrow q=q'\cuña d\leq d'}$${\ estilo de visualización \ a }$${\ estilo de visualización \ leq}$${\ estilo de visualización S}$

El requisito de compatibilidad ascendente