Доказательство беступиковости

Докажем утверждение, что НОВПАНСИОН свободен от тупиков. Для этого достаточно доказать, что любой протокол s этой системы можно продолжить некоторым событием так, что бы снова получить протокол этой же системы. Строго, это можно сформулировать как

"s, $z (s протоколы(НОВПАНСИОН) AND z aНОВПАНСИОН

s^z протоколы(НОВПАНСИОН)).

Доказательство можно осуществлять двумя способами:

Первый из них предполагает применение (насколько это возможно) приведённых выше законов.

Второй способ доказательства состоит в составлении компьютерной программы для исследования протоколов системы в поисках тупика. Такая программ сможет дать интересующий нас ответ за конечное время, если система имеет конечное число состояний, как в нашем случаеНОВПАНСИОН. Достаточно рассмотреть только те протоколы, длина которых не превышает известной верхней границы числа состояний. (Каждому протоколу соответствует некоторое состояние системы, в которое систему приводит из начального состояния последовательность событий, описываемая этим протоколом.)

Число состояний в системе НОВПАНСИОН не превышает 1,8 млн. Но, т. к. в каждом состоянии возможны не меньше двух событий, то количество протоколов, которые надо проверить, будет превышать два в степени 1,8 млн. Трудно представить, что компьютер, когда-нибудь сумеет исследовать все возможные случаи. Таким образом, доказательство отсутствия тупиковых ситуаций, как правило, входит в обязанности разработчика параллельных систем.