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
v, it is a general formula that an infinite number of signal traces could satisfy. see it's definition here:
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:
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.