Способ выражения LTL (вариант), чтобы обеспечить поток данных, удовлетворяющий некоторой логике линейного времени.

Question

Линейная временная логика (LTL) используется для проверка системы.В моем случае я трачу некоторое время, чтобы увидеть возможность использования LTL на этот раз для обеспечения ограничения потока данных.Хватит общих слов, давайте возьмем простой пример:

Оператор ДО в выражении u Until v в литах означает событие u до v, это общая формула, которая бесконечное число трасс сигнала может удовлетворить.см. его определение здесь:страница4

нравиться:

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

В моем случае я хочу применить формулы типа LTL к системе, получающей поток данных;Снова возьмем тот же оператор Until.

скажем, у нас есть два входных сигнала: один для константы u и один для константы v.

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

Потоковый процессор, принимающий эти входные данные, если это узел «UNTIL*», выведет:

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

Причина, по которой я различаю ДО со звездочкой - это вся суть вопроса, "u UNTIL* v" истинно только тогда, когда v принимается в качестве выходных данных, как только он появляется во втором потоке, это одна единственная трассировка, удовлетворяющая "u UNTIL* v" с учетом наших входные сигналы. Как выразить это ограничение?!LTL кажется очень общим для этого «механизма обеспечения ограничений».

примечание:Пожалуйста, будьте терпеливы, я не ученый-компьютерщик и не математик, я обычный программист, который пытается изучить что-то новое.

Answer 1

Это интересный вопрос.

Это не прямой вопрос LTL (линейной временной логики) — скорее вопрос о том, существует ли алгоритм или инструмент, который принимает входной поток и модифицирует его несколько минимальным способом для удовлетворения заданного свойства LTL.

Можно ли сделать то, что вы хотите, или уже было сделано, зависит от того, какие именно изменения в потоке разрешены.В вашем примере вы в некотором смысле смешиваете два потока.Обратите внимание, что LTL определяется для алфавитов, в которых каждый символ может иметь несколько утверждений, которые в данный момент являются ИСТИНОЙ.Итак, в вашем примере вы могли бы просто смешать потоки u и v, чтобы получить:

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

Это также удовлетворяло бы формуле LTL.Если способ ремиксирования заключается в том, что предложение в выходном потоке всегда является подмножеством предложений, установленных во входном потоке, то вы можете использовать реактивный синтез получить преобразователь, который осуществляет смешивание/фиксацию потока.Однако это будет работать только в том случае, если для каждого выходного потока действительно существует способ выполнить микширование.

Если существует какое-то количественное понятие смешивания/фиксации, то количественный синтез может быть областью исследований, которая может дать некоторые результаты.Но вам понадобится описание точного критерия оптимизации модификации потока, чтобы увидеть, применимы ли какие-либо результаты из этой области.