Señal (verificación de modelos)

Intuitivamente, se dice que una señal es de variabilidad finita, o que posee la propiedad de variabilidad finita, si durante cada intervalo acotado, la letra cambia un número finito de veces. En nuestro ejemplo anterior del ascensor, esta propiedad significaría que un usuario solo puede presionar un botón un número finito de veces durante un tiempo finito. De manera similar, en un tiempo finito, el ascensor solo puede abrir y cerrar su puerta un número finito de veces.

Formalmente, se dice que una señal tiene la propiedad de variabilidad finita, a menos que la secuencia sea infinita y${\displaystyle \bigcup _ {i}I_ {i}}$está acotado. Intuitivamente, la propiedad de variabilidad finita establece que no hay un número infinito de cambios en un tiempo finito. Tener la propiedad de variabilidad finita es similar a la noción de no ser Zeno para una palabra temporizada . ^{[ 1 ]}

La noción de variabilidad acotada es una restricción a la noción de variabilidad finita. Una señal tiene la propiedad de variabilidad acotada si existe un límite inferior entre el inicio de dos intervalos con la misma letra. ^{[ 2 ]}

Antes de dar una definición formal, daremos un ejemplo de señal que es finitamente variable pero no acotada. Tomemos el alfabeto.${\displaystyle A=\{a,b\}}$. Toma el intervalo${\displaystyle \gamma }$que envía los reales de la forma${\displaystyle n+{\frac {c}{n}}}$con${\displaystyle n\in \mathbb {N} }$y${\displaystyle c<n}$a${\displaystyle a}$y todos los demás reales a${\displaystyle b}$Durante cada intervalo de tiempo finito, la letra cambia un número finito de veces. Por lo tanto, esta señal es finitamente variable. Sin embargo, la distancia entre dos ocurrencias sucesivas de la letra${\displaystyle a}$es arbitrariamente pequeño. Por lo tanto, no posee la propiedad de variabilidad limitada.

Sea una secuencia${\displaystyle (I_{0},a_{0}),(I_{1},a_{1}),\dots }$. Si${\displaystyle a_{i}\neq a_{i+1}}$para cada entero${\displaystyle i}$, entonces se dice que la secuencia tiene la propiedad de variabilidad acotada si existe un número real${\displaystyle r>0}$de tal manera que, para cada${\displaystyle i<j}$con${\displaystyle a_{i}=a_{j}}$de tal manera que no exista${\displaystyle k}$con${\displaystyle i<j<k}$y${\displaystyle a_{i}=a_{k}}$entonces la diferencia entre el límite inferior de${\displaystyle I_{j}}$y de${\displaystyle I_{i}}$es al menos${\displaystyle r}$. Tenga en cuenta que cada secuencia${\displaystyle \gamma }$es equivalente a una secuencia${\displaystyle \gamma '}$en la que dos letras sucesivas son distintas. La secuencia${\displaystyle \gamma }$Se dice que tiene la propiedad de variabilidad limitada si y solo si${\displaystyle \gamma '}$posee la propiedad de variabilidad limitada.

Se dice que un conjunto de señales tiene la propiedad de variabilidad acotada si el límite inferior mencionado anteriormente es menor que...${\displaystyle r}$se puede elegir que sea el mismo para cada señal del conjunto.

Ahora bien, esta es la principal razón para considerar señales con variabilidad limitada. Supongamos que necesitamos crear un sistema, como un autómata de señales , que deba recordar todo lo ocurrido en las últimas unidades de tiempo. Si sabemos que la señal tiene variabilidad limitada, podemos calcular un límite superior para el número de acciones que ocurrieron durante una unidad de tiempo. De esta manera, podemos crear dicho sistema y asegurar que solo requiera una memoria finita.

Por ejemplo, para un predicado arbitrario${\displaystyle e}$, la señal que indica si la declaración "${\displaystyle p}$La afirmación «cumple en algún momento de la siguiente unidad de tiempo» posee la propiedad de variabilidad limitada. En efecto, cuando esta afirmación se cumple, permanece así durante una unidad de tiempo completa. Por lo tanto, la diferencia entre dos ocasiones en las que esta afirmación se cumple es mayor que una unidad de tiempo.

Se dice que una señal es bipartita si la secuencia de intervalos comienza con un intervalo singular, es decir, un intervalo cerrado cuyos límites inferior y superior son iguales, lo que da lugar a un conjunto unitario. Y si la secuencia alterna entre intervalos singulares e intervalos abiertos.

Cada señal es equivalente a una señal bipartita. En efecto, cualquier intervalo cerrado por la izquierda es la unión de un intervalo singular y de un intervalo abierto por la izquierda, en ese orden. Lo mismo ocurre con los intervalos cerrados por la derecha.

Un autómata de señales que lee una señal bipartita tiene una forma especial. Su conjunto de ubicaciones se puede dividir en ubicaciones para intervalos singulares y ubicaciones para intervalos abiertos. Cada transición va de una ubicación singular a una abierta y viceversa.