Метод доказательства наблюдаемой эквивалентности процессов с передачей сообщений

Рассматривается проблема доказательства наблюдаемой эквивалентности для класса вычислительных процессов, называемых процессами с передачей сообщений. Действия, выполняемые такими процессами, заключаются в посылке или приеме сообщений, проверке логических условий и обновлении значений внутренних переменных процессов. Основным результатом статьи является теорема, сводящая задачу доказательства наблюдаемой эквивалентности пары процессов с передачей сообщений к задаче нахождения формул, ассоциированных с парами состояний этих процессов, удовлетворяющих некоторым условиям, которые связаны с переходами этих процессов. Данное сведение является обобщением известного метода Флойда верификации блок-схем, в котором задача верификации блок-схемы сводится к задаче нахождения формул (называемых промежуточными утверждениями), связанных с некоторыми точками в блок-схемах и удовлетворяющих некоторым условиям, соответствующим переходам в блок-схемах. Изложенный метод доказательства наблюдаемой эквивалентности процессов с передачей сообщений иллюстрируется примером верификации протокола скользящего окна.