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