Как интерпретировать результат msat LTL команды NuXMV

Question

Я использую NuXMV для проверки свойств LTL с помощью команды msat_check_ltlspec_bmc на довольно большой модели. В результате не найдено контрпримеров в заданных пределах. Должен ли я интерпретировать это как истинное свойство? Или это может означать, что анализ не завершен.

Это потому, что, изменяя предложение свойства на true или false, результат всегда не является контрпримером. Большинство результатов являются нелогичными.

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

Answer 1

Проверка ограниченной модели - это метод, ориентированный на ошибки, который проверяет действительность свойства по трассам выполнения до заданной длины k.

• Когда трассировка выполнения нарушает свойство, замечательно: обнаружена ошибка.

• В противном случае (в общем случае) результат проверки модели не дает полезной информации, и его следует рассматривать как таковой.

В некоторых случаях может помочь знание дополнительной информации о модели. В частности, если известно, что каждый след выполнения длиной k должен возвращаться к одному из состояний k-1, то можно сделать более убедительные выводы из-за отсутствия контрпримеров длины, меньшей или равной k.