ИСТИНА

Цель проекта – провести исследование и получить решение серии задач, связанных с двумя фундаментальными проблемами и программирования – проблемы верификации программ и проблемы оптимизации программ. Исследования планируется проводить на разнообразных моделях вычислений, используемых в качестве формальных моделей вычислительных систем – схемах программ и автоматах различных видов, - по следующим шести смежным направлениям, направленным на получение следующих основных результатов:

InThe aim of the project is to to study and find solutions to a series of problems related to two fundamental problems of system programming - program verification and program optimization. The research is planned to be carried out on a variety of computational models used as formal models of computer systems - program schemes and automata of various types by following six related lines, aimed at obtaining the main results listed below: 1. Development of efficient algorithms for minimization of first-order formal models of programs w.r.t. strong (logic&term) equivalence relation; 2. Development of equivalence checking algorithms for combined equivalence of first-order formal models of programs; 3. Development of equivalence checking algorithms for sequential reactive programs modelled by finite transducers operating over semigroups; 4. Development of efficient algorithms for minimization of timed automata used as models of real-time computing systems; 5. Development of model checking algorithms for sequential reactive programs modelled by finite transducers against parameterized variants of temporal logics; 6) Development of efficient algorithms for checking testing-equivalence of processes of spi-calculus used for modelling cryptographic protocols.

В 2020 году было запланирована работа по следующим направлениям. 1. Исследование проблемы эквивалентности конечных детерминированных биавтоматов и детерминированных линейных контекстно-свободных грамматик (В.А. Захаров). 2. Исследование проблемы эквивалентности детерминированных конечных 3-ленточных автоматов (В.А. Захаров). 3. Исследование проблемы логико-термальной эквивалентности стандартных схем программ с дополнительными аксиомами, описывающими алгебраические свойства используемых в программах функциональных символов (операций) (В.А. Захаров). 4. Продолжение исследования задачи минимизации слабо недетерминированных автоматов-преобразователей и стандартных схем программ (относительно логико-термальной эквивалентности) (В.А. Захаров). 5. Продолжение исследования задачи динамической верификации трасс выполнения систем реального времени относительно спецификаций, задаваемых формулами темпоральных логик реального времени (Подымов В.В., Куцак Н.Ю.). 6. Исследование задачи верификации конечных автоматов-преобразователей относительно спецификаций, представленных формулами темпоральной логики Reg-CTL* (Гнатенко А.Р.). 7. Исследование задачи верификации конечных автоматов-преобразователей, работающих над полугруппами специального вида, в которых правила действия операции композиции заданы с помощью систем уравнений над термами, позволяющими учитывать, что возможность получения одинаковых результатов разными последовательностями действий реагирующей системы (А.Р. Гнатенко). 8. Исследование задачи проверки выполнимости формул темпоральной логики LP-RLTL для некоторых классов автоматов-преобразователей реального времени (Е.М. Винарский).

Участниками проекта были получены некоторые результаты, которые свидетельствуют возможности решения поставленных в проекте задач и об осуществимости предлагаемого плана исследований. 1). При изучении задачи-проверки логико-термальной эквивалентности был разработан новый алгебраический подход к решению задач анализа программ, связанных с логико-термальной эквивалентностью. Есть основания полагать, что этот подход вкупе с методами теории схем программ, применяемыми для разрешения эквивалентности и эквивалентных преобразований схем Ляпунова-Янова и стандартных схем программ может быть успешно применен для решения задачи проверки комбинированной эквивалентности схем программ. 2) При изучении задачи минимизации автоматов и схем программ были разработаны новые методы решения задачи минимизации схем программ и автоматов, семантика которых определяется на основе полугрупп. Были установлены также условия применения предложенных методов. Мы полагаем, что область применения этих методов может быть расширена, и на их основе можно получить решения задач минимизации конечных автоматов-преобразователей, стандартных схем программ с логико-термальной и комбинированной эквивалентностью, а также некоторых классов автоматов с таймерами (т.н. временных автоматов (timed automata)). 3) Были получены некоторые предварительные результаты исследования задачи верификации автоматов-преобразователей над полугруппами относительно требований правильности поведения, выраженными при помощи формул новой разновидности темпоральной логики линейного времени. 4) В ранних исследованиях задачи верификации процессов spi-исчисления был намечен новый подход к решению этой задачи за счет использования графовых структур для представления сведений противника. Дальнейшие работы в этом направлении были прерваны, и в нашем проекте мы рассчитываем развить те новые идеи, которые были обозначены в указанной работе.

По каждому из заявленных направлений исследований были получены следующие основные результаты. 1. Исследована задача минимизации конечных автоматов-преобразователей, работающих над полугруппой регулярных префиксных языков. Доказано, что в полугруппе регулярных префиксных языков можно ввести отношение частичного порядка, относительно которого данная полугруппа образует решетку, удовлетворяющую свойству обрыва убывающих цепей. Доказано, что полугруппа регулярных префиксных языков обладает свойством левой сократимости. На основании этих свойств построен полиномиальный по времени алгоритм минимизации конечных автоматов-преобразователей, работающих над полугруппой регулярных префиксных языков. Предложенный алгоритм минимизации конечных автоматов-преобразователей, работающих над полугруппой регулярных префиксных языков, позволяет решить задачу минимизации для одного класса стандартных (первопорядковых) схем программ относительно логико-термальной эквивалентности. Показано, что для схем программ из выделенного семейства в каждом классе логико-термальной эквивалентности имеется единственная (с точностью до изоморфизма) минимальная схема программ с приведенными линейными участками. Результаты исследования задач проверки эквивалентности и минимизации автоматов–преобразователей были представлены на конференции «Дискретные модели в теории управляющих систем», опубликованы в сборнике трудов конференции [21], и подготовлены для публикации в журнале «Моделирование и анализ информационных систем». 2. Проблема эквивалентности также была исследована для одного класса недетерминированных автоматов-преобразователей, работающих с однобуквенным выходным алфавитом. В общем случае даже для однобуквенного выходного алфавита эта задача является алгоритмически неразрешимой. Мы рассмотрели класс недетерминированных автоматов-преобразователей, которые в любом состоянии для каждого входного символа могут записывать на выходной ленте разные слова, но при этом совершают переход в одно и то же состояние. Было установлено, что для указанного класса автоматов-преобразователей проблема эквивалентности разрешима. Решение этой задачи было получено путем описания поведения автоматов из рассматриваемого класса формулами арифметики Пресбургера и использованием разрешающего алгоритма проверки выполнимости формул этой арифметики. Ранее такой подход для решения проблемы эквивалентности автоматов-преобразователей никем не использовался. Результаты исследования задач проверки эквивалентности и минимизации автоматов–преобразователей были представлены на конференции «Дискретная математика и ее приложения», опубликованы в сборнике трудов конференции [22]. 3. Был разработан общий метод построения быстрых алгоритмов проверки эквивалентности для некоторых классов автоматов (конечных преобразователей, двухленточных автоматов, биавтоматов, магазинных автоматов), которые демонстрируют определенные черты детерминированного или однозначное поведение. Этот новый метод сводит проверку эквивалентности автоматов к проверке разрешимости систем уравнений над полукольцами языков или бинарных отношений. Как оказалось, такую проверку достаточно просто провести методом исключения переменных, используя некоторые комбинаторные и алгебраические свойства регулярных префиксных языков. При помощи нового метода были получен следующие результаты: А). построен новый алгоритм проверки эквивалентности детерминированных конечных автоматов, имеющий сложность по времени O(n log n). Б). Выделен новый класс префиксных конечных автоматов-преобразователей и показано, что проверка эквивалентности автоматов из этого класса может быть осуществлена новым методом за время, квадратичное (для префиксных автоматов-преобразователей реального времени) и кубическое (для префиксных автоматов-преобразователей с epsilon-переходами) относительно размеров анализируемых автоматов. В). Показано, что проблема эквивалентности для детерминированных двухленточных конечных автоматов сводится к задаче проверки эквивалентности префиксных конечных автоматов-преобразователей и может быть решена за время, кубическое относительно их размеров. Г). Показано, что проблема эквивалентности для детерминированных многоленточных автоматов, в которых алфавиты всех лент, за исключением одной, являются унарными, сводится к задаче проверки эквивалентности детерминированных автоматов-преобразователей, работающих над коммутативными полугруппами, и может быть решена за время, кубическое относительно размеров анализируемых автоматов. Д). Аналогичным образом установлена разрешимость проблемы эквивалентности для детерминированных конечных биавтоматов за время, кубическое относительно их размеров. Е). При помощи нового метода построен алгоритм проверки эквивалентности для простых грамматик, соответствующих детерминированным магазинным автоматам с одним состоянием. Эти результаты исследований были представлены на ряде конференций, опубликованы в сборнике трудов конференций [23-26], и в журнале «Моделирование и анализ информационных систем» [27]. 4. Нами была исследована проблема эквивалентности для схем программ с процедурами в перегородчатой модели пропозициональных схем программ. Эта модель была ранее введена в работах Р.И. Подловченко. Программа в этой модели представляет собой совокупность графов, каждым из которых описывается устройство одной процедуры программы: порядок выполнения действий, преобразующих данные, вызовов процедур и возвратов из них. Для решения проблемы эквивалентности программ без процедур в широком классе моделей ранее был предложен и успешно применён подход, получивший название «метод совместных вычислений». Кроме того, известен результат, сводящий проблему эквивалентности программ с процедурами в перегородчатых моделях к двум проблемам для программ без процедур в той же модели: проблеме эквивалентности и не исследованной ранее проблеме совместного останова (завершения вычислений). Последняя проблема формулируется так: проверить, задается ли моделью хотя бы одна семантика, в которой вычисления обеих программ конечны. Нами был предложен подход к решению проблемы совместного останова, обосновывающий разрешимость и полиномиальную разрешимость этой проблемы в обширном семействе моделей, законы преобразования данных имеют полугрупповую природу. Предложенный подход представляет собой метод совместных вычислений, предлагавшийся ранее только для решения проблемы эквивалентности и адаптированный для решения новой проблемы. Из полученного результата и известных результатов, упомянутых выше, следует разрешимость и полиномиальная разрешимость проблемы эквивалентности программ с процедурами в обширном семействе перегородчатых моделей полугрупповой природы. Результаты, полученные при решении этой задачи, были опубликованы в журнале «Вестник Московского университета» [36,38]. 5. Были исследованы свойства вычислений конечных автоматов, работающих в реальном времени (Timed Finite State Machines, TFSM). Для моделирования течения времени конечный автомат дополнен специальной вещественной переменной (таймером). В расширенной модели входные и выходные символы сопровождаются пометками времени и, кроме того, каждый переход помечен допустимым временным интервалом (период активности перехода) и выходной задержкой (время, необходимое для обработки поступившего входного символа и выдачи соответствующего выходного символа). Соответственно, входное временное слово активирует последовательность переходов, если время прихода символа принадлежит допустимому интервалу. Отличительной особенностью рассматриваемой нами модели TFSM является то, что порядок, в котором в выходном слове располагаются выходные символы, зависит не только от порядка поступления входных символов, но и от времени, необходимого для их обработки (выходной задержки). В такой модели, при выполнении одной и той же последовательности переходов, выходные символы могут располагаться в выходном слове в разном порядке их следования. Порядок зависит ещё и от того, в какие моменты времени соответствующие входные символы поступали на вход TFSM. В модели TFSM, как и в модели конечного автомата, большинство задач могут быть эффективно решены только в детерминированном случае, поэтому мы начали исследование с моделей, поведение которых детерминировано. TFSM была названа строго детерминированной, если для любой последовательности переходов и для любого входного временного слова, активирующего эту последовательность переходов, порядок следования выходных символов в выходном слове будет определён однозначно. Нами была исследована задача проверки свойства строгой детерминированности для произвольных заданных TFSM. В результате проведенных исследований были получены следующие основные результаты. А). Сформулирован и обоснован критерий строго детерминированного поведения последовательности переходов конечной длины в TFSM, т.е. условие, при котором для любого входного временного слова, активирующего последовательность переходов, порядок следования выходных символов в выходном временном слове не изменяется. Б). Установлены необходимые и достаточные условия строгой детерминированности TFSM, работающих в реальном времени. В). Доказано, что в общем случае задача проверки строго детерминированного поведения TFSM является co-NP-трудной. Для доказательства мы предложили алгоритм, который за полиномиальное время сводит задачу о сумме подмножеств к задаче поиска последовательности переходов, на которой нарушается строго детерминированное поведение проверяемого автомата. Результаты исследования задачи проверки строгой детерминированности TFSM были представлены на конференциях SYRCoSE (Spring/Summer Young Researchers' Colloquium on Software Engineering) и «Дискретные модели в теории управляющих систем», опубликованы в сборнике трудов конференций [3], а также в журнале «Труды Института системного программирования» [4]. 6. В проекте также проводилось изучение задачи верификации систем реального времени, которые моделируются TFSM. Целью исследований являлась задача проверки выполнимости некоторых поведенческих свойств конечных автоматов-преобразователей реального времени, зависящих не только от последовательности входных сигналов, но и от времени их поступления и времени, требующегося на обработку входных сигналов. Вначале было предложено новое альтернативное определение вычислений TFSM с использованием размеченных систем переходов и показано, что два разных определения семантики для рассматриваемого класса TFSM хорошо взаимосвязаны друг с другом. Использование семантики TFSM, основанной на размеченных системах переходов, открывает возможность применения ранее известных методов верификации систем вычислений реального времени для анализа поведения последовательных реагирующих систем. Для спецификации поведения таких систем была разработана новая темпоральная логика LP-RLTL, которая является расширением темпоральной логики линейного времени LTL. Введенной логика имеет две отличительные особенности: a) темпоральные операторы параметризованы регулярными языками над конечным алфавитом входных сигналов с пометками значений реального времени, и б) каждый атомарный предикат является регулярным языком над конечным алфавитом выходных сигналов с пометками значений реального времени. Семантика формул введенной темпоральной логики определяется при помощи отношения выполнимости над парами бесконечных последовательностей входных и выходных сигналов с пометками значений реального времени. В результате проведенных исследований были решены следующие задачи. А). Для описания регулярных языков параметризации, используемых в формулах логики LP-RLTL были введены временные автоматы-распознаватели и показано, что класс языков, распознаваемых этими автоматами, замкнут относительно операций объединения, пересечения, итерации и дополнения. Данный результат был получен при помощи моделирования поведения временного автомата при помощи специальной унифицированной формы (конечно-автоматная абстракция). Б). Разработан алгоритм проверки выполнимости формулы LP-RLTL логики для случая, когда TFSM обладает свойством консервативности: задержки генерации выходных сигналов таковы, в каждом вычислении автомата порядок следования во времени выходных сигналов соответствует порядку следования во времени входных сигналов. Доказана корректность предложенного алгоритма и получена экспоненциальная верхняя оценка времени работы предложенного алгоритма. Результаты проведенных исследований задачи верификации TFSM были представлены на ряде конференций и опубликованы в сборниках трудов конференций [5-7], а также в журнале «Моделирование и анализ информационных систем» [8]. 7. В нашем проекте исследовалась задача также трансляции иерархических временных автоматов (ИВА) в эквивалентные сети временных автоматов (СВА) с как можно меньшим числом состояний. Модели СВА и ИВА используются для формальной верификации распределённых систем реального времени (СРВ), то есть систем параллельно работающих взаимодействующих компонентов, выполнение которых существенно зависит не только от порядка возникновения событий в системе, но и от реального времени возникновения этих событий. Модель СВА проста для понимания и выразительна, и потому популярна в сфере верификации СРВ. Основным недостатоком модели СВА является отсутствие средств описания иерархии компонентов СРВ: описания одних компонентов СРВ как составных частей других, более сложных, компонентов. Нами была предложена вариация понятия ИВА, более компактная и при этом не менее выразительная по сравнению с существующими, а также понятие эквивалентности ИВА и СВА, схожее с одним из видов бисимуляционной эквивалентности конечных систем переходов, сохраняющей выполнимость требований, выражаемых широким классом формул темпоральных логик. На основании новой модели ИВА и сопутствующего ей отношения бисимуляционной эквивалентности был разработан алгоритм уплощения ИВА, позволяющий получать СВА с числом состояний, меньшим по порядку по сравнению с СВА, получаемыми в результате работы известных аналогичных алгоритмов. Результаты исследования задачи трансляции иерархических временных автоматов были представлены на конференции «Дискретные модели в теории управляющих систем», опубликованы в сборнике трудов конференции и в сборнике статей «Прикладная математика и информатика» [34,35,37]. 8). Еще одна задача анализа поведения систем реального времени, которая была исследована в данном проекте, - это задача обнаружения эффекта гонок при загрузке правил маршрутизации в таблицы коммутаторов программно-конфигурируемых сетей (ПКС). Эффект гонок проявляется при взаимодействии трех основных компонентов ПКС – прикладной программы, контроллера и коммутатора. При реконфигурации ПКС приложение при посредстве контроллера устанавливает правила коммутации пакетов в таблицы коммутаторов. Результат применения этих правил существенно зависит от того порядка, в котором правила коммутации были установлены в таблицах коммутаторов. Однако в силу некоторой неопределенности с задержкой доставки правил коммутации по каналам связи (имеющей физическую природу) не всегда инструкции приходят в том же самом порядке, в котором их установка была заказана приложением. Таким образом, возникают гонки как в компонентах ПКС, так и в каналах, связывающих эти компоненты. При изучении этой задачи участниками проекта была проведена классификация гонок и были построены формальные математические модели в виде обобщенных конечных автоматов для компонентов ПКС. На основе введенных моделей были предложены спецификации, описывающие требования нечувствительности систем к гонкам той или иной разновидности, представленные в виде LTL-формул, а также метод порождения специальных последовательностей тестовых запросов, провоцирующих гонки в ПКС и оценена вероятность того, что найденная тестовая последовательность провоцирует гонку в случае, когда в качестве контроллера используется ONOS Controller. Проведенные эксперименты подтвердили, что ONOS Controller чувствителен как к входо-выходные гонки гонкам, так и к внутриканальным гонкам. Для генерации тестов с гарантированной полнотой при помощи конечно-автоматных методов сильно усложняется с увеличением размеров тестируемой системы. В то же время методы формальной верификации позволяют эффективно обрабатывать достаточно большие системы переходов, в частности, SMT-решатели широко используются для решения задач анализа систем с конечным числом переходов. Одним из участников данного проекта было проведено описание известных необходимых и достаточных условий полноты тестовых наборов, полученных конечно-автоматными методами тестирования с помощью логических формул первого порядка, и с использованием SMT-решатель z3 для их проверки. Результаты компьютерных экспериментов со случайно сгенерированными конечными автоматами подтвердили правильность и эффективность предложенного подхода. Полученные результаты были представлены на конференциях Testing Software and Systems в 2019 и 2020 гг. и опубликованы в материалах этой конференции [9,33]. 9). В проекте было проведено исследование задачи динамической верификации трасс выполнения систем реального времени. Динамической верификацией (runtime verification) называется строгая проверка правильности выполнения вычислительной системы относительно заданных требований в том случае, если описание системы отсутствует и для анализа доступно только описание одного выполнения системы. Для систем реального времени таким описанием нередко является набор сигналов: отображений действительных чисел в логические значения, описывающих изменение свойств состояния системы с течением времени. Важным примером системы реального времени с наиболее естественным использованием понятия сигнала является цифровая микроэлектронная схема (далее – просто схема) – ключевой управляющий компонент любой нетривиальной современной вычислительной цифровой аппаратуры. Для записи требований, учитывающих взаимосвязь свойств состояний системы в разные моменты времени, довольно естественно применение формальных языков темпоральных логик, как правило (в большинстве практических случаев) являющихся логиками либо дискретного, либо реального времени. Логики дискретного времени предназначены для задания свойств пошаговых выполнений систем, и течение времени в них представляет собой дискретный целочисленный отсчёт. Логики реального времени предназначены для задания свойств непрерывно выполняющихся систем, и течение времени в этих логиках представляет собой непрерывное увеличение действительного значения текущего момента времени. Нами предложена логика реального времени, предназначенная для динамической верификации схем на ранних этапах разработки и названная сигнальной. В базовых определениях языка сигнальной логики учтены как общие особенности языков темпоральных логик, так и некоторые важные особенности сигналов схем на уровнях абстракции, соответствующих ранним этапам разработки: выполнение в конечном отрезке реального времени, наличие неопределённого (неизвестного) значения наряду с обычными булевыми (0 и 1) и наличие мгновенных фронтов сигналов (точек изменения значения). Также предложены варианты сигнальной логики с расширенным и с укороченным наборами операций. В расширенный набор включены основные операции, характерные для темпоральных логик. Из укороченного набора исключены, в числе прочего, все операции, предназначенные для естественной записи свойств цифровых сигналов схем и нехарактерные для темпоральных логик. Доказано, что исходный, расширенный и укороченный варианты языка одинаково выразительны, что позволяет упростить как запись конкретных свойств, так и дальнейший теоретический анализ языка. Для сигнальной логики нами строго поставлена задача динамической верификации: проверки выполнимости формулы на заданной диаграмме сигналов, описывающей выполнение (прогон) схемы. Разработан алгоритм решения этой задачи, основанный на особой алгебраической трактовке формул. Доказаны корректность и невысокая оценка сложности алгоритма — полином небольшой степени по числу элементарных арифметических операций. Полученные результаты были представлены на ряде конференций, опубликованы в материалах этой конференции [28,29,31,39], а также в журнале «Моделирование и анализ информационных систем» и «Automatic Control and Computer Sciences» [30]. 10. Одним из направлений исследований в этом проекте была задача верификации последовательных реагирующих систем, моделируемых конечными автоматами-преобразователями над свободной полугруппой. Для спецификации поведения системы был разработан формальный язык Reg-CTL*, основанный на темпоральной логике. Этот логический язык обладает возможностью выражать отношения между множествами слов входного алфавита и множествами слов выходного алфавита. Для введенного языка Reg-CTL* и его подсемейств Reg-LTL и Reg- CTL были исследованы две задачи: сравнение выразительных возможностей новых расширений темпоральных логик с другими логическими языками и разработка алгоритмов верификации моделей конечных автоматов-преобразователей относительно спецификаций правильного поведения, выраженных формулами Reg-CTL*. При решении этих задач были получены следующие результаты. А). Было рассмотрено параметризованное расширение LP–LTL темпоральной логики линейного времени, в котором выделено два фрагмента и проведено сравнение выразительные возможности этих фрагментов с логиками линейного времени LTL и монадической логикой второго порядка с одной функцией следования S1S. Формулы первого из этих фрагментов LP-1-LTL строятся над однобуквенным алфавитом входных сигналов и произвольным конечным алфавитом элементарных действий. В качестве семейства шаблонов поведения окружения в формулах этого фрагмента разрешается использовать любые регулярные языки над алфавитом входных сигналов, а в качестве семейства базовых предикатов будем использовать семейство регулярных языков специального вида (языков, состоящих из всех возможных слов, оканчивающихся одной и той же заданной буквой). Второй фрагмент LP-n-LTL определяется аналогично, с той лишь разницей, что алфавиты входных сигналов и выходных действий совпадают. Было доказано, что а). темпоральная логика линейного времени LTL строго менее выразительна, чем фрагмент LP-1-LTL; доказательство этого утверждения проводилось с привлечением игры Эренфойхта-Фреше; б). монадическая логика второго порядка с одной функцией следования S1S и фрагмент LP-n-LTL имеют одинаковую выразительную способность: моделями формул этих логик являются все регулярные языки сверхслов, допускаемые автоматами Бюхи. Б) Был разработан алгоритм и изучена сложность задачи верификации моделей автоматов-преобразователей дискретного времени относительно спецификаций их поведения, выраженных формулами логики ветвящегося времени Reg-CTL, являющейся расширением логики деревьев вычислений CTL. Было доказано, что эта задача является PSPACE-полной. В). Был разработан алгоритм и изучена сложность задачи верификации моделей автоматов-преобразователей дискретного времени относительно спецификаций их поведения, выраженных формулами темпоральной логики Reg-CTL*, являющейся расширением логики деревьев вычислений CTL*. Было установлено, что эта задача принадлежит классу сложности EXPSPACE. Полученные результаты исследований были представлены на нескольких конференциях, опубликованы в трудах этих конференций [10-12,15,16,18,19], а также в журналах «Моделирование и анализ информационных систем», «Труды института системного программирования» и «Automatic Control and Computer Sciences» [13,14,17,20]. 11. Была исследована задача проверки информационной безопасности протоколов, описанных при помощи базовых средств исчисления мобильных процессов (пи-исчисления). Для ее решения было предложено расширение исчисления мобильных процессов, позволяющее добавлять к моделям протоколов мониторинги – процессы специального вида, воспроизводящие возможности вычислений пассивного противника, способного лишь перехватывать сообщения. Сформулировано требование стойкости (информационной безопасности протоколов относительно атак и угроз в модели пассивного противника. Показано, что задача проверки требования информационной безопасности протоколов в модели пассивного противника является co-NP-полной. Для доказательства этого утверждения было показано, каким образом для каждой 3-КНФ можно построить процесс пи-исчисления и сформулировать угрозу так, чтобы вопрос о выполнимости 3-КНФ оказался равносилен вопросу о стойкости построенного процесс пи-исчисления относительно заданной угрозы в модели пассивного противника. Мы также предприняли попытку дальнейшего развития предложенной ранее модели противника путем добавления новых возможностей, позволяющих противнику вступать в диалог с наблюдаемыми процессами. Были также предложены две модели активного противника, отличающиеся возможностями противника генерировать сообщения для передачи их наблюдаемым процессам. Отличительная особенность этих моделей состоит в том, что противник может быть представлен в виде отдельного процесса spi-исчисления, действия которого включают специальные примитивы конструирования сообщений при помощи термов, которые могут быть перехвачены за счет взаимодействия с процессами анализируемого протокола. Для обоих моделей было показано, что задача проверки свойства стойкости телекоммуникационного протокола (относительного заданных множеств имен, составляющих исходные знания противника и его цель) является co-NP-полной. Полученные результаты были опубликованы в журналах «Моделирование и анализ информационных систем» и «Automatic Control and Computer Sciences» [1,2]. 1. Аббас М.М., Захаров В. А. Даже простые процессы pi-исчисления трудны для анализа // Моделирование и анализ информационных систем. — 2018. — Т. 25, № 6. — С. 589–606 2. Abbas M. M., Zakharov V. A. Even simple pi-calculus processes are difficult to analyze // Automatic Control and Computer Sciences. - 2019. - Vol. 53, no. 7. - P. 589–606. 3. Винарский Е. М., Захаров В. А. О проверке детерминированности конечных автоматов с временными ограничениями // Дискретные модели в теории управляющих систем: Труды Х Международной конференции, Москва и Подмосковье, 23-25 мая 2018 г. Т. 1. — Москва: Москва, 2018. — С. 81–83. 4. Винарский Е. М., Захаров В. А. К проверке строго детерминированного поведения временных конечных автоматов // Труды Института системного программирования РАН. — 2018. — Т. 30, № 3. — С. 325–340. 5. Винарский Е. М., Захаров В. А. О задаче верификации для одного класса автоматов реального времен // Материалы XIII Международного семинара Дискретная математика и ее приложения имени академика О. Б. Лупанова (Москва, МГУ, 17–22 июня 2019 г.). - Изд-во механико-математического факультета МГУ, 2019. - С. 257–260. 6. Винарский Е. М. О свойствах временных автоматов / "Тихоновские чтения": научная конференция: тезисы докладов. - МаксПресс Москва, 2019. - С. 93-93. 7. Vinarskii E. M., Zakharov V. A. On some properties of timed finite state machines // Системная информатика. — 2020. — Vol. 17. — P. 11–20. 8. Винарский Е. М., Захаров В. А. О моделировании последовательных реагирующих систем при помощи автоматов, работающих в реальном времени // Моделирование и анализ информационных систем. — 2020. — Т. 27, № 4. — С. 396–411. 9. Vinarskii E., Laputenko A., Yevtushenko N. (2020) Using an SMT Solver for Checking the Completeness of FSM-Based Tests. In: Casola V., De Benedictis A., Rak M. (eds) Testing Software and Systems. ICTSS 2020. Lecture Notes in Computer Science, vol 12543. Springer, Cham 10. Gnatenko A., Zakharov V. On the model checking of finite state transducers over semigroups // Preliminary Proceedings of the 12 th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE 2018), — 2018. — P. 26–34 11. Gnatenko A., Zakharov V. On the expressive power of some extensions of linear temporal logic // Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018. — Ярославль: Ярославль, 2018. — P. 29–36. 12. Гнатенко А. Р., Захаров В. А. Языки спецификаций моделей Крипке на основе темпоральных логик и их выразительные возможности // Дискретные модели в теории управляющих систем: Труды Х Международной конференции, Москва и Подмосковье, 23-25 мая 2018 г. Т. 1. — Москва: Москва, 2018. — С. 131–133. 13. Гнатенко А. Р., Захаров В. А. О верификации конечных автоматов-преобразователей над полугруппами // Труды Института системного программирования РАН. — 2018. — Т. 30, № 3. — С. 303–324. 14. Гнатенко А. Р., Захаров В. А. О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. — 2018. — Т. 25, № 5. — С. 506–524. 15. Гнатенко А. Р., Захаров В. А. Верификация моделей реагирующих систем относительно одного расширения темпоральной логики CTL* // Материалы XIII Международного семинара Дискретная математика и ее приложения имени академика О. Б. Лупанова (Москва, МГУ, 17–22 июня 2019 г.). - Изд-во механико-математического факультета МГУ, 2019. - С. 263–266. 16. Гнатенко А. Р., Захаров В. А. О сложности верификации конечных автоматов-преобразователей над свободными полугруппами // "Тихоновские чтения": научная конференция: тезисы докладов. - МаксПресс Москва, 2019. - С. 91–91. 17. Gnatenko A. R., Zakharov V. A. On the expressive power of some extensions of linear temporal logic // Automatic Control and Computer Sciences. - 2019. - Vol. 53, no. 7. - P. 506–524 18. Gnatenko A. R. On the complexity of model checking problem for finite state transducers over free semigroups. European Summer School in Logic, Language and Information 2019 (ESSLLI 2019) Student Session Proceedings, 2019. 19. Gnatenko A. R., Zakharov V. A. Using an extension of CTL∗ for specification and verification of sequential reactive systems // Системная информатика. — 2020. — Vol. 17. — P. 21–32. 20. Гнатенко А. Р., Захаров В. А. О задаче верификации моделей программ для одного расширения логики CTL* // Моделирование и анализ информационных систем. — 2020. — Т. 27, № 4. — С. 428–441 21. Жайлауова Ш. Р., Захаров В. А. О минимизации конечных автоматов-преобразователей над полугруппой конечных префиксных языков // Дискретные модели в теории управляющих систем: Труды Х Международной конференции, Москва и Подмосковье, 23-25 мая 2018 г. Т. 1. — Москва: Москва, 2018. — С. 119–122. 22. Жайлауова Ш. Р., Захаров В. А. О проблеме эквивалентности недетерминированных автоматов-преобразователей над однобуквенным выходным алфавитов // Материалы XIII Международного семинара Дискретная математика и ее приложения имени академика О. Б. Лупанова (Москва, МГУ, 17–22 июня 2019 г.). - Изд-во механико-математического факультета МГУ, 2019. - С. 272–275. 23. Захаров В. А. Полиномиальный алгоритм проверки эквивалентности детерминированных двухленточных автоматов // Дискретные модели в теории управляющих систем: Труды Х Международной конференции, Москва и Подмосковье, 23-25 мая 2018 г. Т. 1. — Москва: Москва, 2018. — С. 128–130 24. Захаров В. А., Джусупекова З. А. Полиномиальный алгоритм проверки эквивалентности слабо недетерминированных конечных автоматов-преобразователей // Дискретные модели в теории управляющих систем: Труды Х Международной конференции, Москва и Подмосковье, 23-25 мая 2018 г. Т. 1. — Москва: Москва, 2018. — С. 134–136 25. Захаров В. А. О проверке эквивалентности детерминированных биавтоматов // "Тихоновские чтения": научная конференция: тезисы докладов. - МаксПресс Москва, 2019. - С. 94–94. 26. Zakharov V. A. Equivalence checking of prefix-free transducers and deterministic two-tape automata // Language and Automata Theory and Applications, 13th International Conference, LATA 2019, St. Petersburg, Russia, March 26-29, 2019, Proceedings. - Vol. 11417. Lecture Notes in Computer Science. - Springer Cham, Switzerland, 2019. - P. 146–158. 27. Захаров В. А. Эффективные алгоритмы проверки эквивалентности для некоторых классов автоматов // Моделирование и анализ информационных систем. — 2020. — Т. 27, № 3. — С. 260–303 28. Куцак Н. Ю., Подымов В. В. Алгебра троичных цифровых сигналов // "Тихоновские чтения": научная конференция: тезисы докладов. МаксПресс Москва, 2019. — С. 102–102. 29. Куцак Н. Ю., Подымов В. В. Алгебра троичных цифровых сигналов // "Тихоновские чтения": научная конференция: тезисы докладов. — МаксПресс Москва, 2019. — С. 102. 30. Куцак Н. Ю., Подымов В. В. Формальная верификация диаграмм троичных цифровых сигналов // Моделирование и анализ информационных систем. - 2019. - Т. 26, № 3. - С. 332–350. 31. Куцак Н. Ю., Подымов В. В. О выразимости операций логики троичных цифровых сигналов // Тихоновские чтения: научная конференция: тезисы докладов: посвящается памяти академика Андрея Николаевича Тихонова: 26 – 31 октября 2020 г. — Т. 1 из ТЕЗИСЫ ДОКЛАДОВ. — Москва: Москва, 2020. — С. 41–41. 32. Kutsak N. Y., Podymov V. V. Formal verification of three-valued digital waveforms // Automatic Control and Computer Sciences. — 2020. — Vol. 54, no. 7. — P. 630–644. 33. Lopez J., Kushik N., Vinarskij E., Yevtushenko N., Zighache D.. A model checking based approach for detecting sdn races // Lecture Notes in Computer Science. - 2019. - Vol. 11812. - P. 194-211. 34. Подымов В. В. Об уплощении иерархических временных автоматов // Дискретные модели в теории управляющих систем: Труды Х Международной конференции, Москва и Подмосковье, 23-25 мая 2018 г. Т. 1. — Москва: Москва, 2018. — С. 222–225. 35. Подымов В. В. Алгоритм уплощения иерархических временных автоматов // Прикладная математика и информатика. — Т. 59 из Труды факультета ВМК МГУ им. М.В. Ломоносова. — 2018. — С. 5–15. 36. Подымов В. В. Алгоритмы проверки эквивалентности программ с процедурами в прогрессивных полугрупповых перегородчатых моделях // Вестник Московского университета. Серия 15: Вычислительная математика и кибернетика. - 2019. - № 4. - С. 37–44. 37. Podymov V. V. A flattening algorithm for hierarchical timed automata // Computational Mathematics and Modeling. - 2019. - Vol. 30, no. 2. - P. 99–106. 38. Podymov V. V. Efficient equivalence-checking algorithms for procedural programs in progressive semigroup gateway models // Moscow University Computational Mathematics and Cybernetics. — 2019. - Vol. 43, no. 4. - P. 181–187. 39. Попков Г. А., Подымов В. В. Бисимуляционная эквивалентность систем переходов с реальным временем // Тихоновские чтения: научная конференция: тезисы докладов: посвящается памяти академика Андрея Николаевича Тихонова: 26 – 31 октября 2020 г. — Т. 1 — Москва: Москва, 2020. — С. 42.