ПРОГРАММИРОВАНИЕ, 2010, no 4, с. 40-50
ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ =
УДК 681.3.06
СИНТЕЗ РАЗЛИЧАЮЩИХ ЭКСПЕРИМЕНТОВ ДЛЯ ВРЕМЕННЫХ АВТОМАТОВ*
© 2010 г. М. Л. Громов, Н. В. Евтушенко
Томский государственный университет 634050 Томск, пр. Ленина, 36 E-mail: gromov@sibmail.com, ninayevtushenko@yahoo.com Поступила в редакцию 25.05.2009 г.
Статья посвящена построению различающих экспериментов с полностью определенными временными автоматами. Показывается, в частности, что два полностью определенных недетерминированных автомата различимы кратным безусловным экспериментом, если и только если эти автоматы не являются эквивалентными. Автоматы различимы простым условным экспериментом, если и только если эти автоматы r-различимы, то есть не имеют общей полностью определенной редукции. Соответствующий условный эксперимент описывается временным автоматом специального вида, и предлагается процедура построения такого r-различающего временного автомата.
1. ВВЕДЕНИЕ
Одной из современных проблем является проблема синтеза и анализа управляющих систем, работающих в режиме реального времени, таких, как различные контроллеры, элементы телекоммуникационных систем и другие. Формально, поведение таких систем можно описать на основе конечных полуавтоматов (см., например, [1-3]) и автоматов [4, 5]. Для осуществления контроля за функционированием системы требуется умение отличать исправную систему от неисправной или различать две неисправные системы. Такое распознавание можно провести посредством эксперимента с предъявленной системой [6]. Поскольку для конечных автоматов существует хорошо развитая теория таких экспериментов, и в ряде случаев поведение системы, описанное полуавтоматом, можно перевести в автоматное описание [7], мы в данной работе используем автоматное описание поведения системы, то есть множество действий системы разделено на непересекающиеся множества входных и выходных действий. Под действием входных
* Работа частично поддержанна проектом ФЦП (гос. контракт N 02.514.12.4002).
воздействий система переходит из состояния в состояние, выдавая при этом выходной сигнал. Мы рассматриваем временной автомат из работ [4, 5], который, кроме переходов, в каждом состоянии имеет определенную задержку. Если время ожидания входного воздействия превысит задержку в текущем состоянии, то временной автомат переходит в следующее состояние, в котором снова ожидает входное воздействие. В таком автомате можно выделить конечное множество временных интервалов, в которых система имеет одинаковое поведение [1], и, соответственно, по временному автомату можно построить конечный автомат, добавив к входным символам множество таких интервалов. Поэтому для временных автоматов сохраняются отношения совместимости и различимости, введенные в классической теории автоматов [6, 8]. Некоторые дополнительные отношения различимости между временными автоматами вводятся в работе [5], однако в этой работе не предлагаются методы построения соответствующих различающих последовательностей. В работах [2, 3] исследуется классическое отношение эквивалентности между временными полуавтоматами, когда эквивалентные полуавтоматы имеют одно и то же поведение, и предлагаются алгоритмы для постро-
ения соответствующих различающих последовательностей на основе предположения "о всех погодных условиях" [9].
В данной работе мы рассматриваем отношения различимости между временными автоматами, подобные отношениям для классических недетерминированных автоматов [8, 10]. Полностью определенные временные автоматы различимы, если существует временная входная последовательность, на которую множества реакций этих автоматов различны, то есть если эти автоматы имеют различное поведение. Один временной автомат не является редукцией другого, если существует временная входная последовательность, множество реакций на которую первого автомата не содержится в множестве реакций второго автомата, то есть поведение одного автомата не содержится в поведении другого автомата. Временные автоматы разделимы, если существует временная входная последовательность, множества реакций этих автоматов на которую не пересекаются, и автоматы г-различимы, если эти автоматы не имеют общей полностью определенной редукции, то есть не существует полностью определенного временного автомата, поведение которого содержится в поведении каждого из автоматов. В данной работе мы показываем, что проверку первых трех отношений можно осуществить безусловным экспериментом, причем эксперимент по проверке отношений различимости и редукции проводится при соблюдении предположения "о всех погодных условиях" [9]. Два разделимых временных автомата можно различить безусловным экспериментом без использования предположения "о всех погодных условиях". Два временных недетерминированных полностью определенных автомата можно различить посредством условного эксперимента, без использования предположения "о всех погодных условиях", если и только если эти автоматы г-различимы. Такой условный эксперимент можно представить посредством специального различающего автомата, алгоритм построения которого предлагается в данной работе. Все различающие эксперименты строятся на основе пересечения исходных временных автоматов. Оценки сложности таких экспериментов совпадают с таковыми для классических (не временных) автоматов.
Структура работы следующая. В разделе 2 вводятся основные определения. В разделе 3 вводится пересечение двух временных автоматов. В разделе 4 мы исследуем отношения различимости, "не быть редукцией", разделимости и г-различимости. В подразделе 4.3 показывается, каким образом условный эксперимент с временным автоматом можно описать с использованием различающего автомата, и устанавливается, что два временных недетерминированных полностью определенных наблюдаемых автомата можно различить посредством условного эксперимента, если и только если эти автоматы г-различимы. В этом же подразделе предлагается алгоритм построения различающего автомата.
2. ОСНОВНЫЕ ОПРЕДЕЛЕНИЯ И ОБОЗНАЧЕНИЯ
В данной работе мы используем понятие временного автомата из работы [4]. Как обычно, для представления временной зависимости используется специальная дискретная, так называемая временная, переменная (часы). Временной автомат содержит также специальную функцию, описывающую поведение системы при отсутствии на нее внешних воздействий. Далее через N и Z+ обозначаются множества натуральных и целых неотрицательных чисел соответ-свенно.
Временным автоматом (в данной работе часто просто автоматом) называется шестерка Б = (Б, I, О, в, аб, аб), где Б - конечное непустое множество состояний с выделенным начальным состоянием в, I и О - конечные непересекающиеся входной и выходной алфавиты соответственно, Аб С Б х I х О х Б - отношение переходов и А$ : Б ^ Б х (М и {то}) - функция задержки, определяющая время, по истечении которого состояние системы должно измениться, если на систему в текущем состоянии не был подан ни один входной символ, причем если для некоторого состояния в верно Аэ(в) = (в', то), то в' = в.
Если (в,г,о, в') Е аб (обозначение: в в'), то будем говорить, что автомат Б, находясь в состоянии в и принимая входной символ г, выдает выходной символ о и меняет свое состояние на в'; после этого временная переменная принимает
Рис. 1. Пример временного автомата.
значение 0, то есть отсчет времени в состоянии в' начинается с 0.
Если для каждой пары (в, г) € 5 х I существует не более одной пары (о, в') € О х Б такой, что (в, г, о, в') € Л$, то временной автомат Б называется детерминированным; иначе временной автомат называется недетерминированным. Если для каждой пары (в, г) € Б х I существует, по крайней мере, одна пара (о, в') € О х Б такая, что (в, г, о, в') € Л $, то автомат Б называется полностью определенным. Временной автомат Б называется наблюдаемым, если для любой тройки (в, г, о) € Б х I х О существует не более одного состояния в' € Б такого, что (в, г, о, в') € Л $.
Функция А$(в) = (в',£) (обозначение: в Д в') описывает переход автомата по задержке: если в состоянии в в течение Ь единиц времени на автомат не было подано ни одного входного символа, то автомат перейдет в состояние в', временная переменная примет значение 0, то есть отсчет времени в состоянии в' начнется с 0. Если для некоторого состояния в имеет место А$(в) = (в, ж), то автомат может оставаться в состоянии в бесконечно долгое время.
Пример 1. На рис. 1 представлен пример временного автомата. В нем, для упрощения, опу-
щены петли II II и IV IV. Если в состоянии I в течение трех тактов подать входное воздействие b, то на выходе появится действие a, и автомат поменяет свое состояние на II, в котором и будет оставаться до подачи следующего входного воздействия. Однако, если ни одно воздействие не будет подано в течение трех тактов, то в момент времени 3 автомат, руководствуясь переходом Д(1) = (III, 3), перейдет в состояние III.
Пусть S = (S, I, O, s, As, Дэ) - временной автомат. Временным входным символом называется пара (i,t) G I х Z+. Последовательность из временных входных символов называется временной входной последовательностью.
Временной входной символ (i,t) означает, что входной символ i подается на систему в t-ый момент времени после получения выходной реакции на предыдущее входное воздействие. В данной работе мы не уточняем, в какой момент времени после подачи входного символа выдается выходной символ. Для простоты будем считать, что если система принимает на вход некоторый входной сигнал, то выходной сигнал выдается в тот же такт, и система меняет свое состояние.
Распространим отношение поведения временного автомата на временные входные символы. Соответственно для каждого момента времени необходимо вычислить состояние, в котором будет находиться временной автомат в момент времени t. Если в начальный момент времени автомат находился в состоянии s, то с использованием функции задержки мы находим состояние s', для которого сумма задержек из состояния s не больше t и становится больше t, если к данной сумме добавить задержку в состоянии s'. Такое состооя
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.