A way to express LTL (varient) to enforce a stream of data to satisfy some linear time logic

Question

Linear Time Logic (LTL) is used for system verification. In my case, I am investing some time, to see the feasibility of using LTL this time to enforce a constraint on a stream of data. Enough of generalities, let's take a simple example:

The operator UNTIL in the expression u Until v in LTL means, event u until v, it is a general formula that an infinite number of signal traces could satisfy. see it's definition here: page4

like:

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

In my case, I want to enforce an LTL like formulae to a system receiving a stream of data; Again let's take the same operator Until.

let's say we have two input signals, one for constant u, and one for constant v.

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

The stream processor taking these inputs, if it is an "UNTIL*" node, would output:

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

The reason I differentiate UNTIL with an asterisk is the whole point of the question, "u UNTIL* v" is only true when v is taken as output as soon as it appears in the second stream, it is one single trace satisfying "u UNTIL* v" given our input signals. How to express this constraint ?! LTL seems very general for this "constraint enforcing mechanism".

note: Please bear with me, I am no computer scientist, nor a mathematician, I am an average programmer who tries to learn new things.

Answer 1

This is an interesting question.

It is not directly an LTL (Linear Temporal Logic) question -- rather a question about whether there is an algorithm or tool that takes an input stream and modifies it a somewhat minimal way to satisfy a given LTL property.

Whether that you want can be done or has been done depends on what exactly the allowed modifications to the stream are. In your example, you are, in a sense, remixing two streams. Note that LTL is defined over alphabets in which every character can have multiple propositions that are TRUE at the time. So in your example, you could have just mixed the u and v stream together to obtain:

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

This would have satisfied the LTL formula as well. If the way in which you remix is that the proposition in the output stream is always a subset of the propositions set in the input stream, then you can use reactive synthesis to obtain a transducer that does the stream mixing/fixing. However, this will only work if for every output stream there actually is a way to perform the mix.

If there is some quantitative notion of mixing/fixing, then quantitative synthesis may be a research area that may have some results. But you would need a description of the precise stream modification optimization criterion to see if any of the results from that area are applicable.