Дорогие студенты,
Обращаю внимание, что в тексте 4 задания сказано, что свойства,
описанные на LTL, должны быть инвариантны к прореживанию.
Это означает, что именно так (инвариантно к прореживанию) нужно
интерпретировать словесную формулировку свойств.
В частности, "P истинно один раз" в формулировке, инвариантной к
прореживанию, означает, что в трассе есть один неразрывный участок, на
котором истинно P.
С уважением,
Константин Савенков.