Выполнена автоматизация проверки правильности спецификаций протоколов инициирования сеансов как мультиагентной системы, представляемой про- цессными моделями и описанием требований их правильности на языке вре- менной модальной логики. Автоматизацию проверки правильности специфи- каций предложено осуществлять логическими программами, получаемыми с помощью предлагаемой методики перехода от процессной модели описания спецификации и требований правильности на языке модальной логики к ло- гической программе проверки правильности на языке логического программи- рования ПРОЛОГ. Развиты принципы перехода от процессных моделей SIP- спецификаций к логической программе до детальной методики получения всех необходимых разделов логической программы. Методика проиллюстрирована примером логической программы для случая двух взаимодействующих агентов: пользовательского и сервисного.