Національна академія наук України
Національна академія наук України
Інститут кібернетики імені В.М.Глушкова
ЧЕБОТАРЬОВ Анатолій Миколайович
УДК 519.713.1
ДОКАЗОВЕ ПРОЕКТУВАННЯ АЛГОРИТМІВ
ФУНКЦІОНУВАННЯ РЕАКТИВНИХ СИСТЕМ
05.13.13 — обчислювальні машини, системи та мережі
Автореферат дисертації на здобуття наукового ступеня
доктора технічних наук
Київ 2002
Дисертацією є рукопис
Робота виконана в Інституті кібернетики ім. В.М.Глушкова НАН України
Науковий консультант доктор технічних наук, професор Коваль Валерій
Миколайович, Інститут кібернетики ім. В.М.Глушкова
НАН України, завідувач відділом
Офіційні опоненти:
доктор фізико-математичних наук, професор Анісімов Анатолій
Васильович, Київський національний університет ім. Т.Г.Шевченка,
завідувач кафедрою математичної інформатики,
доктор технічних наук, професор Кузнєцов Олег Петрович,
Інститут проблем управління ім. В.О.Трапєзнікова РАН,
завідувач лабораторією,
доктор технічних наук, професор Литвинов Віталій Васильович,
Інститут проблем математичних машин і систем НАН України,
завідувач відділом.
Провідна установа:
Національний технічний університет України “КПІ” МОН України,
кафедра обчислювальної техніки.
Захист відбудеться “ 5 ” грудня 2002 р. о “ 14 ” годині на засіданні спеціалізованої вченої ради
Д 26.194.03 в Інституті кібернетики ім. В.М.Глушкова НАН України за адресою:
03680, МСП, Київ-187, проспект Академіка Глушкова, 40.
З дисертацією можна ознайомитися у бібліотеці Інституту кібернетики НАН України.
Автореферат розісланий “ 30 ” жовтня 2002 р.
Учений секретар
спеціалізованої вченої ради РОМАНОВ В.О.
ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ
Актуальність теми дисертації. Наш час характеризується інтенсивною комп'ютеризацією усіх сфер людської діяльності, широким розповсюдженням автоматичних методів одержання і обробки інформації з використанням кібернетичних систем. Серед сучасних кібернетичних систем суттєво збільшилася кількість реактивних систем, тобто систем, постійно взаємодіючих з їхнім оточенням. Це, зазвичай, системи реального часу, робота яких полягає у виробленні реакції (звідси назва “реактивні”) на вхідну інформацію, що змінюється. До таких систем відносяться також розподілені або багатоагентні системи, кожний агент яких постійно взаємодіє з одним або кількома іншими агентами, які утворюють для нього зовнішнє середовище. Прикладами реактивних систем є телекомунікаційні мережі, системи керування технологічними процесами, системи керування літальними апаратами тощо.
Помилки у функціонуванні таких систем, як системи керування ядерними реакторами, хімічним виробництвом, засобами космічної техніки можуть призвести до катастрофічних наслідків, пов'язаних з великими матеріальними втратами і людськими жертвами. Тому до надійності та безпомилковості функціонування таких систем висуваються надзвичайно жорсткі вимоги. Зокрема, необхідно, щоб алгоритм функціонування системи точно відповідав вимогам, які визначаються його початковою специфікацією. Досягнути цього можна застосуванням строгих методів коректного проектування алгоритмів функціонування реактивних систем (реактивних алгоритмів), причому велике значення має забезпечення коректності алгоритму на початкових етапах його розробки, оскільки вартість усунення помилок, допущених на цих етапах, найбільш велика.
У методах коректного проектування реактивних алгоритмів, які використовуються на початкових етапах їх розробки, можна виділити два основні підходи:
а) формальна верифікація неформально одержаного процедурного представлення алгоритму;
б) використання математично обгрунтованих формальних методів для перетворення декларативної специфікації вимог до функціонування алгоритму в імперативне (процедурне) його представлення високого рівня.
При першому підході доводиться, що одержаний алгоритм має певні необхідні властивості, але не гарантується, що поведінка алгоритму буде точно відповідати його призначенню. При другому підході, який називається синтезом, гарантується точна відповідність початкової специфікації алгоритму її процедурній реалізації. У цьому випадку початкова специфікація повинна відображувати усі вимоги до функціональної поведінки алгоритму, що проектується.
Зазначені підходи мають ряд спільних рис. При обох підходах для задання початкової специфікації алгоритму або його властивостей використовуються декларативні мови. Деякі методи верифікації реактивних алгоритмів, зокрема методи перевірки здійсненності специфікації на моделі (model checking), так само, як і методи другого підходу, використовують процедуру синтезу автомата за логічною специфікацією властивостей алгоритму. Однак характер задач, що розв'язуються, їхня розмірність і методи розв'язання в цих двох підходах суттєво відрізняються.
Синтез алгоритму – це не одноразовий акт, а послідовність перетворень, які здійснюються, зазвичай, за участю людини. При цьому результат синтезу буде гарантовано задовольняти початкову специфікацію лише у випадку, якщо коректність кожного перетворення, яке здійснюється в процесі синтезу, буде формально доведена. Це стосується не тільки перетворень, які виконуються автоматично (коректність котрих забезпечується формальним доведенням коректності відповідних методів), але й тих, що здійснюються за участі людини. Таким чином, усіляке втручання людини в процес проектування повинне контролюватися системою проектування, яка відхиляє помилкові дії розробника. Таку методологію проектування реактивних алгоритмів назвемо доказовим проектуванням. Слід зазначити, що іноді доказовим проектуванням називають методологію, яка базується на верифікації, оскільки вона використовує автоматичне доведення теорем або перевірку здійсненності формул. У нашому випадку цей термін характеризує методологію проектування реактивних алгоритмів, основану на автоматичному синтезі, результати якого не потребують перевірки на відповідність специфікації.
Гостра необхідність розвитку методів коректного проектування реактивних систем, особливо систем, критичних до помилок їхнього функціонування, викликала велику кількість робіт, присвячених дослідженням у цій області. Особливо інтенсивно ці дослідження стали розвиватися з початком використання різних темпоральних логік для специфікації і верифікації реактивних алгоритмів. Основоположними в цій області були роботи Дж.Бюхі, П.Волпера, Е.Кларка, Л.Лемпорта, З.Манни, А.Пнуелі, М.Рабіна, Д.Скотт, Б.А.Трахтенброта, Е.Емерсона та ін. Їхні ідеї одержали широкий розвиток, і нині методи, які використовують темпоральні логіки або інші аналогічні числення, наприклад, числення, що базуються на операторах нерухомої точки, застосовуються на усіх етапах проектування реактивного алгоритму, починаючи із специфікації, верифікації і закінчуючи формальним синтезом алгоритму. Ці дослідження пов'язані з такими іменами як М.Варді, Р.Куршан, Р.МакНотон, А.Сістла, В.Томас (автоматичні методи в дослідженнях реактивних алгоритмів), К.МакМіллан, Ф.Сомензі (підхід до верифікації, оснований на перевірці здійсненності формули на моделі); Р.Е.Брайант, Р.К.Брайтон, Р.Куршан, О.А.Міщенко (використання двійкових діаграм рішень для ефективної реалізації алгоритмів проектування) та багатьма іншими. Вітчизняні учені також зробили суттєвий внесок у теорію і практику доказового проектування реактивних алгоритмів. Слід згадати закладену В.М.Глушковим і продовжену його учнями (Ю.В.Капітоновою, О.А.Летичевським, К.П.Вершиніним, О.І.Дегтярьовим, О.В.Лялецьким, М.К.Мороховець) школу автоматизації доведення теорем, а також роботи Ю.В.Капітонової, В.М.Коваля, О.А.Летичевського в області логіко-алгебраїчного підходу до проектування програм і систем.
Нині основна увага приділяється розробці методів, придатних для проектування систем промислового рівня складності. Хоча автори багатьох робіт підкреслюють переваги й перспективність методології синтезу, переважна більшість робіт, які відносяться до вищезазначених напрямків досліджень, розвивають перший підхід до проектування коректних алгоритмів, і тільки в лічених роботах розглядаються проблеми, пов'язані з методологією синтезу реактивного алгоритму. Це обумовлено складністю проблеми синтезу, яка для лінійної темпоральної логіки або логіки CTL* є повною в класі 2EXPTIME. Використання синтезу при верифікації обмежується синтезом автомата, що відповідає властивості системи, яка перевіряється. Звичайно формули, які виражають властивості, що мають практичний інтерес, досить прості, і відповідний автомат має незначну кількість станів у порівнянні з моделлю алгоритму, що верифікується. При використанні методології синтезу для проектування алгоритмів специфікації реальних систем виражаються формулами, у сотні разів більш складними, що робить застосування методів синтезу, які використовуються при верифікації, практично неможливим. Крім того, саме формулювання проблеми синтезу розрізняється для двох розглянутих підходів. У першому випадку проблема синтезу розглядається для замкнутої системи, коли для існування розв'язку достатньо несуперечності специфікації, у другому – для відкритої, коли потрібно існування розв'язку для будь-якої можливої поведінки середовища, що значно ускладнює проблему.
Таким чином, актуальна проблема забезпечення безпомилковості процесу проектування реактивних алгоритмів практичного рівня складності на етапі побудови процедурного представлення алгоритму до цього часу не вирішена.
Зв'язок роботи з науковими програмами і темами. Робота виконувалася відповідно до наступних наукових тем Інституту кібернетики НАН України, в яких дисертант був відповідальним виконавцем та виконавцем.
СГ.100.01 “Створити і ввести в дослідну експлуатацію в Інституті кібернетики ім. В.М.Глушкова АН УРСР САПР високопродуктивних ЕОМ з апаратною реалізацією системного програмного забезпечення на основі перспективної елементної бази” №ДР 01860096699 (1986 – 1990);
СГ.100.03 “Створити і ввести в експлуатацію експериментальну систему для автоматизованого проектування ЕОМ нових поколінь на НВІС з рівнем інтеграції 106 елементів на кристал” №ДР 01860045702 (1986 – 1989);
В.Г.Е.100.09 “Розробити ефективні методи доведення тверджень та розв'язку задач на алгебро-логічних моделях предметних областей” №ДР 0194U009539 (1991 – 1994);
В.Ф.100.03 “Розробка математичної теорії взаємодії компонент комп'ютерного середовища та її застосування у системі програмування АПС” №ДР 0198U00320 (1998 – 2000);
Проект INTAS 96-0760 “Rewriting Techniques and Efficient Theorem Proving” в рамках Європейської наукової програми INTAS (1998 – 2000).
Метою дисертаційної роботи є розв'язання проблеми забезпечення безпомилковості процесу проектування реактивних алгоритмів промислового рівня складності, що передбачає розробку математичного апарату доказового проектування алгоритмів і на цій основі розробку методології проектування, яка гарантує одержання такого процедурного представлення алгоритму, яке задовольняє усі вимоги до функціонування цього алгоритму.
Основні задачі дисертаційної роботи, які визначаються поставленою метою.
1. Розробити систему орієнтованих на синтез мов специфікації реактивних алгоритмів на основі логіки предикатів першого порядку, яка забезпечує прийнятний компроміс між виразністю засобів специфікації та ефективністю обробки специфікацій процедурами проектування.
2. Розробити математично обгрунтовані методи перевірки несуперечності специфікацій, які суттєво перевершують за ефективністю існуючі методи.
3. Розробити теорію і методи синтезу керуючої частини реактивного алгоритму, виходячи з автоматної семантики мов специфікації.
4. Розробити математичний апарат аналізу взаємодіючих процесів, призначений для розв'язку задач синтезу алгоритмів функціонування відкритих систем.
5. На основі побудованої теорії взаємодіючих автоматів розробити методи перевірки реалізуємості специфікації та її одночасного перетворення до вигляду, необхідного для реалізації, з урахуванням інформації про поведінку середовища.
6. Розробити ефективні методи синтезу автомата-розпізнавача за формулою лінійної темпоральної логіки.
7. Розробити методи редукції моделі алгоритму, що верифікується, необхідні для верифікації складних алгоритмів, одержаних у результаті синтезу.
Предметом дослідження є задачі та методи доказового проектування реактивних алгоритмів на початковому етапі їхньої розробки, зокрема задачі, які виникають при переході від декларативної специфікації алгоритму до його процедурного представлення.
Методи досліджень базуються на математичній логіці, теорії доведень, теорії автоматів, теорії автоматів-розпізнавачів над нескінченними об'єктами, теорії паралельних процесів.
Наукова новизна роботи полягає в побудові теорії доказового проектування реактивних алгоритмів. Зокрема:
· запропоновано теоретично обгрунтований підхід до побудови синтаксису і семантики мов специфікації, який дозволив розробити ефективні процедури проектування;
· запропонована семантика використовуваних мов специфікації та урахування специфіки предметної області дозволили удосконалити резолюційні методи перевірки несуперечності специфікацій, що призвело до суттєвого підвищення їхньої ефективності;
· для сформульованої у новій постановці проблеми аналізу коректності взаємодії двох процесів розроблено математичний апарат, який дозволив одержати більш прості та ефективні методи її розв'язання у порівнянні з використовуваними методами на основі теоретико-ігрового підходу;
· на основі доведеної теореми про специфікацію побудовано ряд методів синтезу автоматів, суттєво ефективніших, ніж метод семантичного табло, який нині використовується;
· в області верифікації алгоритмів запропоновано метод синтезу автомата–розпізнавача за формулою лінійної темпоральної логіки, який дає значно кращі результати за кількістю станів автомата в порівнянні з останніми відомими методами, а також метод редукції алгоритму, що верифікується;
· у процесі вирішення задач доказового проектування реактивних алгоритмів одержано нові результати в теорії автоматів над нескінченними послідовностями.
Усі запропоновані методи і алгоритми теоретично обгрунтовано.
Практичне значення одержаних результатів. Використання на практиці запропонованих методів проектування дозволяє значно скоротити терміни розробок, суттєво зменшити обсяг робіт, пов'язаних із специфікою алгоритмів функціонування реактивних систем та їхньої верифікації, а також уникнути помилок у процедурному представленні алгоритмів, що розроблюються. Гарантована відповідність алгоритму його декларативній специфікації суттєво підвищує надійність процесу проектування, яка, у свою чергу, відбивається на надійності систем, що розроблюються.
Запропоновані методи, алгоритми та засоби проектування використовувалися в ряді розробок, у тому числі:–
спеціалізованих процесорів і системи обміну інформацією спільно з п/я А-1178,–
засобів сполучення компонентів локальної інформаційно-обчислювальної мережі (“СИЛУР”) спільно з п/я В-2431,–
інтелектуальної системи управління движителями мобільних роботів спільно з Донецьким державним інститутом штучного інтелекту.–
підсистеми управління системи відтворення звуку з валиків Едісона в Інституті проблем реєстрації інформації НАН України.
Основні фрагменти методики проектування реалізовані в системах автоматизації доказового проектування реактивних алгоритмів PROCOD і Dual.
Теоретичні та прикладні результати досліджень знайшли відображення в навчальних курсах за відповідними спеціальностями, що читаються у Національному авіаційному університеті,
м. Київ, Технологічному університеті Поділля, м. Хмельницький та Портлендському університеті, США.
Особистий внесок здобувача. Усі наукові результати, наведені в дисертації, одержані особисто здобувачем. У роботах [5, 7, 14, 20], опублікованих у співавторстві, дисертантові належать постановки задач і основні теоретичні результати, пов'язані з методами їхнього розв'язання, у роботі [17] – методи специфікації та синтезу автоматів, у роботі [23] – підхід до побудови специфікації реактивного алгоритму.
Апробація результатів дисертації. Результати досліджень, подані в дисертації, доповідалися на таких конференціях та семінарах. На II Всесоюзній конференції з прикладної логіки (Новосибірськ, 1988), на ХХХ Всесоюзній школі-семінарі ім. М.А.Гаврилова (Кишинев, 1988), на IV міжнародній конференції “Logic Programming and Automated Reasoning” (Санкт-Петербург, 1993), на I міжнародному науковому семінарі ”The First NASA/DOD Workshop on Evolvable Hardware” (Пасадена, США, 1999), на міжнародному семінарі “Rewriting Techniques and Efficient Theorem Proving” (Київ, 2000), на I і III міжнародних науково-практичних конференціях з програмування УкрПРОГ (Київ, 2000, 2002), неодноразово на Республіканському семінарі "Теорія автоматів та її застосування" наукової ради НАН України з проблеми "Кібернетика" (Київ).
Публікації. За темою дисертації опубліковано 28 друкованих робіт, з них 19 – у провідних вітчизняних та зарубіжних журналах, чотири – в працях конференцій, чотири – у збірниках та одна – в тезах конференції.
Структура та обсяг роботи. Дисертація складається із вступу, семи розділів, заключної частини, списку використаних джерел, який налічує 134 найменування, та двох додатків. Повний обсяг дисертації становить 307 сторінок, з них три рисунки, 12 сторінок переліку використаних джерел та 16 сторінок додатків.
ОСНОВНИЙ ЗМІСТ РОБОТИ
У вступі на основі аналізу стану проблеми, що досліджується, обгрунтовується актуальність теми дисертації, формулюються мета і задачі дослідження, стисло характеризується зміст дисертації.
У першому розділі розглянуто мови специфікації реактивних алгоритмів, побудовані на логіці одномісних предикатів першого порядку. Запропоновано дворівневу організацію системи мов специфікації, доведено ряд теорем, які дозволили визначити автоматну семантику мов, а також теорему про специфікацію, що лежить в основі методів аналізу і синтезу автоматних моделей алгоритмів і підходу до вибору мови специфікації верхнього рівня.
Предметом дослідження у першому розділі є функціональна специфікація алгоритму, тобто опис його функціональних властивостей, який починається з побудови функціональної моделі алгоритму. Основні поняття, в термінах яких здійснюється опис функціональної моделі, поділяються на три класи: об'єкти, дії, умови. Об'єкти – це змінні, значеннями яких можуть бути числа, слова, множини, послідовності, масиви тощо. Дії – це перетворення, що виконуються над об'єктами і змінюють їхні стани, а також сигнали (або повідомлення), які видаються у зовнішнє середовище. Умови – це предикати, визначені на станах об'єктів і вхідних змінних алгоритму.
Побудова функціональної моделі починається з вибору структур даних, тобто об'єктів і операцій (дій) над ними, найбільш зручних для опису моделі. Потім визначаються умови й формулюються твердження, які характеризують відношення між станами об'єктів, перетворення об'єктів, визначені операціями, і умови виконання операцій. Ці твердження, виражені в логічній мові, складають логічну специфікацію алгоритму.
Алгоритм, що специфікується, подається у вигляді двох частин: керуючої і операційної, які взаємодіють між собою та з зовнішнім середовищем. Взаємодія між керуючою і операційною частинами здійснюється через двійкові канали. Взаємодія з зовнішнім середовищем здійснюється як через інформаційні канали, так і через двійкові (керуючі) канали. Логічна специфікація алгоритму визначає опис його керуючої частини та тих аспектів операційної частини й зовнішнього середовища, які відносяться до взаємодії керуючої і операційної частин між собою та з зовнішнім середовищем. Отже, логічна специфікація алгоритму складається з трьох частин: специфікацій керуючої частини, операційної частини та зовнішнього середовища. Математичною моделлю кожної з вищеперелічених частин специфікації є скінченний автомат. Складові частини алгоритму зручно специфікувати як неініціальні системи, окремо задаючи початкову умову, яка визначає початкові стани відповідних автоматів.
У пропонованій методології проектування передбачається використання двох рівнів мови: мови початкової специфікації L*, яка має достатні для практичних потреб виражальні можливості й забезпечує зручність запису початкових вимог до алгоритму, та внутрішньої мови (мова L), яка має порівняно обмежені виражальні можливості, але ефективно оброблюється процедурами синтезу. Специфікація у початковій мові однозначно транслюється у внутрішню мову.
Розгляд мов специфікації розпочнемо з більш простої мови L. Мова L є фрагментом логіки предикатів першого порядку з одномісними предикатами й фіксованою областю інтерпретації, якою виступає множина Z цілих чисел (множина моментів часу).
Позначимо F0 і F1 множини формул, побудованих за допомогою логічних зв'язок відповідно із атомів вигляду p(k) або p(t+k), де p – одномісний предикатний символ, t – змінна, + – операція додавання цілих чисел, а k – цілочислова константа, яка називається рангом атома. Різниця між максимальним і мінімальним рангами атомів, які входять у формулу, називається її глибиною. Формули із F0 використовуються тільки для задання початкових умов, а специфікацією неініціальної системи є формула вигляду "tf(t), де f(t)ОF1.
Інтерпретація мови – це впорядкований набір визначених на Z одномісних предикатів, які відповідають усім предикатним символам із множини W предикатних символів мови (сигнатура предикатних символів).
Нехай W = {p1, …, pq}. Інтерпретація I = <p1, ј, pq>, де pi (i = 1, …, q) – одномісні предикати, визначені на Z, називається моделлю для формули F, якщо F істинна при цій інтерпретації.
Обмеження предиката p на область Zs = {zОZ | z і s}, де s О Z, назвемо s-обмеженням цього предиката. Відповідно визначимо s-обмеження інтерпретації I як впорядковану сукупність s-обмежень предикатів p1, ј, pq. Для кожного моменту часу z О Z набір <p1(z), ј, pq(z)> є двійковим вектором довжини q. Нехай S – множина усіх таких векторів, тоді s-обмеження інтерпретації I можна розглядати як нескінченне слово (синоніми: надслово, w-слово) в алфавіті S. Так установлюється відповідність між інтерпретаціями мови і надсловами в алфавіті S. З кожною несуперечною замкнутою формулою F асоціюється множина WF надслів у алфавіті S, які відповідають 1-обмеженням усіх моделей для формули F. Множину WF назвемо множиною надслів, що задаються формулою F.
Автоматна семантика мови L.
Визначення 1.1. Скінченний X–Y-автомат Мура А – це п'ятірка <X, Y, Q, cA, mA>, де X і Y – відповідно вхідний і вихідний алфавіти, Q – скінченна множина станів, а cA: QґX ® 2Q і mA: Q ®– відповідно функції переходів і виходів. Автомат А називається детермінованим, якщо для будь-яких x О X, q О Q ЅcA(q, x)ЅЈ 1, у супротивному разі він називається недетермінованим.
Визначення 1.2. X–Y-автомат A = <X, Y, Q, cA, mA> називається квазідетермінованим, якщо для будь-яких x О X, q О Q із q1, q2 О cA(q, x) випливає m(q1) № № m(q2).
Автомат А, серед станів якого виділено одне або декілька початкових станів, називається ініціальним, у супротивному разі автомат називається неініціальним. Ініціальний автомат A0 задається у вигляді пари (A, F0), де A – неініціальний автомат, а F0 – початкова умова, яка визначає в ньому деяку непусту підмножину початкових станів. На всіх етапах синтезу, де автомат подається у вигляді формули мови специфікації, розглядається перший елемент цієї пари, і тільки на заключному етапі, коли буде побудовано множину станів автомата, що специфікується, використовується другий елемент пари. Це зроблено щоб виключити терми, які не містять змінних, і цим спростити процедури синтезу.
Визначення 1.3. X–Y-автомат A = <X, Y, Q, cA, mA> називається циклічним, якщо для кожного q О Q виконуються такі умови:
існують такі x1 О X і q1 О Q, що q1 О cA(q, x1),
існують такі x2 О X і q2 О Q, що q О cA(q2, x2).
Очевидно, що будь-який автомат, що визначає поведінку керуючої або операційної частини реактивного алгоритму, може бути заданим у вигляді пари (A, F0), де A – циклічний автомат.
Надслово в алфавіті XґY назвемо вхід-вихідним надсловом.
Циклічний автомат може бути однозначно охарактеризованим у термінах допустимих вхід-вихідних надслів.
Визначення 1.4. Вхід-вихідне надслово l = (x1, y1)(x2, y2)… допустиме в стані q автомата A, якщо існує таке надслово станів q0q1q2…, де q0 = q, що для будь-якого i = 0, 1, 2,… qi+1 О cA(qi, xi+1) і m( qi+1) = yi+1. Вхід-вихідне надслово l допустиме для автомата А, якщо воно допустиме
хоча б в одному із його станів.
Позначимо W(A) множину всіх вхід-вихідних надслів, допустимих для автомата А.
Теорема 1.1. Для кожної несуперечної формули F вигляду "tf(t) (f(t) О F1) існує у загальному випадку недетермінований неініціальний циклічний автомат А, для якого множина всіх допустимих вхід-вихідних надслів співпадає з множиною надслів, які задаються формулою F.
Ця теорема визначає автоматну семантику мови. Будемо говорити, що автомат А задовольняє специфікацію F, якщо W(A) = WF. Клас усіх автоматів, які задовольняють специфікацію F, позначатимемо K(F). Розглянемо спосіб побудови автомата A(F) із класу K(F), який використовувався при доведенні теореми 1.1.
Нехай специфікація автомата має вигляд F = "tf(t). При інтерпретації таких формул на множині цілих чисел для будь-якого k О Z справедлива еквівалентність "tf(t) Ы "tf(t+k), де f(t+k) позначає формулу, отриману із f(t) шляхом додавання k до рангів усіх її атомів (зсув на k). Таким чином, можна обмежитися розглядом формул f(t), у яких максимальний ранг атомів дорівнює 0.
Нехай W – множина всіх предикатних символів, які зустрічаються у формулі f(t), а r – глибина цієї формули. Позначимо SW множину всіх двійкових векторів довжини |W|, де |W| позначає потужність множини W. Послідовність s0, s1, …, sr векторів із SW назвемо станом глибини r, а множину Q(r, W) усіх таких послідовностей – простором станів глибини r для формули f(t). На множині Q(r, W) визначимо відношення N безпосереднього слідування так, що за кожним станом q = s0, s1, …, sr безпосередньо слідують 2|W| станів вигляду s1, …, sr, s , де s О SW. Множину всіх станів, які безпосередньо слідують за q, будемо позначати N(q). Якщо компоненти вектора si у стані q = s0, s1, …, sr розглядати як істинностні значення відповідних атомів рангу i r при певному впорядкуванні множини W, то можемо говорити про значення формули f(t) на стані q.
При використанні мови L для специфікації автоматів предикатні символи ставляться у відповідність вхідним і вихідним двійковим каналам автомата, що специфікується. Тому множина предикатних символів W розбивається на два класи: вхідні й вихідні, які позначаються відповідно U і W. Визначимо вхідний алфавіт X і вихідний алфавіт Y автомата A(F) як множини всіх двійкових векторів довжини відповідно |U| і |W|. Кожний вектор із SW можна розглядати як пару <x, y>, де x О X, y О Y, тому нарівні з позначенням s0, …, sr для стану глибини r будемо використовувати позначення <x0, y0>, …, <xr, yr>.
Побудуємо допоміжний автомат Aў(F) = <X, Y, Qў, cAў, mAў >. Множина станів Qў – це усі ті стани із Q(r, W), на яких f(t) істинна. Функції переходів і виходів цього автомата визначимо таким способом. Нехай q О Qў і x О X, тоді cAў(q, x) – це множина всіх тих станів <x0, y0>, …, <xr, yr> із N(q) З Qў, у яких xr = x; mAў(<x0, y0>, …, <xr, yr>) = yr. Автомат A(F) є максимальним циклічним підавтоматом автомата Aў(F).
Визначення 1.5. Автомат А називається автоматом зі скінченною пам'яттю, якщо існує таке натуральне k, що стани, в які кожне допустиме вхід-вихідне слово довжини k переводить усі стани автомата A, еквівалентні.
Клас усіх автоматів, які специфікуються в мові L, складають циклічні квазідетерміновані автомати зі скінченною пам'яттю.
Простота мови L дозволила отримати для неї досить ефективні процедури синтезу, але зумовлені цією простотою невеликі виражальні можливості мови перешкоджають використанню її як засобу початкової специфікації і обмежують клас автоматів, що специфікуються, автоматами зі скінченною пам'яттю.
Мова L* з достатніми для практичних потреб виражальними властивостями будується як підмножина мови Lmax , яка є природним розширенням мови L, пов'язаним із введенням кванторів і лінійного порядку на множині цілих чисел.
Множина термів мови Lmax має вигляд T = {(ti + k) | ti О Var, k О Z}, де + – операція додавання цілих чисел, а Var = {t, t1, …, tn} – множина предметних змінних.
Маємо два типи атомарних формул (атомів): {pi(t) | pi О W, t О T}, де W – множина одномісних предикатних символів, і {ti Ј tj | ti, tj О T}. Формули, які використовуються для специфікації автоматів, мають вигляд "tF(t), де F(t) – довільна формула мови першого порядку з одною вільною змінною t. Областю інтерпретації мови є множина Z цілих чисел.
Нижче наведено результати, які дозволяють пов'язати синтаксичні обмеження, що накладаються на клас формул мови, з її виражальними можливостями й властивостями процедури синтезу. Ці результати використовуються для виділення підмножини L* мови Lmax. Оскільки сполучною ланкою між формулами й автоматами, які ними специфікуються, виступають множини надслів
(w-слів), визначимо необхідні типи надслів, операції над ними, а також топологію на множині надслів, у термінах якої характеризуються класи формул.
Нехай S — скінченний алфавіт, Z — множина цілих чисел, N+ = {z О Zф z > 0} і
N- = {z ОZф z Ј 0}. Відображення r множини {1, …, n} (n О N+) в S називається словом довжини n в алфавіті S і позначається r = r(1)r(2)…r(n). Відображення u: Z ® S, l: N+®і g: N-® S називаються відповідно двостороннім надсловом (позначається …u(-2)u(-1) u(0)u(1)u(2)…), надсловом (позначається l(1)l(2)… ) і зворотним надсловом (позначається …g(-2)g(-1)g(0)) в алфавіті S. Множина всіх слів у алфавіті S, включаючи пусте слово, позначається S*, множина всіх надслів – Sw, а множина всіх зворотних надслів – S-w. Для двостороннього надслова u і n О Z визначимо n-префікс u(-Ґ, n) і n-суфікс u(n+1, Ґ) відповідно як зворотне надслово …u(n-2)u(n-1)u(n) і надслово u(n+1)u(n+2)…. Якщо значення n не суттєве, будемо говорити про w-префікс і w-суфікс двостороннього надслова.
На множині S* И S-w И Sw визначимо звичайним способом (часткову) операцію конкатенації "Ч", яку поширимо також на множини слів і надслів.
Множину Sw розглядатимемо як топологічний простір з так званою природною топологією. Відкритими множинами в цій топології є усі множини вигляду KЧSw, де K Н S*. Доповнення відкритої множини в Sw називається замкнутою множиною.
Симетрично запроваджується топологія на S-w.
Перейдемо до опису надсловарної семантики Lmax. Кожній замкнутій формулі F мови ставиться у відповідність множина моделей для цієї формули, тобто множина таких інтерпретацій, на яких F істинна. Нехай W = {p1, …, pq} — множина всіх одномісних предикатних символів, які зустрічаються у формулі F. Інтерпретація формули F –це впорядкований набір визначених на Z одномісних предикатів p1, ј, pq, які відповідають предикатним символам із W. Нехай S – множина всіх двійкових векторів довжини q, тоді інтерпретацію I = <p1, ј, pq> можна подати у вигляді двостороннього надслова в алфавіті S, а множину всіх моделей для F – у вигляді множини MF двосторонніх надслів у цьому алфавіті. Кожному u О MF поставимо у відповідність множину надслів Su = {l О Sw | u(-Ґ, 0)Чl О MF}. Таким чином отримуємо сукупність множин надслів ВF = {Su ф u О MF}. Ця сукупність визначає надсловарну семантику формули F.
Для визначення автоматної семантики мови Lmax зручно використовувати модель автомата Мілі.
Визначення 1.6. Скінченний неініціальний X–Y-автомат Мілі А є четвіркою <X, Y, Q, dA>, де X, Y, Q – скінченні множини відповідно вхідних символів, вихідних символів і станів, а
dA: QґXґY ® 2Q – функція переходів автомата.
X–Y-автомат Мілі A називається квазідетермінованим, якщо для будь-яких q О Q, x О X, y О Y |dA(q, x, y)| Ј 1. Квазідетерміновані X–Y-автомати зручно розглядати як детерміновані часткові автомати без виходу з вхідним алфавітом S = XґY. Такий автомат A = <S, Q, dA>, де dA: QґS ® Q – часткова функція, називатимемо S-автоматом.
Нехай q1, q2 О Q. Трійку <q1, s, q2>, таку що dA(q1, s) = q2, назвемо переходом в автоматі A = <S, Q, dA> із стану q1 в стан q2, а символ s – позначкою цього переходу. Визначення циклічного S-автомата та допустимості вхідного надслова (S-надслова) аналогічні наведеним раніше. Далі під автоматом будемо розуміти неініціальний циклічний S-автомат.
Визначення 1.7. Зворотне S-надслово …s-1s0 представлене станом q автомата A, якщо існує таке зворотне надслово станів …q-2q-1q0, де q0 = q, що для будь-якого i = -1, -2, … dA(qi, si+1) = qi+1.
Отже, з кожним станом qi циклічного S-автомата асоціюється множина Si всіх S-надслів, допустимих у стані qi, і множина Pi всіх зворотних S-надслів, представлених станом qi. Нехай множина Q станів S-автомата A дорівнює {q1, …, qn}. Сукупність множин S-надслів (S1, …, Sn), де Si – множина надслів, допустимих у стані qi (i = 1, 2, …, n), назвемо поведінкою (неініціального) автомата A.
Визначення 1.8. Два автомати A1 і A2 з поведінками відповідно (Sў1, …, Sўn) і (SІ1, …, SІm) називаються еквівалентними (строго еквівалентними), якщо кожне Sўi (i = 1, …, n) міститься серед SІ1, …, SІm і кожне SІi (i = 1, …, m) міститься серед Sў1, …, Sўn.
Прокоментуємо поняття “поведінка автомата”. Коли мовою специфікації була мова L, а отже автомати, що специфікувалися, належали класу циклічних автоматів зі скінченною пам'яттю, відповідною характеристикою автомата була множина всіх допустимих для нього вхід-вихідних надслів. Для циклічних автоматів зі скінченною пам'яттю така характеристика визначала автомат з точністю до еквівалентності. У разі циклічних автоматів, пам'ять яких не є скінченною, це вже не так. Тому щоб із збіжності поведінок автоматів випливала їхня еквівалентність, доводиться використовувати більш тонку характеристику.
Основна ідея, яка дозволяє використовувати формулу F для специфікації автомата, полягає в тому, що сукупність множин надслів ВF розглядається як поведінка певного S-автомата.
У роботі сформульовано й доведено необхідні та достатні умови того, щоб сукупність
(S1, …, Sn) множин надслів у алфавіті S була поведінкою певного S-автомата з n станами.
Не для кожної формули F = "tF(t) ВF задовольняє ці умови, тобто не кожна така формула специфікує скінченний автомат. Але за умов певних обмежень класу формул, що розглядаються, сукупність множин надслів, яка асоціюється з формулою F, задовольняє необхідні вимоги.
Визначення 1.9. Замкнута формула F фіктивна в інтервалі (k, +Ґ), якщо на будь-яких двосторонніх надсловах, k-префікси яких співпадають, вона або одночасно істинна, або одночасно хибна.
Визначення 1.10. Формула F(t), з однією вільною змінною t, називається k-обмеженою (k О Z), якщо для будь-якого t О Z F(t) фіктивна в інтервалі (t + k, +Ґ).
Теорема 1.2. Кожна несуперечна формула вигляду "tF(t), де F(t) – k-обмежена формула, задає поведінку скінченного неініціального S-автомата.
Отже, якщо всі формули мови специфікації k-обмежені, то будь-яка несуперечна формула специфікує непустий клас автоматів. Але залишається відкритим питання побудови процедури синтезу автомата за специфікацією і процедури перевірки несуперечності специфікації. Задача полягає у виборі такої підмножини мови Lmax, щоб зазначені проблеми мали достатньо просте рішення і при цьому не дуже зменшувався клас автоматів, що специфікуються. Для розв'язку цієї задачі використовується доведена в дисертації теорема про специфікацію. Наведемо деякі погодження і результати, необхідні для формулювання цієї теореми.
Формулу F(t) з однією вільною змінною t будемо використовувати для задання множини зворотних надслів, а саме, множини k-префіксів усіх таких двосторонніх надслів u, що F(k) істинна на u.
Як зазначалося вище, символи алфавіту двосторонніх надслів, які відповідають моделям (інтерпретаціям) для формули F, є двійковими векторами, компоненти яких відповідають одномісним предикатним символам формули. Кожному такому двійковому вектору довжини q поставимо у відповідність кон'юнкцію вигляду p?1(t)& … &p?q(t), яка набуває значення "істина" на цьому векторі. Тут p?i(t) О {pi(t), Шpi(t)}, а pi (i О 1, ..., q) – предикатний символ, який відповідає i-й компоненті вектора. І останнє погодження відносно позначень. Як і раніше, формулу, одержану із F(t) шляхом заміни всіх входжень t на t+k (k О Z), будемо позначати F(t+k).
Теорема 1.3 (про специфікацію). Нехай A – неініціальний циклічний S-автомат із станами q1, ..., qn, а F1(t), ..., Fn(t) – такі 0-обмежені формули, що для всіх i = 1, ..., n виконуються такі
умови:
1) Ri ЗPi № Ж, де Ri – множина зворотних надслів, яка задається формулою Fi(t), а Pi – множина зворотних надслів, представлених станом qi;
2) Ri З Rj = Ж при i № j;
3) якщо s – позначка переходу з qi в qj, то RiЧs Н Rj;
4) кожне Ri або відкрите, або замкнуте, або є перетином чи об'єднанням відкритої і замкнутої множин.
Тоді формула F = "t(Fi(t-1) & ), де mi – число переходів у автоматі A із стану qi, а (t) – елементарна кон'юнкція, яка відповідає позначці sij j-го переходу із стану qi, специфікує автомат A.
Якщо зв'язок теореми 1.3 з проблемою аналізу автомата досить прозорий, то побудова процедури синтезу на основі цієї теореми потребує додаткових пояснень.
Визначення 1.11. Нехай формула F має вигляд "t(Fi(t-1) & ), де Fi(t-1) – такі (-1)-обмежені формули, що при i № j формула Fi(t)&Fj(t) тотожно хибна, fij(t) – елементарні кон'юнкції атомарних формул вигляду p(t) або їхніх заперечень. Формула F називається нормальною формою, якщо для кожного i = 1, ..., n і кожного j = 1, ..., mi знайдеться таке k О {1, ..., n}, що формула "t(Fi(t-1) & fij(t) ® ® Fk(t)) загальнозначима.
Зауважимо, що вимога загальнозначимості останньої формули відповідає умові 3) теореми 1.3.
У основі метода синтезу автомата лежить наступне твердження.
Твердження 1.1. Для будь-якої 0-обмеженої несуперечної формули мови Lmax існує еквівалентна їй нормальна форма.
Нехай Ri, як і раніше, позначає множину зворотних надслів, які задаються формулою Fi(t). Очевидно, що для нормальної форми умови 2) і 3) теореми виконуються. Якщо крім того виконуються і умови 1) і 4), то нормальна форма формули F однозначно визначає автомат, який співпадає з автоматом, що специфікується формулою F. Вибір підмножини мови Lmax здійснюється так, щоб у одержаній мові для будь-якої формули вигляду F(t) існувала еквівалентна їй нормальна форма, для якої виконується умова 4). У цьому випадку для побудови автомата, що специфікується формулою, достатньо для деяких станів перевірити, чи виконується умова 1).
Нехай W – сигнатура одномісних предикатних символів, а Var – множина предметних змінних. Серед формул мови Lmax виділимо два класи, які назвемо t-формулами і 0-формулами. Усяка t-формула є формулою з однією вільною змінною, а 0-формулу одержуємо з t-формули F(t) (t О Var) підстановкою t = 0.
Поняття t-формули визначається наступним способом.
1. Атомарна формула вигляду p(ti - k), де p О W, ti О Var, k О N, є елементарною формулою.
2. Якщо F1(t) і F2(t) – елементарні формули, то ШF1(t), F1(t) Ъ F2(t), F1(t) & F2(t), F1(t) ® F2(t) є також елементарними формулами.
3. Усяка елементарна формула є простою формулою.
4. Для k1, k3 О N, k2 О Z, якщо F0(ti) і F2(tj) – елементарні формули, а F1(ti) – проста формула, то $?ti(ti Ј t - k1)&F0(ti)&F1(ti) & "tj((ti + k2 Ј tj Ј t - k3) ®F2(tj)) – також проста формула.
5. Усяка проста формула є t-формулою.
6. Якщо F1(t), F2(t) – t-формули, то ШF1(t), F1(t)ЪF2(t), F1(t)&F2(t), F1(t) ®F2(t) – також
t-формули.
7. Інших t-формул, окрім тих, що одержані у відповідності з 1 – 6, немає.
Індукцією за
