Обчислювальні методи верифікації темпоральних обмежень цілісності в процесі управління змінами в онтологіях

Размещено на http://www.allbest.ru/

Харківський національний університет імені В. Н. Каразіна

УДК 519.688:004.82:621.3.049.77

Обчислювальні методи верифікації темпоральних обмежень цілісності в процесі управління змінами в онтологіях

01.05.02 - математичне моделювання та обчислювальні методи

АВТОРЕФЕРАТ

дисертації на здобуття наукового ступеня

кандидата технічних наук

Кеберле Наталія Геннадіївна

Харків 2011

Дисертацією є рукопис.

Робота виконана в Запорізькому національному університеті Міністерства освіти і науки України.

Науковий керівник кандидат фізико-математичних наук, доцент

Єрмолаєв Вадим Анатолійович,

доцент кафедри інформаційних технологій

Запорізького національного університету

Офіційні опоненти: доктор фізико-математичних наук, професор

Глибовець Микола Миколайович,

завідувач кафедри інформатики,

декан факультету інформатики

Національного університету

“Києво-Могилянська академія” кандидат технічних наук, доцент

Хайрова Ніна Феліксовна, докторант кафедри інтелектуальних комп'ютерних систем Національного технічного університету “Харківський політехнічний інститут”

Захист відбудеться “ 25 ” травня 2011 року о 15.30 годині на засіданні спеціалізованої вченої ради Д 64.051.09 Харківського національного університету імені В. Н. Каразіна за адресою: 61077, м. Харків, пл. Свободи, 4, ауд. 6-52.

З дисертацією можна ознайомитись у Центральній науковій бібліотеці Харківського національного університету імені В.Н.Каразіна за адресою: 61077, м. Харків, пл. Свободи, 4.

Автореферат розісланий “ 15 ” квітня 2011 року.

Вчений секретар спеціалізованої вченої ради С.І. Шматков

управління верифікація темпоральний

АНОТАЦІЯ

Кеберле Н. Г. Обчислювальні методи верифікації темпоральних обмежень цілісності в процесі управління змінами в онтологіях. - Рукопис.

Дисертація на здобуття наукового ступеня кандидата технічних наук за спеціальністю 01.05.02 - математичне моделювання та обчислювальні методи. - Харківський національний університет імені В. Н. Каразіна. Харків, 2011 р.

Дисертація присвячена вдосконаленню засобів перевірки якості моделей знань, поданих у вигляді онтологій, при модифікації. Розроблено формальний апарат моделювання динамічних предметних областей у онтологіях, що здатен підвищити ефективність процесу технічної підготовки виробництва в цілому за рахунок зменшення кількості помилок при модифікації онтологій.

Запропоновано формальну модель динаміки знань про предметну область враховує темпоральну структуру, в межах якої розвивається динамічна предметна область. Розроблено метричні темпоральні логічні числення для формального подання моделі динаміки знань. Для розроблених числень на основі методу семантичних табло побудовано методи перевірки виконуваності формул. Формалізовано поняття темпорального обмеження цілісності в межах моделі динаміки знань. Розроблено обчислювальний метод верифікації темпоральних обмежень цілісності, який базується на методах перевірки виконуваності формул метричних темпоральних числень. Запропоновані моделі та методи використано для перевірки якості моделей знань в процесі управління змінами в онтологіях інформаційних систем підтримки технічної підготовки виробництва.

Розроблено прототип програмного комплексу підтримки процесу автоматизованої верифікації темпоральних обмежень цілісності, заданих на етапі специфікації модифікацій у процесі управління змінами в онтологіях.

Ключові слова: обчислювальні методи, концептуалізація динамічної предметної області, онтологія, метрична темпоральна логіка, темпоральне обмеження цілісності, машина логічного виводу.

АННОТАЦИЯ

Кеберле Н. Г. Вычислительные методы верификации темпоральных ограничений целостности в процессе управления изменениями в онтологиях. - Рукопись.

Диссертация на соискание ученой степени кандидата технических наук по специальности 01.05.02 - математическое моделирование и вычислительные методы. - Харьковский национальный университет имени В. Н. Каразина. Харьков, 2011 г.

Диссертация посвящена усовершенствованию средств проверки качества моделей знаний при модификации. Разработан формальный аппарат моделирования динамических предметных областей в онтологиях, способный повысить эффективность процесса технической подготовки производства в целом за счёт уменьшения количества ошибок при модификации онтологий.

Анализ существующих средств поддержки процесса накопления и уточнения моделей знаний о процессах технической подготовки производства показал, что эффективность технической подготовки производства в целом может быть повышена за счёт применения более совершенных средств проверки качества моделей знаний, учитывающих динамику процессов технической подготовки производства.

Предложена новая модель динамики знаний, основанная на множестве версий онтологии, упорядоченных в заданной темпоральной структуре, и на множестве темпоральных ограничений целостности. Уточнение свойств темпоральной структуры позволяет рассматривать разные модели поведения динамической предметной области. В частности, для задач управления изменениями в онтологиях рассмотрено использование дискретной линейной в прошлое и в будущее темпоральной структуры, в которой каждый момент времени соответствует новой версии онтологии.

Разработаны метрические темпоральные логические исчисления для формального представления модели динамики знаний о предметной области, для которых на основании метода семантических табло построены методы проверки выполнимости формул.

Формализовано понятие темпорального ограничения целостности в рамках модели динамики знаний. Разработанный вычислительный метод верификации темпоральных ограничений целостности основан на методах проверки выполнимости утверждений метрических темпоральных исчислений.

Разработан прототип программного комплекса поддержки процесса верификации темпоральных ограничений целостности, заданных на этапе спецификации модификации в процессе управления изменениями в онтологиях. Прототип программного комплекса позволяет выполнять набор функций, связанных с упрощением темпорального ограничения целостности, проверкой выполнимости и логической истинности темпорального утверждения, формализующего темпоральное ограничение целостности, верификацией набора темпоральных ограничений целостности на заданном архиве версий онтологий.

Ключевые слова: вычислительные методы, концептуализация динамической предметной области, онтология, метрическая темпоральная логика, темпоральное ограничение целостности, машина логического вывода.

ABSTRACT

Keberle N. G. Computational methods of temporal integrity constraints verification in ontology change process. - Manuscript.

The thesis on competition of scientific degree of candidate of the technical sciences on the specialty 01.05.02 - mathematical simulation and computing methods. - V. N. Karazin Kharkiv National University. - Kharkiv. - 2011.

The thesis is dedicated to the improvement of the ontology change management process by means of the formal verification of temporal integrity constraints in terms of proposed metric temporal logic approach, aiming at ontology development efficiency increase.

Temporal integrity constraints elicited from a dynamic domain and formalized with the help of temporal logics allow controlling the process of ontology change. Formally defined, such constraints have to be checked formally and automatically, avoiding mistakes of manual inspection.

Software prototype supporting the verification process of a set of temporal integrity constraints over ontology versions archive is designed.

Key words: computational methods, conceptualization of a dynamic domain, ontology, metric temporal logic, temporal integrity constraint, reasoning engine.

1. ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми дисертаційної роботи. Технічна підготовка виробництва (ТПВ) передбачає виконання комплексу заходів, що включають конструкторську та технологічну підготовку, успішність яких зумовлена застосуванням інформаційних систем підтримки (ІСП). Для високотехнологічних наукоємних галузей промисловості важливим є забезпечення якості моделей, що використовуються у ТПВ. Проведення технічного контролю якості у межах ТПВ вимагає включення до ІСП ТПВ відповідних засобів.

Оцінка якості використаних моделей базується на отриманні різноманітних знань та даних. Забезпечення адекватних формалізованих моделей подання знань є важливим фактором для забезпечення ефективності процесів ТПВ.

Структура та номенклатура знань про продукцію та процеси у ІСП ТПВ зазнає змін з часом, тому ІСП ТПВ включає в себе процес накопичення та уточнення моделей знань про ТПВ. Метою цього процесу є забезпечення переходу від попередніх до наступної (уточненої) версії моделі таким чином, щоб забезпечити її якість за наступними контрольованими признаками: внутрішня несуперечливість уточненої моделі; її несуперечливість відносно до інших моделей, використаних в ІСП; коректність уточненої моделі відносно набору вимог, обумовлених поточними особливостями ТПВ. Водночас, складність моделей знань про процеси ТПВ з урахуванням їх динамізму призводить до цілого комплексу проблем перевірки несуперечливості відповідних ІСП. Рішенню задач математичного, алгоритмічного і програмного забезпечення процесу накопичення та уточнення моделей знань у ІСП ТПВ присвячена дана дисертаційна робота.

Застосування логічних моделей знань у вигляді онтологій при створенні ІСП ТПВ надає можливість використання формальних засобів їх подання і перевірки несуперечливості. У розвитку досліджень з використання онтологій для моделювання складних систем помітний внесок зробили роботи М. Вулдриджа, В. І. Городецького, Н. Дженнінгса, В. А. Єрмолаєва, В. Мажика, К. Сікари та ін. Урахування динаміки предметної області та подання динамічних предметних областей у онтологіях, а також їх формально-мовна підтримка розглядалися А. Артале, М. Захарящевим, К. Лутцем, Ф. Уолтером, Е. Франконі, В. Я. Терзіяном, Є. І. Кучеренком та ін. Найбільш часто використовуваним підходом до оцінки коректності системи є верифікація моделей цієї системи за допомогою засобів темпоральної логіки. В розвитку методів формальної верифікації важливий внесок внесли дослідження Л. Лемпорта, А. Пнуелі, А. Сістла, Е. Кларке, Дж.-П. Катоена, М. М. Глибовця та ін. У даній роботі цей підхід адаптується і використовується для формальної верифікації моделей подання динаміки знань.

У даний час розроблено декілька моделей процесів управління змінами в онтологіях. Аналіз існуючих моделей показав, що в них є недоліки, які не дозволяють своєчасно проводити аналіз вимог до модифікації онтологій та їх уточнення. Одним з таких недоліків є відсутність формальних засобів подання обмежень цілісності, обумовлених предметною областю, на етапі специфікації модифікацій, та методів формальної верифікації заданих обмежень цілісності, що спричиняє зайві витрати часу. На підставі аналізу зроблено висновок про те, що наукова задача, яка полягає в удосконаленні засобів перевірки якості онтологій при модифікації є актуальною.

Зв'язок роботи з науковими програмами, планами, темами. Робота над дисертацією проводилася автором на кафедрі інформаційних технологій Запорізького національного університету в межах науково-дослідної теми “Розробка математичних моделей та методів опису і взаємодії елементів єдиного інформаційного простору в інтегрованій мережі ВУЗів на базі принципів діакоптики і архітектур типу майстер-агент” (№ ДР 0199У001571).

Мета і задачі дослідження. Мета роботи полягає в підвищенні ефективності процесу технічної підготовки виробництва за рахунок зменшення кількості помилок при модифікації моделей знань, поданих у вигляді онтологій, у інформаційних системах підтримки технічної підготовки виробництва, шляхом використання розроблених автоматизованих засобів верифікації обмежень цілісності.

Об'єктом дослідження є процес управління змінами в онтологіях у інформаційних системах підтримки технічної підготовки виробництва.

Предметом дослідження є методи верифікації темпоральних обмежень цілісності в процесі управління змінами в онтологіях.

Методи досліджень. Теоретичною основою роботи є принципи та методи теорії множин, логіки, теорії обчислювальної складності, теорії формальних систем, системного аналізу. Для побудови програмних засобів було використано принципи об'єктно-орієнтованого програмування.

Для досягнення поставленої мети дослідження в роботі сформульовані задачі:

дослідити особливості процесу управління змінами в онтологіях для інформаційних систем;

розробити модель динаміки знань про предметну область інформаційної системи на базі множини версій моделі онтології та множини темпоральних обмежень цілісності;

розробити обчислювальні методи верифікації темпоральних обмежень цілісності на множині версій моделі онтології, та методику їх застосування в процесі управління змінами в онтологіях;

розробити прототип програмного комплексу, призначеного для підтримки автоматизованої верифікації темпоральних обмежень цілісності в процесі управління змінами в онтологіях, та впровадити цей комплекс у ІСП ТПВ.

Наукова новизна отриманих результатів. На основі виконаних теоретичних досліджень та проведених експериментів отримано нове рішення важливої наукової задачі - удосконалення засобів перевірки якості онтологій при модифікації шляхом проведення формальної верифікації темпоральних обмежень цілісності в термінах запропонованого формально-логічного апарата моделювання, призначеного для використання у процесі управління змінами в онтологіях, що дозволяє підвищити ефективність процесу технічної підготовки виробництва за рахунок зменшення кількості помилок при модифікації онтологій.

У межах поставленої задачі одержано наступні наукові результати:

а) уперше на основі теорії формальних систем і теорії множин запропоновано формальну модель, засоби формального подання та методи перевірки виконуваності формул онтології динамічної предметної області, які відрізняються від існуючих урахуванням властивостей темпоральної структури, в межах якої проходить розвиток предметної області, що створило підґрунтя для реалізації методів верифікації темпоральних обмежень цілісності на множині версій моделі онтології;

б) уперше розроблено метод верифікації темпоральних обмежень цілісності, що базується на запропонованих методах перевірки виконуваності формул онтології динамічної предметної області, що дозволило застосувати формальні засоби перевірки обмежень цілісності в процесі управління змінами в онтологіях;

в) набули подальшого розвитку методи моделювання динаміки знань про предметну область завдяки формалізації темпоральних обмежень цілісності, обумовлених предметною областю, що дозволяє підвищити ефективність процесу технічної підготовки виробництва за рахунок зменшення кількості помилок при модифікації онтологій;

г) вдосконалено процес управління змінами в онтологіях за рахунок використання моделі динаміки знань, що дозволило застосувати знання про обмеження, обумовлені динамікою предметної області;

д) вдосконалено засоби перевірки якості онтологій при модифікації за рахунок використання розробленого методу верифікації темпоральних обмежень цілісності.

Практичне значення отриманих результатів. Запропоновані моделі і методи дозволяють науково обґрунтовано підходити до процесів створення та уточнення моделей знань у інформаційних системах підтримки ТПВ, та у сукупності вдосконалюють засоби перевірки якості онтологій при модифікації.

Запропонований обчислювальний метод перевірки виконуваності формул онтології динамічної предметної області доведено до рівня впровадження програмного забезпечення. Метод використовується при перевірці несуперечливості онтології динамічної предметної області.

Запропонований обчислювальний метод верифікації темпоральних обмежень цілісності доведено до рівня впровадження програмного забезпечення. Метод використовується в процесі управління змінами в онтологіях при перевірці обмежень цілісності, залежних від предметної області, та заданих з метою контролю над модифікаціями онтологій статичної предметної області.

Розроблені прототип програмного комплексу (машина виводу Pellet-MeT) та формальна мова OWL-MeT опису онтологій динамічної предметної області дозволяють скоротити час і трудомісткість уточнення онтологій у ІСП ТПВ.

Достовірність отриманих результатів підтверджена успішним застосуванням розробленого прототипу в процесі управління змінами в онтологіях інформаційної системи управління продуктивністю процесів проектування мікроелектронних пристроїв, яка розроблена у дослідницькому промисловому проекті PSI (Performance Simulation Initiative) у межах співробітництва з компанією Cadence Design Systems GmbH, ФРН (відділ VCAD EMEA, довідка від 01.12.2009 р.).

Особистий внесок здобувача. Усі основні наукові положення, результати, висновки та рекомендації дисертаційної роботи отримані автором самостійно. З публікацій, що написані в співавторстві, використано лише ті результати, що отримані автором особисто: побудова метричної темпоральної логіки дескрипцій і аналіз її властивостей, побудова структури мови OWL-MeT [2]; застосування метричної темпоральної логіки дескрипцій як засобу формулювання тверджень про зміни у онтологіях [9]; вибір програмних засобів реалізації машини логічного виводу для OWL-MeT, реалізація алгоритмів логічного виводу для OWL-MeT [10].

Апробація результатів дисертації. Результати дослідження доповідались та обговорювались на міжнародних науково-практичних конференціях: III Міжнародна науково-практична конференція „Математичне та програмне забезпечення iнтелектуальних систем” (Дніпропетровськ, 16-18 листопада, 2005), IV Міжнародна науково-практична конференція „Математичне та програмне забезпечення iнтелектуальних систем” (Дніпропетровськ, 15-17 листопада, 2006), III Міжнародна конференція „Теоретичні та прикладні аспекти побудови програмних систем” (Київ, 6-8 грудня, 2006), International Conference „Dynamical System Modeling and Stability Investigation” (Kyiv, May 22-25, 2007), Workshop on Ontology Dynamics IWOD'2007 in conjunction with 4th European Semantic Web Conference ESWC'2007 (Innsbruck, June 4-7, 2007), Міжнародна науково-практична конференція „Веб-програмування та Інтернет-технології (WebConf09)” (Мінськ, 8-10 червня, 2009), 6th Workshop on Web Ontology Language Experiences and Directions OWLED'2009 in conjunction with International Semantic Web Conference ISWC'2009 (Washington DC, Oct. 23-24, 2009) та на наукових семінарах кафедри інформатики Національного університету ”Києво-Могилянська академія” та кафедри теоретичної та прикладної інформатики Харківського національного університету імені В.Н. Каразіна.

Публікації. Результати дисертації відображені у 13 публікаціях: 6 статей в збірниках наукових праць (з них 5 без співавторів), 3 статті у матеріалах конференцій, 4 тези доповідей на конференціях.

Структура й обсяг дисертації. Робота складається зі вступу, чотирьох розділів, висновків, списку використаних джерел та додатків. Вона містить 210 сторінок, з яких 149 сторінок основного тексту, 2 табл. на окремих аркушах, список використаних джерел з 157 найменувань на 17 сторінках, 10 додатків на 42 стор.

2. ОСНОВНИЙ ЗМІСТ РОБОТИ

У вступі обґрунтовано актуальність теми дисертаційної роботи, зазначено зв'язок роботи з науковими темами, сформульовано мету і задачі дослідження, визначено об'єкт, предмет і методи дослідження, показано наукову новизну та практичне значення отриманих результатів, наведено інформацію про практичне використання, апробацію та їх висвітлення у друкованих працях.

У першому розділі розглянуто напрямки вирішення основних проблем моделювання знань у ІСП ТПВ в умовах динаміки предметної області. Зазначено, що ефективність ТПВ залежить від якості моделей знань про предметну область, використаних у ІСП ТПВ. Засоби технічного контролю якості моделей знань в умовах динаміки предметної області вимагають приділення уваги процесам уточнення знань у інформаційних системах. Структурна і семантична складність предметних областей, притаманна сучасним ІСП ТПВ у високотехнологічних галузях промисловості, призводить до використання логічних моделей знань у вигляді онтологій. Проведений аналіз існуючих підходів до управління змінами в онтологіях показав, що вони залишають відкритими цілий ряд питань: відсутність формальних засобів подання обмежень цілісності, обумовлених предметною областю, що призводить до помилок реалізації модифікацій інженерами знань; відсутність формальних методів верифікації заданих обмежень цілісності, що призводить до виконання семантично некоректних або зайвих модифікацій та їх розповсюдження на залежні елементи інформаційної системи.

Аналіз дозволив визначити наступні вимоги до засобів управління змінами в онтологіях: використання декларативних засобів для подання обмежень цілісності, обумовлених предметною областю; забезпечення можливості оперувати при поданні обмежень цілісності різними версіями моделі онтології; залучення формальних методів перевірки коректності моделей онтологій відносно заданих обмежень.

Сформульовано загальну математичну постановку задачі дослідження: дана динамічна предметна область , розробити модель онтології для , формальну мову для подання такої моделі онтології, та обчислювальні методи верифікації обмежень, обумовлених особливостями і заданих у , відносно онтологій для . Забезпечити перевірку якості версії онтології при модифікації за допомогою методів верифікації обмежень. Критерієм якості виступає відсоток виконаних у онтології обмежень, обумовлених предметною областю .

У другому розділі в рамках рішення загальної задачі розроблено математичний апарат моделювання динамічних предметних областей.

Динамічна предметна область - це предметна область, що зазнає зміни з часом. Часова складова процесу зміни вимагає визначення темпоральної структури.

Темпоральна структура (або часовий фрейм, П. Блекберн) - це кортеж

, (1)

де - множина моментів часу, - відношення передування у часі.

Залежно від властивостей множини та відношення можна отримати різні моделі часу. Наприклад, відношення із властивостями рефлексивності та транзитивності відповідає лінійному дискретному часу, а відношення із властивістю щільності - неперервному часу.

Для моделювання динамічної предметної області у інформаційній системі в роботі розглядаються тільки дискретні темпоральні структури, з урахуванням припущення, що зміна у предметній області не має тривалості і відбувається миттєво. Тоді кожний момент часу відповідає саме моменту появи оновленої предметної області, а множина є множиною всіх таких моментів, коли з'являється оновлена предметна область. Таким чином, темпоральна структура відповідає набору версій предметної області, і факт, що дві версії є сусідніми, не означає, що їх появу розділяє однаковий проміжок реального календарного часу.

Основою апарата моделювання динамічних предметних областей є поняття концептуалізації. З позицій семіотичного моделювання, концептуалізація - сукупність прагматично значущих об'єктів, понять, їх властивостей та відношень, визначених у предметній області. Розрізняння екстенсіональної та інтенсіональної концептуалізації (згідно з Н. Гуаріно, Дж. МакКарті та П. Хайєсом) для динамічних предметних областей отримує наступні формулювання.

Екстенсіональна концептуалізація динамічної предметної області - це кортеж

, (2)

де - екстенсіональна концептуалізація в момент часу , - момент часу моделювання, - скінченна або зчисленна множина об'єктів у предметній області,

- скінченна або зчисленна множина відношень у предметній області, - темпоральна структура.

Інтенсіональна концептуалізація динамічної предметної області - це кортеж

, (3)

де - скінченна або зчисленна множина концептуальних відношень, що спостерігаються у просторі предметної області , - множина можливих «світів», - темпоральна структура.

Формальна модель онтології динамічної предметної області - це кортеж

(4)

де - онтологія, актуальна в момент часу , - темпоральна структура.

Уточнюючи властивості часу у темпоральній структурі можна визначати особливу поведінку моделі онтології, яка точніше відображає особливості змін у предметній області.

Модель онтології (4) надає основу для формалізації обмежень цілісності, що мають створюватися та перевірятися у процесі управління змінами в онтологіях на етапі специфікації модифікацій. Модель (4) дозволяє розглядати з єдиних позицій всі версії онтології, що були та будуть розроблені в межах конкретної інформаційної системи для заданої предметної області як елементи онтології динамічної предметної області. Таким чином, обмеження цілісності можуть враховувати елементи онтологій, актуальних в різні (або навіть у всі) моменти часу. Для формального подання таких вимог у інформаційних системах необхідно мати відповідні мовні засоби. Для цього використовуються формальні системи на основі темпоральних модальних логік.

Темпоральні логіки широко застосовуються як для опису поведінки динамічної системи у часі, так і для верифікації коректності станів такої системи в різні моменти або проміжки часу.

Нехай - темпоральна формальна мова. Темпоральне обмеження цілісності - правильно побудована формула , яка формалізує обмеження на елементи моделі (4). Задача верифікації темпорального обмеження цілісності полягає у перевірці виконуваності в моделі відносно вказаного моменту часу, тобто

,

де .

Використання знань, з урахуванням їх динаміки, про предметну область у інформаційних системах, вимагає вдосконалення існуючих моделей подання знань.

Модель динаміки знань про предметну область інформаційної системи - це кортеж

(5)

де - онтологія, актуальна в момент часу , - темпоральна структура, - темпоральна формальна мова з множиною правильно побудованих формул , - скінченна множина темпоральних обмежень цілісності.

У розділі обґрунтовано доцільність використання топологічних і метричних властивостей часу для формалізації темпоральних обмежень цілісності.

У третьому розділі описано використання моделі (4) у методі верифікації темпоральних обмежень цілісності. Метод верифікації темпоральних обмежень цілісності полягає у наступному:

1. Створення темпорального обмеження цілісності у вигляді
-формули .

2. Перевірка логічної істинності на темпоральній структурі (1),
|= .

3. Перевірка виконуваності в моделі (4) у вказаний момент часу.

Перевірка логічної істинності та виконуваності формул розглядається для трьох послідовно введених метричних темпоральних формально-логічних систем: пропозиційних PTC(MT) і HPTC(MT) з кванторами тільки по моментах часу, та на їх базі - фрагменту числення предикатів першого порядку з унарними та бінарними предикатними буквами (відомого як логіка дескрипцій) - для подання онтологій динамічних предметних областей. В розділі досліджуються логічні властивості цих систем - повнота, несуперечливість, розв'язуваність, приналежність до класу складності задачі перевірки виконуваності формул.

Запропоновані метричні темпоральні системи побудовано для дискретного лінійного необмеженого в майбутнє і в минуле часу, моменти часу впорядковані за допомогою рефлексивного і транзитивного відношення порядку.

Відповідна темпоральна структура визначається як

, (6)

де - зчисленна множина моментів часу, ізоморфна множині цілих чисел, - має властивості лінійності в майбутнє і в минуле, нескінченності в майбутньому і в минулому, рефлексивності та транзитивності, тобто є відношенням нестрогого порядку на .

Алфавіт PTC(MT) складається з множини пропозиційних змінних ; пропозиційних зв'язок ; множини темпоральних операторів Fn, Pn (Fn - « через n моментів часу буде так, що…», Pn - « n моментів часу назад було так, що…»); множини предикатних букв PRED, яка містить хоча б « = »; множини термів -натуральних чисел і «0», числових змінних, і , де - натуральні числа, «0» або числові змінні, - бінарні операції «+» та «-».

Множина правильно побудованих формул вичерпується такими формулами: всі пропозиційні змінні; якщо і - формули, то , , , , є формулами PTC(MT); якщо « = » - предикатна буква, якій відповідає бінарний предикат рівності, заданий над цілими числами,
і - терми, то є формулою; якщо - формула, то ,,, , - також є формулами PTC(MT).

Формули PTC(MT) інтерпретуються у моделях Кріпке з метрикою

M , (7)

де T - непуста множина можливих «світів» - моментів часу, є бінарними відношеннями досяжності на T, відповідно у відношенні майбутнього і минулого, - функція інтерпретації, яка показує, в яких станах кожний пропозиційний символ приймає значення «істина», - функція інтерпретації предикатних букв, - метрика на множині T.

Система аксіом, які, за Прайором, формально задають властивості (6)
і були додані до пропозиційної системи L4, є такою (наведені аксіоми, що контролюють роботу темпоральних операторів у відношенні майбутнього, аксіоми для минулого є дзеркальними):

- логічна однорідність у майбутнє;

;

;

;

;

- необмеженість у майбутнє;

- відсутність вітвлення у майбутньому;

- транзитивність у майбутньому;

-ітерування темпоральних модальностей.

Ця система аксіом є незалежною від аксіом пропозиційного числення, а обрана темпоральна структура (5) відповідає моделі модальної системи S4.

Нехай - довільна формула PTC(MT). Доведено, що, якщо вивідна ( ), то вона є логічно істинною ( ) (Теорема 1), PTC(MT) несуперечлива (Теорема 2), якщо , то (Теорема 3), PTC(MT) повна (Теорема 4). Для доведення використовувалися поняття негативної нормальної форми (н.н.ф.) та запропонованої у роботі FnPn-нормальної форми, в якій темпоральні оператори стоять у підформулах першими.

Метод перевірки виконуваності формули засновано на методі семантичних табло Бета-Кріпке - розроблено набір правил (див. Табл.1) для побудови конструкції , що складається з усіх ланцюгів списків підформул формули .

Засіб маркування *F, *P списків формул у ланцюгу було застосовано
для запобігання нескінченному використанню - та -правил (нескінченний ланцюг можна отримати при побудові конструкції для, наприклад, ).

Лема. Для довільної формули PTC(MT) процес побудови конструкції завжди завершується після скінченного числа кроків.

Алгоритм побудови конструкції є таким:

Застосовується 0 - правило для створення списку .

Застосовується - правило для відокремлення диз'юнкцій.

Застосовується - правило для відокремлення кон'юнкцій.

Застосовуються та - правила створення нових списків формул.

Застосовуються - та - правила, що породжують нові списки формул.

Застосовуються -, - правила, що доповнюють списки формул.

Застосовуються -, - правила, що доповнюють списки формул.

Процес побудови конструкції зупиняється у двох випадках: якщо у кожному ланцюгу є список , що містить і , і ; якщо такий ланцюг вже є у конструкції.

Таблиця 1 Правила побудови семантичного табло для перевірки виконуваності формули PTC(MT) (показано для операторів, що діють у відношенні майбутнього)

Назва правила	Умови та слідства застосування правила
- правило	Умова:	1. 2. 3.
	Дія:	1. Якщо не існує списку , то такий список створюється і нова формула додається до 2. Якщо список існує, то додається до 3. Між та встановлюється відношення . 4. Якщо існує список , який є попередником відносно , і такий, що , то позначається *F.
- правило	Умова:	1. 2. 3. не позначена *F
	Дія:	Або Або нова формула додається до списку
-правило	Умова	1. 2.
	Дія	1. 2. Для кожного списку , такого що відношення встановлено,

З'ясовано, що PTC(MT) розв'язувана (Теорема 5), зведення до FnPn-н.ф. виконується за поліноміальний час (Теорема 6), і що задача перевірки виконуваності формули PTC(MT) належить до PSPACE-повних на довільному та транзитивному фреймі, і до NP-повних на лінійному фреймі (Теорема 7).

Мова, що лежить у основі PTC(MT), не дає можливості вказати у формулі явно конкретні моменти часу, відносно яких буде оцінюватися виконуваність підформул. Таким чином, формули PTC(MT) не мають прив'язки до конкретної множини моментів темпоральної структури (6), і виконуваність будь-якої формули оцінюється взагалі для будь-якої множини моментів . Метричне гібридне пропозиційне числення тверджень HPTC(MT) використовує гібридний оператор виконуваності @ для звернення до конкретних моментів часу у формулах. Семантика оператора виконуваності @ полягає в тому, що формула означає: “ виконується (має модель) у конкретному стані, означеному а”.

Алфавіт HPTC(MT) складається з алфавіту PTC(MT) та непустої множини темпоральних номіналів . Кожен номінал представляє ім'я деякого можливого моменту часу з . Множина термів HPTC(MT) співпадає із множиною термів PTC(MT), а множина правильно побудованих формул доповнюється формулами та а. Функція відповідності відображає множину темпоральних номіналів у множину цілих чисел.

Для побудованого числення проведено аналіз логічних властивостей: HPTC(MT) несуперечлива (Теорема 8), повна (Теорема 9), розв'язувана (Теорема 10). Розроблено набір правил табло для побудови конструкції, за допомогою якої можливо перевірити виконуваність формули HPTC(MT), які доповнюють правила табло PTC(MT) правилами обробки конструкцій та а. Доведено зведення формули HPTC(MT) до @FnPn-н.ф. за поліноміальний час (Теорема 11). Задача перевірки виконуваності формули HPTC(MT) належить до класу EXPTIME-важких на як довільному фреймі, так і на транзитивному фреймі (Теорема 12).

Темпоральна логіка дескрипцій є композицією логік - логіки дескрипцій з номіналами, та - спрощеним варіантом логіки HPTC(MT) без числових змінних по моментах часу та без предикатів по цим змінним, з використанням підстановок , .

Алфавіт мови складається з наступних множин букв: нетемпоральних атомарних концептів до яких відносяться також наперед задані концепти top и bottom; нетемпоральних складених концептів ; зв'язків для нетемпоральних концептів , дужок {,}, і кванторів ; ролей ; темпоральних концептів ; звичайних номіналів ; темпоральних номіналів ; - натуральних чисел і числа «0»; примітивних зв'язок для темпоральних концептів і формул intersection, union, not, @, subclassof, equivalent, « : » ; модальностей future n, past n, somefuture, somepast, allfuture, allpast.

У мові дозволені два види концептів - нетемпоральні та темпоральні, які будуються за допомогою таких конструкторів: якщо , top, bottom - атомарні нетемпоральні концепти, - нетемпоральні концепті, - роль, - номінал, то множина нетемпоральних концептів складається з концептів , top, bottom, E u F, E t F, E, R.E, R.E , {o}; якщо - нетемпоральний концепт, - темпоральні концепти, - темпоральний номінал, то множина темпоральних концептів складається з концептів виду , {a}, C intersection D, C union D, not C, C@{a}, future n C, past n C, somefuture C, somepast C, allfuture C, allpast C. Таким чином, множина темпоральних концептів включає множину нетемпоральних концептів.

Правильно побудовані формули складаються з: усіх елементів множини темпоральних концептів; формул виду C equivalent D, C subclassof D, a:C, not , union , intersection , де - темпоральні концепті, - темпоральний номінал, , - правильно побудовані формули.

У темпоральні та гібридний оператори застосовуються тільки до темпоральних концептів. Конструктори ролей для темпоральних концептів не застосовуються.

інтерпретується в моделі Кріпке

M, (8)

де - множина можливих «світів» - моментів часу, - множина екземплярів у k-му можливому «світі», - метрика на ,

- відношення досяжності, пов'язані умовою конверсії для можливих світів u та w, - функція інтерпретації, та - функція гібридної оцінки.

Інтерпретація ставить у відповідь кожному деяку -інтерпретацію . Функція відповідності (так, як і для HPTC(MT)) відображає множину темпоральних номіналів у множину цілих чисел. Для темпорального номіналу {a}, функція гібридної оцінки ставить у відповідь кожному {a} унікальний можливий світ - елемент .

Інтерпретація специфічних конструкцій є такою:

Для даної моделі M і даного світу i справедливі наступні твердження про виконуваність:

M, i |= future n C	т.і.т.т.к.	M, i +n |= C
M, i |= past n C	т.і.т.т.к.	M, i - n |= C
M, i |= somefuture C	т.і.т.т.к.	: M, j |= C
M, i |= somepast C	т.і.т.т.к.	: M, j |= C
M, i |= allfuture C	т.і.т.т.к.	: M, j |= C
M, i |= allpast C	т.і.т.т.к.	: M, j |= C
M, i |= C@{a}	т.і.т.т.к.	M, Den(a) |= C

Теорема 13. розв'язувана.

Теорема 14. Проблема виконуваності формул EXPTIME-важка.

Метод перевірки виконуваності для - формулы також базується на методі семантичних табло , де - скінченна множина вузлів дерева, - відношення передування на вузлах, _ функція розмітки, яка ставить у відповідь кожному вузлу систему обмежень .

Для початкової формули корінь дерева, , пов'язано з системою , формула - немаркована, навіть якщо або . Правила обробки конструкцій -частини логіки є стандартними для логік дескрипцій.

Правила створення нової системи обмежень, які обумовлені -частиною логіки, показані у табл. 2.

Доведено, що процедура побудови табло для завершується після скінченного числа кроків (Теорема 15), ця процедура є несуперечливою (Теорема 16) і повною (Теорема 17).

Таблиця 2 Правила породження нової системи обмежень

Назва правила	Умови та слідства застосування правила
- правило	Умова:	1. 2.
	Дія:	1. Створюється новий вузол 2. Створюється нова система обмежень 3. ; 4. 5. 6.
- правило	Умова:	1. 2. Не існує вузла із системою обмежень або 3.
	Дія:	Якщо вузла не існувало, то 1. Створюється новий вузол 2. Створюється нова система обмежень 3. 4. ; 5.
		У іншому випадку 4'. ; 5'.

Четвертий розділ присвячено дослідженню застосування моделі (5) динаміки знань про предметну область у інформаційних системах підтримки ТПВ. Встановлено, що для використання розробленого математичного апарату необхідна розробка програмного комплексу, призначеного для автоматизації процесу верифікації темпоральних обмежень цілісності.

Розглянуто структуру та функції розробленого автором прототипу програмного комплексу - машини логічного виводу Pellet-MeT, призначеної для автоматизації процесу перевірки виконуваності формул онтології динамічної предметної області. У прототипі реалізовано наступні можливості: зчитування набору темпоральних обмежень цілісності, заданих у вигляді формул у запропонованій мові OWL-MeT, що реалізує логіку дескрипцій ; спрощення темпорального обмеження цілісності з використанням властивостей темпоральних логік з розділу 3; перевірка виконуваності формули у мові OWL-MeT з використанням алгоритму табло для з розділу 3; верифікація набору темпоральних обмежень цілісності на заданому архіві версій онтологій.

Методика верифікації темпоральних обмежень цілісності у процесі управління змінами в онтологіях полягає у наступному:

1. На етапі специфікації модифікацій у онтологіях - створити або відредагувати набір темпоральних обмежень цілісності.

2. На етапі кодування змін у онтологіях, після внесення змін - провести автоматизовану верифікацію набору темпоральних обмежень цілісності за допомогою запропонованого методу верифікації. Провести корекцію специфікації модифікацій, в залежності від результату верифікації.

Апробація запропонованої методики була проведена для предметної області “Продуктивність систем та процесів проектування мікроелектронних пристроїв“. Архів версій онтологій налічував 21 версію наборів онтологій PSI, створених протягом декількох років. Структура архіву відповідала лінійній дискретній обмеженій в майбутнє і в минуле темпоральній структурі.

Для оцінки ефективності використання верифікації темпоральних обмежень цілісності було розглянуто базовий процес управління змінами в онтологіях за Л. Стоянович та досліджено два показника: кількість повернень з етапу j на вже закінчений етап i (0<i<j) у зв'язку зі знаходженням на етапі j помилки, якої припустилися на етапі i; сумарна кількість людино-годин, яку було витрачено на кожному з етапів процесу управління змінами в онтологіях.

Об'єктом апробації виступив набір онтологій PSI версії 2.3.3. У першій групі розробників модифікації онтологій до версії 2.3.4 проводилися згідно зі специфікацією модифікацій на етапі кодування, а їх коректність та виконання у новій онтології обмежень, обумовлених предметною областю, перевірялися на етапі валідації вручну, за допомогою редактора онтологій. У другій групі на підставі специфікації модифікацій був створений набір темпоральних обмежень цілісності (у мові OWL-MeT), відповідно до моделі (5), на підставі особливостей динаміки предметної області. Логічна істинність всіх обмежень відносно темпоральної структури була автоматизовано перевірена у Pellet-MeT за допомогою методу перевірки виконуваності формул з розділу 3. Після кодування змін, на етапі валідації весь набір обмежень був автоматизовано верифікований відносно оновленого архіву версій онтологій, також за допомогою Pellet-MeT.

Якість онтологій визначалася як відношення кількості виконаних обмежень до загальної кількості заданих обмежень. В разі знаходження невиконаних обмежень, процес розробки повертався або на етап специфікації модифікацій (з редагуванням специфікації модифікацій), або на етап кодування (з редагуванням коду).

Проведений аналіз дозволив стверджувати, що використання моделі (5) сприяє зменшенню кількості помилок при модифікації онтології.

Під час аналізу першого показника було встановлено, що при використанні темпоральних обмежень цілісності на етапі специфікації модифікацій кількість повернень на цей етап зменшується за рахунок якості аналізу модифікацій.

У табл. 3 наведено порівняльні дані по кількості повернень на етап специфікації модифікацій з інших етапів процесу управління змінами в онтологіях у двох групах розробників.

Таблиця 3 Порівняльна кількість повернень на етап специфікації модифікацій

Етап процесу управління змінами у онтології	Кількість повернень на етап
	Група 1 (без т.о.ц.)	Група 2 (з т.о.ц.)
Визначення семантики модифікацій	12	3
Кодування (OWL)	11	3
Валідація	3	1

Оцінка другого показника дозволила стверджувати, що використання апарату темпоральних обмежень цілісності у процесі управління змінами в онтологіях знижає сумарно трудомісткість внесення змін до онтологій у ІСП ТПВ, що вимірюється в людино-годинах, на 10%.

Застосування темпоральних обмежень цілісності у процесі управління змінами в онтологіях не зменшує часових витрат на етапі специфікації модифікацій, оскільки в процесі роботи виконуються допоміжні дії - формулюється та узгоджується із специфікацією набір темпоральних обмежень цілісності, виконується їх верифікація, виправляються знайдені помилки у специфікації. Зменшення сумарного часу пов'язане зі зменшенням кількості повернень на попередні етапи та зі зменшенням часу на валідацію онтології.

У додатку А наведено доведення теореми про існування FnPn-нормальної форми для формули числення PTC(MT). У додатку Б наведено вигляд характеристичної форми конструкції для числення PTC(MT). У додатку В доведено теорему про приналежність задачі перевірки виконуваності формули числення PTC(MT) до класу EXPTIME-важких задач. У додатку Г наведено структуру -connection для метричної темпоральної логіки дескрипцій. У додатку Д наведено абстрактний синтаксис мови OWL-MeT у нотації Бекуса-Наура. У додатку Е наведено формальне відображення мови OWL-MeT в RDF граф. У додатку Ж описано словника конструкцій OWL-MeT у RDF Schema. У додатку З наведені експериментальні результати нормалізації для набору тестових онтологій та затрачений час на нормалізацію. У додатку И наведено затрачений час на роботу процедури поповнення та насичення системи табло для набору тестових онтологій. У додатку К наведено приклад тестової OWL-MeT онтології.

ВИСНОВКИ

У дисертації отримано нові науково обґрунтовані результати в області математичного моделювання та обчислювальних методів, що в сукупності вирішують важливу наукову задачу - удосконалення засобів перевірки якості онтологій при модифікації шляхом проведення формальної верифікації темпоральних обмежень цілісності в термінах запропонованого формально-логічного апарата моделювання, призначеного для використання на етапі специфікації модифікацій в онтологіях, що дозволяє підвищити ефективність процесу технічної підготовки виробництва за рахунок зменшення кількості помилок при модифікації онтологій.

В процесі виконання роботи отримано наступні наукові і практичні результати.

Сформульовано загальні вимоги до засобів управління змінами у моделях знань, поданих у вигляді онтологій, що використовуються в ІСП ТПВ. З урахуванням даних вимог проведено аналіз існуючих моделей процесу управління змінами в онтологіях, який показав, що вони не можуть повною мірою вирішувати задачі, які виникають на етапі специфікації модифікацій. Показано, що для підвищення ефективності ТПВ необхідно розробити формальний апарат моделювання динамічних предметних областей, призначений для побудови і верифікації обмежень цілісності, що мають виконуватися в процесі управління змінами в онтологіях.

Розроблено математичний апарат моделювання динамічних предметних областей. Запропоновано нову формальну модель онтології динамічної предметної області. Для задач управління змінами в онтологіях запропоновано використовувати дискретну лінійну в майбутнє і в минуле темпоральну структуру, в якій кожен момент часу відповідає новій версії онтології.

Розроблені метричні темпоральні логічні числення для формального подання моделі онтології динамічної предметної області, для яких на основі методу семантичних табло побудовані методи перевірки виконуваності формул.

Формалізовано поняття темпорального обмеження цілісності. Розроблено обчислювальний метод верифікації темпоральних обмежень цілісності, що базується на методах перевірки виконуваності формул метричних темпоральних числень.

Розроблено модель динаміки знань про предметну область інформаційної системи на базі множини версій моделі онтології та множини темпоральних обмежень цілісності.

Розроблено алгоритм верифікації темпоральних обмежень цілісності, заданих для множини версій моделі онтології, які є актуальними в різні проміжки часу.

Виконана експериментальна оцінка ефективності застосування розробленого обчислювального методу верифікації темпоральних обмежень цілісності в процесі управління змінами в онтологіях. Результати аналізу проведених експериментів вказують на підвищення ефективності ТПВ у середньому на 10%.

Розроблено прототип програмного комплексу підтримки процесу верифікації темпоральних обмежень цілісності у процесі управління змінами в онтологіях.

Прототип дозволяє виконувати набір функцій, пов'язаних зі спрощенням темпорального обмеження цілісності з використанням властивостей темпоральних логік, перевіркою виконуваності обмеження, верифікацією набору темпоральних обмежень цілісності на заданому архіві версій.

Таким чином, була досягнута мета дослідження, яка полягає в підвищенні ефективності процесу технічної підготовки виробництва за рахунок зменшення кількості помилок при модифікації моделей знань, поданих у вигляді онтологій, у інформаційних системах підтримки технічної підготовки виробництва, шляхом використання розроблених автоматизованих засобів верифікації обмежень цілісності.

СПИСОК ОПУБЛІКОВАНИХ ПРАЦЬ

1. Кеберле Н.Г. Моделирование динамических предметных областей в онтологиях / Н. Г. Кеберле // Збірник наукових праць Харківського університету Повітряних Сил ім. І. Кожедуба. -- 2009. -- № 3. -- С. 121--127.

2. Кеберле Н.Г. Применение логических средств для анализа изменений в онтологиях // Н. Г. Кеберле, В. А. Ермолаев, W.-E. Matzke // Системи управління, навігації та зв'язку. -- 2009. -- № 3. -- С. 105--110.

3. Keberle N.G. On the Decidability of Propositional Metric Temporal Calculus / Н. Г. Кеберле // Вісник Харківського національного університету ім. Каразіна. -- 2006. -- № 733. -- С. 149--159. -- (Серія: Математичне моделювання. Інформаційні технології. Автоматизовані системи управління ; вип. 6).

4. Keberle N.G. Hybrid Propositional Metric Temporal Calculus / Н. Г. Кеберле // Питання прикладної математики і математичного моделювання. -- 2007. -- С. 197--212.

5. Keberle N.G. Properties of Propositional Metric Temporal Calculus for Description of Evolving Conceptualization / Н. Г. Кеберле // Питання прикладної математики і математичного моделювання. -- 2006. -- С. 80--99.

6. Кеберле Н.Г. Огляд сучасних систем інтеграції неоднорідних баз даних і знань / Н. Г. Кеберле // Вісник Львівського національного університету ім. Франка. -- 2002. -- С. 163--172. -- (Серія: Прикладна математика та інформатика ; вип. 4).

7. Keberle N.G. Temporal Classes and OWL [Електронний ресурс] / N. G. Keberle // 6th Workshop on Web Ontology Language Experiences and Directions (OWLED'2009) in conjunction with International Semantic Web Conference (ISWC'2009), Washington DC, USA, Oct. 23-24, 2009. -- Режим доступу до матер. : http //www.webont.org/owled2009/owled2009_submission_
27.pdf.

8. Кеберле Н.Г. Сравнение элементов онтологии в архиве версий / Н. Г. Кеберле // Веб-программирование и Интернет-технологии (WebConf09) : междунар. науч.-практ. конф., 8-10 июня, 2009 г. : сб. матер. -- Минск, 2009. --Ч. 2. -- С. 14-15.

9. Keberle N.G. Ontology Evolution Analysis with OWL-MeT [Електронний ресурс] / N. G. Keberle, Y. I. Litvinenko, Y. A. Gordeyev, V. A. Ermolayev // Workshop on Ontology Dynamics (IWOD'2007) in conjunction with 4th European Semantic Web Conference (ESWC'2007), Innsbruck, Austria, 4-7 June, 2007. -- Режим доступу до матер. : http //kmi.open.ac.uk/events/iwod/papers/paper-05.pdf.

10. Кеберле Н.Г. Реалізація темпорального розширення мови OWL у машині виводу Pellet / Н. Г. Кеберле, Ю. І. Літвиненко, Ю. А. Гордеєв // Dynamical System Modeling and Stability Investigation : Int'l. Conf., May 22-25, 2007 : thesis of conf. reports. -- K., 2007. -- С. 374.

11. Keberle N.G. Metric Temporal Logics for Evolving Ontology Analysis / N. G. Keberle // Теоретичні та прикладні аспекти побудови програмних систем (TAAPSD'2006) : міжнар. конф., 5-8 груд., 2006 р. : тези допов. -- Київ, 2006. -- С. 199--202.

12. Keberle N.G. Hybrid Propositional Metric Temporal Calculus / N. G. Keberle // Математичне та програмне забезпечення інтелектуальних систем (MPZIS2006) : міжнар. наук.-практ. конф., 15-17 лист., 2006 р. : тези допов. -- Дніпропетровськ, 2006. -- С. 54--55.

13. Keberle N.G. Properties of Propositional Metric Temporal Calculus for Description of Evolving Conceptualization / N. G. Keberle // Математичне та програмне забезпечення інтелектуальних систем (MPZIS-2005) : міжнар. наук.-практ. конф., 16-18 лист., 2005 р. : тези допов. -- Дніпропетровськ, 2005. -- С. 65--66.

Размещено на Allbest.ru

...