Аннотация:http://www.mathnet.ru/links/c95f6e4b51c45ca3e29928b88ac80ba2/ia311.pdf
Рассматривается проблема доказательства наблюдаемой эквивалентности для класса вычислительных процессов, называемых процессами с передачей сообщений. Действия, выполняемые такими процессами, заключаются в посылке или приеме сообщений, проверке логических условий и обновлении значений внутренних переменных процессов. Основным результатом статьи является теорема, сводящая задачу доказательства наблюдаемой эквивалентности пары процессов с передачей сообщений к задаче нахождения формул, ассоциированных с парами состояний этих процессов, удовлетворяющих некоторым условиям, которые связаны с переходами этих процессов. Данное сведение является обобщением известного метода Флойда верификации блок-схем, в котором задача верификации блок-схемы сводится к задаче нахождения формул (называемых промежуточными утверждениями), связанных с некоторыми точками в блок-схемах и удовлетворяющих некоторым условиям, соответствующим переходам в блок-схемах. Изложенный метод доказательства наблюдаемой эквивалентности процессов с передачей сообщений иллюстрируется примером верификации протокола скользящего окна.