Проверяющие эксперименты с ненаблюдаемым древовидными автоматами

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