Настоящая статья посвящена развитию методики формальной проверки правильности взаимодействия агентов, моделирующих сетевое взаимодействие. Поведение агентов специфицируется на языке процессных выражений. Взаимодействующие агенты широко применяются для моделирования сетевых взаимодействий, использующих различные протоколы. Автоматизацию проверки правильности спецификаций предлагается осуществлять логическими программами, получаемыми с помощью представленной в настоящей статье методики перехода от канонических процессных выражений, специфицирующих поведение агентов, а также требований правильности взаимодействия на языке модальной логики.