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