Дорогие студенты,

Обращаю внимание, что в тексте 4 задания сказано, что свойства, описанные на LTL, должны быть инвариантны к прореживанию.

Это означает, что именно так (инвариантно к прореживанию) нужно интерпретировать словесную формулировку свойств.

В частности, "P истинно один раз" в формулировке, инвариантной к прореживанию, означает, что в трассе есть один неразрывный участок, на котором истинно P.

С уважением, Константин Савенков.