Архив выступлений: 2015-2016 учебный год, весенний семестр

И. Б. Бурдонов, А. С. Косачев (ИСП РАН).
«Исследование ориентированного графа коллективом двигающихся автоматов».

Аннотация доклада.

Исследование графов автоматами является корневой задачей во многих приложениях. К таким приложениям относятся верификация и тестирование программных и аппаратных систем, а также исследование сетей, в том числе сети интернета и GRID на основе формальных моделей. Модель системы или сети, в конечном счёте, сводится к графу переходов, свойства которого нужно исследовать. За последние годы размер реально используемых систем и сетей и, следовательно, размер их моделей и, следовательно, размер исследуемых графов непрерывно растёт. Проблемы возникают тогда, когда исследование графа одним автоматом (компьютером) либо требует недопустимо большого времени, либо граф не помещается в памяти одного компьютера, либо и то, и другое. Поэтому возникает задача параллельного и распределённого исследования графов. Эта задача формализуется как задача исследования графа коллективом автоматов (несколькими параллельно работающими компьютерами с достаточной суммарной памятью).

Предлагается алгоритм обхода заранее неизвестного ориентированного графа неограниченной группой параллельно работающих конечных автоматов, перемещающихся по дугам графа и взаимодействующих друг другом с помощью обмена сообщениями. Работа начинается с одного автомата в начальной вершине графа. Автомат, находящийся в некоторой вершине графа, может 1) генерировать другой автомат в той же вершине графа, 2) перемещаться по дуге, выходящей из этой вершины, 3) послать сообщение другому автомату по его адресу. Время работы описываемого алгоритма в худшем случае ограничено O(m+nd), где n — число вершин графа, m — число его дуг, d — диаметр графа, представленная оценка достигается на некотором семействе графов.

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