Una forma de expresar LTL (variante) para imponer un flujo de datos para satisfacer cierta lógica de tiempo lineal

Question

Lógica de tiempo lineal (LTL) se utiliza para verificación del sistema.En mi caso, estoy invirtiendo algo de tiempo para ver la viabilidad de usar LTL esta vez para imponer una restricción en un flujo de datos.Basta de generalidades, pongamos un ejemplo sencillo:

El operador HASTA en la expresión u Until v en LTL significa evento u hasta v, es una fórmula general que un numero infinito de trazas de señal podría satisfacer.mira su definición aquí:página 4

como:

u,u,u,v,v,v,...
u,u,u,u,u,u,...
u,v,v,v,v,v,...

En mi caso, quiero aplicar fórmulas similares a LTL en un sistema que recibe un flujo de datos;De nuevo tomemos el mismo operador Hasta.

digamos que tenemos dos señales de entrada, una para u constante y otra para v constante.

u,u,u,u,u,u,...
 , , , ,v,v,...

El procesador de flujo que toma estas entradas, si es un nodo "UNTIL*", generaría:

u,u,u,u,v,v,...

La razón por la que me diferencio HASTA con un asterisco es el objetivo de la pregunta, "u HASTA* v" solo es cierto cuando v se toma como salida tan pronto como aparece en la segunda secuencia, es un único rastro que satisface "u HASTA* v" dada nuestra señales de entrada. ¿Cómo expresar esta restricción?LTL parece muy general para este "mecanismo de aplicación de restricciones".

nota:Por favor, tengan paciencia, no soy informático ni matemático, soy un programador promedio que intenta aprender cosas nuevas.

Answer 1

Esta es una pregunta interesante.

No es directamente una pregunta de LTL (lógica temporal lineal), más bien, una pregunta sobre si hay un algoritmo o herramienta que toma un flujo de entrada y modifica una forma algo mínima de satisfacer una propiedad LTL determinada.

Si lo que desea que se pueda hacer o se ha hecho depende de las modificaciones permitidas a la secuencia. En su ejemplo, usted está, en cierto sentido, remezcando dos arroyos. Tenga en cuenta que LTL se define sobre los alfabetos en los que cada carácter puede tener múltiples proposiciones que son verdaderas en ese momento. Entonces, en su ejemplo, podría haber mezclado la transmisión U y V para obtener:

u,u,u,u,{u,v},{u,v},....

Esto habría satisfecho con la fórmula LTL también. Si la forma en que se remix es que la proposición en el flujo de salida siempre es un subconjunto de las proposiciones establecidas en el flujo de entrada, puede usar la síntesis reactiva para obtener un transductor que hace la mezcla de transmisión. /fijación. Sin embargo, esto solo funcionará si para cada transmisión de salida allí es una forma de realizar la mezcla.

Si hay alguna noción cuantitativa de mezcla / fijación, entonces la síntesis cuantitativa puede ser un área de investigación que pueda tener algunos resultados. Pero necesitaría una descripción del criterio de optimización de modificación de transmisión precisa para ver si alguno de los resultados de esa área es aplicable.