Я не очень понял...

[thesz]

...в чем там проблема, но есть отличная книга "Верификация моделей программ". Там про разные варианты рассказывается.

Если я всё правильно помню (а книга запихнута довольно далеко), то можно поменять темпоральную логику и взять её вариант попроще. Соответственно, сложность упадёт.

Comments

[mpd]

И всё же, сложность. Абстрактная?
"Скока вешать граммов?"

[thesz]

Там 2^O(N), всё равно. Из-за поиска решения через выполнимость булевских формул. Однако, современные решатели умеют решать это всё за достаточно быстрое время. Миллионы высказываний и миллионы переменных могут быть обработаны в течении часов.

[nponeccop]

Надо в первоисточник глядеть. А на него даже ссылки нет. И двойная экспонента записана, используя синтаксис произведения, так что если понимать пост буквально, получается какая-то ржака O(5) vs O(25). Имели ввиду явно не это, но что - из топика непонятно.

Upd: даже скобки неправильно раставлены, в результате 2*2*O(N) вместо O(2**(2**n)), какая-то путаница температуры кипения воды с прямым углом. Отказать.

[thesz]

Двойные звёздочки сожрал Juick, сделав срединную двойку жирной.

И да, надо писать 2^O(N), ибо тут вопрос в логарифме (то есть, множителе). А то O(2^N) означает всего лишь c*2^N, где c > 0. Выбор же алгоритма перебора меняет основание экспоненты.

[nponeccop]

Cмена основания экспоненты эквивалентна умножению на константу. (a * 2)^N = a ^ N * 2 ^ N.

[thesz]

Это занудство с моей стороны, но: возьмите определение О-нотации и попробуйте вывести ваше преобразование.

http://en.wikipedia.org/wiki/Big_O_notation

Оно неправильно.

[dmzlj]

сложность-то упадёт, с одной стороны. с другой стороны, пока рассмотрен только статический случай (и сеть, определённая как множества коммутаторов, и правила маршрутизации --- статические).

т.е модель можно еще упростить, но вопрос, не потеряется ли тогда практичность.