Решение параллельных уравнений для w-регулярных языков | Прикладная дискретная математика. Приложение. 2009. № 1.

Решение параллельных уравнений для w-регулярных языков

We consider the problem of deriving a component of asystem that combined with a known part of a system meets the given specification. Weassume that the behavior of the overall system and of its parts is described by Buchiautomata that accept w-regular languages, i.e. languages containing infinite words. Theproblem of deriving an unknown component can be casted into the problem of solvinglanguage equations over w-regular languages. However solving techniques for equationsover regular languages cannot be directly applied to the case of w-regular languages.

Solving parallel equations over w-regular languages.pdf Многие задачи синтеза и анализа реактивных систем могут быть сведены к решениюуравнения вида C oX = S , где C , X , S суть регулярные или w-регулярные языки ио - операция композиции языков. Компонента C описывает поведение известной частисистемы и называется контекстом, компонента S описывает общее поведение системыи называется спецификацией, X есть неизвестная компонента, поведение которой необходимонайти. В данной работе мы рассматриваем случай, когда компоненты системывзаимодействуют между собой асинхронно, т. е. допускаются произвольные задержкипо времени между событиями взаимодействующих компонент. Асинхронное взаимодействиекомпонент описывается операцией параллельной композиции.В классе регулярных языков любое разрешимое уравнение имеет наибольшее решение,которое может рассматриваться как резервуар, содержащий все возможныерешения, интересные с теоретической или практической точек зрения [1]. Для уравнений,компонентами которых являются регулярные языки, известны методы нахождениянаибольшего решения [2]. Поскольку регулярные языки ассоциируются с полуавтоматамии автоматами [3], то решение уравнения для регулярных языков сводитсяк решению соответствующего автоматного уравнения.^-Регулярные языки состоят из слов бесконечной длины и описываются полуавтоматамиБюхи (Buchi) [4]. Полуавтомат Бюхи распознает слово а, если и толькоесли а посещает финальные состояния бесконечное число раз. Для регулярных языковоперация параллельной композиции включает в себя операцию распространения,которая описывает поведение компоненты относительно других компонент системы, иоперацию ограничения, которая описывает поведение компоненты относительно интересующихнас алфавитов. Соответственно при определении параллельной композициидля w-регулярных языков мы также должны определить эти операции. Мы исследовалинесколько различных операций распространения w-языка и выбрали операцию,которая вставляет между символами слов языка всевозможные конечные последовательности,определенные над внешним алфавитом. Иными словами, каждая компонента«общается» с внешней средой посредством конечных слов, но композиция в целомфункционирует бесконечно долго. Для определения операции ограничения мы ввелипонятие полуавтомата Бюхи с так называемыми е-переходами, где е - пустое слово.Ограничение ^-регулярного языка вводится аналогично ограничению регулярногоязыка, но операции ограничения ^-регулярного языка и регулярного языка обладаютразличными свойствами. Введенные операции распространения и ограничения позволяютопределить операцию параллельной композиции w-регулярных языков подобнооперации параллельной композиции для регулярных языков.Как показывает следующий пример, несмотря на то, что операции параллельнойкомпозиции регулярных и ш-регулярных языков очень похожи, методы решенияуравнений для регулярных языков не могут быть напрямую применены прирешении уравнений для ш-регулярных языков. Рассмотрим w-регулярные языкиC = ((ii + i2)(ui + W2))* (ii« i)! + (*2« 2)ш и S = (ii + *2)**! (где верхний индекс шозначает бесконечную конкатенацию слова) и их множества конечных префиксовIn it(C ) = ((ii + *2)(ui + u ))* (iiu i)* + (*2^2)* и In it(S ) = (ii + *2)*** = (ii + *2)*.Наибольшим решением уравнения In it(C ) о X = In it(S ) является регулярный языкSol = (ui + u 2)*. Как обычно, определим предел регулярного языка L как ш-регулярныйязык, содержащий каждое бесконечное слово, множество конечных префиксов которогосодержится в L. Взяв предел регулярного языка Sol, получим lim(Sol) = (ui + п2)ш.Однако ш-язык (ni + п2)ш не является решением уравнения C о X = S , так как (ni + п2)шсодержит слово п., расширение которого на алфавит I содержит слово (i2n2)! , а значит,пересечение C П (lim(Sol))^/ будет содержать слово (i2n2)! , ограничением которогона алфавит I будет слово i., не содержащееся в S . Однако можно показать, чтоформула наибольшего решения для ш-регулярных языков имеет такой же вид, как ипри решении уравнения для регулярных языков, т. е. наибольшее решение уравненияC о X = S есть ш-язык C о S. В нашем примере наибольшим решением уравненияявляется ш-регулярный язык (ni + п2)ш\п%.Бушков В. Г. выражает благодарность фонду Бортника за финансовую поддержкупо проекту 8858, Евтушенко Н. В. выражает благодарность РФФИ за финансовуюподдержку по проекту 06-08-89500.

Ключевые слова

Авторы

ФИООрганизацияДополнительноE-mail
Бушков Виктор ГеоргиевичТомский государственный университетмагистрантv.bushkov@gmail.com
Евтушенко Нина ВладимировнаТомский государственный университетпрофессор, доктор технических наук, заведующая кафедройninayevtushenko@yahoo.com
Всего: 2

Ссылки

Buffalov S., El-Fakih K., Yevtushenko N., et al. Progressive solutions for a parallel automata equation / / FORTE'03. Berlin: Springer, 2003. P. 367-382.
Yevtushenko N. V., Villa T., Brayton R. K., et al. Sequential synthesis by language equation solving / / Intenational Workshop on Logic Synthesis. June, 2000.
Глушков В. М. Синтез цифровых автоматов. М.: Физматгиз, 1962. 476 с.
Mukund M. Finite-state automata on infinite inputs / / The 6th National Seminar on Theorectical Computer Science. Banasthali, Rajasthan, India, 1996. V. 2.
 Решение параллельных уравнений для w-регулярных языков | Прикладная дискретная математика. Приложение. 2009. № 1.

Решение параллельных уравнений для w-регулярных языков | Прикладная дискретная математика. Приложение. 2009. № 1.