К синтезу адаптивных проверяющих последовательностей для недетерминированных автоматов

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