ИСТИНА

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