Вопросы линейной темпоральной логики (2)

Question

Если вы не знакомы с LTL (линейная временная логика), пропустите этот вопрос!И да, LTL очень важен для программирования, поскольку он является ядром системы проверки моделей, которую мы используем для проверки программ.

Учитывая эти символы предложений и их значения ...
Gp - всегда P
Fp - иногда P

Что означают следующие утверждения?

GFGp = ?  
FGFp = ?

Мне тяжело с логикой вокруг LTL, и я не могу обернуться вокругПриведенные выше заявления, спасибо за любую помощь!

Answer 1

Сначала немного терминологии:

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

Комбинации правильно сформированных формул (WFF) с (заменой обычных логических символов ...)) &&, ||,! и => также являются правильно построенными формулами.Это все стандартные FOL.(Линейная) временная логика добавляет еще несколько комбинационных возможностей, так что F (WFF), G (WFF) и X (WFF) сами по себе являются правильно построенными формулами.

Поскольку F (WFF) сама по себе может быть правильно сформированной формулой, мы можем иметь F (F (WFF) в качестве правильно сформированной формулы, а также G (F (F (WFF)) и множестводругие странные агломерации. Но что они означают?

Говоря лично, я считаю полезным думать в терминах наборов предложений для сложных формул, где G относится к набору предложений, а F вызываетодно предложение. Как вы упомянули, учитывая некоторый текущий узел, Fp означает, что p будет встречаться по крайней мере в одном из преемников этого узла, а Gp означает, что p будет происходить во всех преемниках текущего узла.

Итак, GFp говорит, что каждое состояние (после этого) имеет по крайней мере одно состояние-преемник, где происходит * 1012. * Таким образом, p гарантированно произойдет (когда-нибудь в будущем) после каждой операции.

FGp означает, что существует по крайней мере одно состояние (после этого), полный набор преемников которого равен p. Таким образом, в процессе есть момент, когда это p когда-либо после.

Далее FGFp говорит, что есть некоторый момент, после которого GFp держится.Опять же, GFp требует, чтобы p следовало (хотя бы один раз) из каждой операции, поэтому все это примерно означает, что когда-нибудь в будущем мы получим p от всего (конечно, это может означать, что это всеp с этого момента или p это только последнее состояние).

GFGp означает, что преемником каждого состояния является FGp.Я предполагаю, что это означает, что каждая точка в пути имеет некоторое состояние преемника, чьи потомки все p (что кажется близким, но не таким же, как весь путь p).

В замешательстве еще?Я.

Answer 2

Я думаю, что

Fp означает, что P наконец будет удерживаться (где-то на следующем пути).

Итак, GFp должен означать, что p будет удерживаться где-то на последующем пути, где бы на пути вы ни находились «стоя». Или, другими словами, р будет занимать бесконечные последующие места пути.

FGp должно означать, что на последующем пути есть место, где с тех пор всегда стоит p.

Я не уверен, но GFGp может быть доказан так же, как FGp

и FGFp такие же, как GFp.

Answer 3

GFGp = пример FGp: все собаки в конечном итоге попадут на небеса, и однажды останутся там навсегда

FGFp = GFp: рано или поздно все собаки попадут на небеса (и если они спустятся / возродятся и т. Д. На земле, они снова отправятся в гавань).

Answer 4

Чтобы упростить понимание, я буду использовать альтернативную запись:

G = globally = [] = always
F = finally = <> = eventually

Так что [] <> p означает, что p встречается бесконечно часто, т. Е. Никогда не прекращается.Например, ** p ******* p ***** p *** p *** ...

Формула <> [] p означает, что в последовательности есть местопосле чего только р происходит непрерывно.Например, *** ppppp ...

Now <> [] <> p означает, что в конечном итоге p будет происходить бесконечно часто, что точно так же, как и p бесконечно часто, то есть <. []<> p = [] <> p.

Точно так же [] <> [] p означает, что с любого момента времени в конечном итоге всегда p.Но это точно говорит о том, что в конечном итоге р, поэтому [] <> [] р = <> [] р.