Обход неизвестного графа коллективом автоматов. Недетерминированный случай

Исследование графов автоматами является корневой задачей во многих приложениях. К таким приложениям относятся верификация и тестирование программных и аппаратных систем, а также исследование сетей, в том числе сети интернета и GRID на основе формальных моделей. Модель системы или сети, в конечном счёте, сводится к ориентированному графу переходов, свойства которого нужно исследовать. За последние годы размер реально используемых систем и сетей и, следовательно, размер их графовых моделей непрерывно растёт. Проблемы возникают тогда, когда исследование графа одним автоматом (компьютером) либо требует недопустимо большого времени, либо граф не помещается в памяти одного компьютера, либо и то и другое. Поэтому возникает задача параллельного и распределённого исследования графов. Эта задача формализуется как задача исследования графа коллективом автоматов. В основе такого исследования лежит обход графа (проход по всем его дугам, достижимым из начальной вершины). Автоматы могут генерироваться в начальной вершине графа, перемещаться по дугам графа в направлении их ориентации и обмениваться между собой сообщениями через независимую (от графа) сеть связи. Суммарная память автоматов используется для хранения описания пройденной части графа. Для перемещения из вершины по выходящей из неё дуге графа автомат каким-то образом должен идентифицировать эту дугу: указать её номер. В нашей статье «Обход неизвестного графа коллективом автоматов» предложен алгоритм такого обхода для случая детерминированных графов. Задача усложняется, если граф недетерминирован. В таком графе одному номеру дуги соответствует, вообще говоря, несколько дуг, из которых для перехода выбирается одна дуга недетерминированным образом. Для того, чтобы обход графа был возможен, должна быть гарантия, что при неограниченном числе экспериментов каждая выходящая из вершины дуга с данным номером может быть пройдена. Такой недетерминизм мы называем справедливым. Решению задачи обхода справедливо недетерминированных графов посвящена данная работа.