Uma forma de expressar LTL (varient) para impor um fluxo de dados para satisfazer algum tempo linear lógica

Question

O Tempo Linear Lógica (LTL) é usado para a verificação do sistema.No meu caso, eu estou a investir algum tempo, para ver a viabilidade do uso de LTL desta vez para impor uma restrição em um fluxo de dados.O suficiente de generalidades, vamos dar um exemplo simples:

O operador ATÉ na expressão u Until v em LTL significa, evento u até v, é uma fórmula geral que um número infinito de traços de sinal poderia satisfazer.ver a definição aqui:page4

como:

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

No meu caso, eu quero impor um LTL como fórmulas para um sistema de recepção de um fluxo de dados;Novamente vamos tomar o mesmo operador, Até.

digamos que temos dois sinais de entrada, um para a constante u, e um constante v.

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

O fluxo de processador de tomar essas entradas, se ele é um "ATÉ*" nó de saída seria:

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

A razão de eu diferenciar ATÉ com um asterisco é o ponto da questão, "u ATÉ que* v" só é verdadeiro quando v é tomado como saída, assim que ele aparece no segundo fluxo, é um traço único satisfatório "u ATÉ que* v" dada a nossa sinais de entrada. Como expressar essa restrição ?!LTL parece muito geral para esta "restrição de aplicação do mecanismo de".

nota:Por favor, tenha paciência comigo, eu não sou cientista da computação, nem um matemático, eu sou uma média de programadores que tenta aprender coisas novas.

Answer 1

Esta é uma pergunta interessante.

Ele não é diretamente uma LTL (Linear Temporal Logic) pergunta-ao invés de uma pergunta sobre a existência de um algoritmo ou de uma ferramenta que leva a um fluxo de entrada e se modifica um pouco o mínimo de forma a satisfazer um determinado LTL propriedade.

Se o que você quer pode ser feito ou foi feito depende do que exatamente as modificações permitidas para o fluxo.No seu exemplo, você está, em certo sentido, os remixes de dois córregos.Note que LTL é definido através de alfabetos em que cada personagem pode ter várias proposições que são VERDADEIRAS no momento.Assim, no seu exemplo, você poderia ter apenas misto de u e v de fluxo para obter:

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

Isso teria satisfeito a fórmula LTL bem.Se a maneira na qual você remix é que a proposição em que o fluxo de saída é sempre um subconjunto do conjunto de proposições em que o fluxo de entrada e, em seguida, você pode usar reativa a síntese para obter um transdutor que o fluxo de mistura/fixação.No entanto, isto só irá funcionar se para cada fluxo de saída na verdade, há uma maneira para realizar a mistura.

Se há alguns quantitativos noção de mistura/fixação, em seguida, quantitativa síntese pode ser uma área de pesquisa que pode ter alguns resultados.Mas você precisaria de uma descrição específica fluxo de modificação do critério de otimização para ver se qualquer um dos resultados dessa área são aplicáveis.