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

Введение

Актуальность темы

Цель диссертационной работы

Научная новизна.

Используемые формализмы.

Теория категорий.

Алгебры.

Коалгебры.

1 Бесконечные синхронные потоки

1.1 Моделирование бесконечных потоков

1.2 Имя потока, вариант поведения и множество поведений потока.

1.3 Бесконечные синхронные потоки.

1.4 Моделирование конечных последовательностей.

2 Метод синхронных потоков

2.1 Объект.

2.2 Композиция объектов.

2.3 Алгоритм синтеза математической модели системы из моделей составляющих ее объектов.

2.4 Формальная коалгебраическая семантика.

3 Темпоральная логика на потоках

3.1 Линейная темпоральная логика на потоках.

3.2 Проверка моделей и доказательство теорем.

4 Алгоритмы автоматического построения и анализа вариантов поведения объекта или системы объектов

4.1 Уточненная модель объекта с зависимыми и независимыми потоками.

4.2 Требования конечного недетерминизма в поведении объекта.

4.2.1 Требования уникальности поведения объекта

4.2.2 Требования конечного недетерминизма в поведении объекта.

4.3 Алгоритм построения фрагментов вариантов поведений объекта.

4.4 Линейная темпоральная логика на фрагментах.

4.5 Алгоритм анализа фрагментов вариантов поведения объекта путем проверки выполнимости ими временных свойств

5 Моделирование вариантов поведения системы производственных объектов

5.1 Модель простого производственного объекта.

5.2 Модель простого складского объекта.

5.3 Модель складского объекта с учетом динамики основных фондов.

5.4 Модель внешнего поставщика фондов.

5.5 Модель внешнего заказчика продукции.

5.6 Модель системы производственного объекта с учетом внешних поставщиков и заказчика.

5.7 Построение и анализ вариантов развития замкнутой системы.

Основные результаты диссертационной работы

Актуальность темы

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

Одним из перспективных направлений развития автоматизированных методов, является разработка методов моделирования с использованием дискретных потоков. Основы методов моделирования с использованием дискретных потоков заложены в 2001-2002 годах Ф.Арбабом, М.Бройем, Я.Руттеном, К.Столоном.

В методе Броя и Столена входы и выходы каждого компонента системы, называемого объектом, моделировались при помощи потоков. Внутренние состояния объектов не рассматривались. Синхронность потоков не использовалась. Семантика объектов задавалась при помощи функций, преобразующих потоки на входах в потоки на выходах.

В методе Руттена и Арбаба предложены два варианта семантики: ко-алгебраическая и на основе конечных автоматов. Как и в работах Броя и Столена, потоки использованы для моделирования входов и выходов объекта. В коалгебраической семантике внутренние состояния объектов не рассматривались. В семантике на основе конечных автоматов внутренние состояния определены внутренними состояниями соответствующего конечного автомата. Унификация способа моделирования входов, выходов и внутренних состояний не проведена. Синхронность потоков не использована.

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

Цель диссертационной работы

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

Научная новизна

В диссертации

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

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

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

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

4. В методе синхронных потоков разработаны

4.1. Алгоритм синтеза математической модели системы по заданной структуре и по моделям составляющих систему объектов.

4.2. Алгоритм построения фрагментов вариантов поведений объекта или системы объектов и алгоритм анализа выполнимости ими временных (темпоральных) свойств.

5. Методом синхронных потоков разработаны дискретные модели: простого производственного объекта, простого складского объекта, складского объекта с учетом динамики его основных фондов, внешнего поставщика фондов, внешнего заказчика готовой продукции.

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

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

Методы исследования

Методы исследования базируются на методах алгоритмизации, дискретного моделирования процессов, теории универсальных коалгебр, темпоральных логик, логике первого порядка.

Теоретическая и практическая значимость

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

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

Апробация работы

Результаты диссертации докладывались и обсуждались на следующих конференциях: Workshop on Specification and Verification of Component-Based Systems (Лиссабон, 2005), CONCUR (Лондон 2004), International Workshop on Coalgebraic Methods in Computer Science (Барселона 2004), ETAPS (Барселона 2004), Всероссийская научно-практическая конференция "Инновации в науке, технике, образовании и социальной сфере"(Казань 2003), Международная научная конференция "Компьютерное моделирование и информационные технологии в науке, инженерии и образовании"(Пенза 2003), на школах-семинарах International Marktoberdorf Summer School (Мюнхен, 2004 и 2005), на семинарах Института теоретической информатики Технического университета Дрездена (Дрезден, 2003-2005), кафедры Управления, маркетинга и предпринимательства Казанского государственного технического университета им. А.Н. Туполева (Казань, 2003-2005).

Используемые формализмы

В этой секции определены понятия, использованные при задании математической семантики метода синхронных потоков. Семантика метода синхронных потоков основана на понятиях финальных коалгебр бесконечных потоков элементов (из заранее определенного множества) и их подкоалгебр.

Далее приведен необходимый минимум определений. Теория универсальных коалгебр подробно рассмотрена в работах [80], [90] а также [62, 79, 75, 76, 77, 86, 56, 60, 61].

Теория универсальных коалгебр является сравнительно молодым направлением в теоретической информатике, поэтому многие определения теории коалгебр базируются на теории категорий или на принципе дуальности и на дуальных определениях из теории универсальных (абстрактных, высших) алгебр. Теория универсальных алгебр подробно рассмотрена в работах [31, 7, 46, 23, 8, 21, 9, 24, 28, 20, 53]. Теория категорий изложена в работах [96, 48, 5, 47, 64, 95, 73, 63, 83].

Теория категорий

Теория категорий — это раздел математики, изучающий свойства отношений между математическими объектами, независящие от внутренней структуры самих объектов.

Определение 0.0.1. Категория С состоит из класса объектов objc и класса arre стрелок или морфизмов таких что:

• для каждого морфизма / G arre определена его область определения и область значений. Пусть областью определения морфизма / является объект A £ objc, а областью значений — объект В G objc, тогда морфизм / определен как: : А^В

• для каждой пары морфизмов / : А —> В и д : В —> С определена их композиция:

9 о/ : А-+С

• для каждого объекта А задан тооюдественный морфизм 1(1 а'а'. АА

• выполняются нижеследующие законы ассоциативности и толс-дествеииости морфизмов.

Аксиома 0.0.2 (Закон тождественности). Тождественные морфизмы действуют тривиально. Пусть / : А —> В, тогда: о1йА = «/до/ = /

Аксиома 0.0.3 (Закон ассоциативности). Операция композиции ассоциативна. Пусть f : АВ, д : В С и Н : С И тогда:

Л ° (3 ° /) = (Л°р)о/

Стандартным способом описания утверждений теории категорий являются коммутативные диаграммы.

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

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

Рис. 1: Коммутативные диаграммы двух аксиом теории категорий: коммутативная диаграмма закона тождественности (слева) и коммутативная диаграмма закона ассоциативности (справа)

Определение 0.0.5. Морфизм / : А —> В называется изоморфизмом, если существует такой морфизм g : В —» А, что

70/ = idа и f од = idB

Определение 0.0.6. Два объекта А и В, между которыми существует изоморфизм, называются изоморфными А = В.

В частности, для любого объекта А тождественный морфизм id^ является изоморфизмом, поэтому любой объект изоморфен сам себе.

Определение 0.0.7. Для категории С определена дуальная ей категория Сор, в которой:

• объекты совпадают с объектами исходной категории:

A G obj с°р если и только если A G obj с

• морфизмы получены «обращением стрелок»: fop : В —► A G arr с°р если и только если f : Л —В G arr с

Для любого утверждения теории категорий можно сформулировать дуальное утверждение с помощью обращения стрелок. Дуальное явление обозначается тем же термином, но с приставкой "ко-".

Определение 0.0.8. Произведение объектов А я В это объект Ах В с двумя морфизмами р\ : А х В —> А и P2 : А х В —> В такой, что для Р1 , „ р2

А ■*-А х В-* В

А-^А + В^-В у С С

Рис. 2: Коммутативная диаграмма произведения объектов (слева) и коммутативная диаграмма суммы объектов (справа) любого объекта С с морфизмами /1 : С —> А и /2 : С -> В существует единственный (уникальный) морфизм {/ь/2) : С Ах В такой, что:

Определение 0.0.9. Сумма, копроизведепие объектов А я В это объект А + В с двумя морфизмами ц : А А + В и : В —> А +В такой, что для любого объекта С с морфизмами д1 : А —► С и д2 : В —> С существует единственный (уникальный) морфизм [(71, <72] : А + В —* С такой, что:

Определение произведения объектов 0.0.8 наглядно представлено в виде коммутативной диаграммы слева на рис. 2, а определение 0.0.9 суммы объектов — в виде коммутативной диаграммы справа на рис. 2.

Теорема 0.0.10. Если произведение и копроизведепие существуют, то они определяются однозначно с точностью до изоморфизма.

Определение 0.0.11. Универсальный или инициальный объект категории — это такой объект, из которого существует единственный морфизм в любой другой объект этой категории.

Теорема 0.0.12. Если универсальный объект в категории существует, то он определяется с точностью до изоморфизма.

Дуальным образом определяется финальный или коуниверсальный объект.

Р1 ° (/ъ /2) = /1 и Р2°(/ь/2) = /2 дъд2]°ч = д\ и [01,02] о г2 = 92

Определение 0.0.13. Финальный, терминальный или коуниверсаль-ный объект категории — это такой объект, в который из любого другого объекта категории существует единственный морфизм.

Теорема 0.0.14. Если финальный объект в категории существует, то он определяется с точностью до изоморфизма.

Введем понятие функтора, которое потребуется для описания коалгебр.

Определение 0.0.15. Функтор — это отображение одной категории в другую, сохраняющее структуру. Функтор F : С —» В ставит в соответствие каждому объекту категории С объект категории В и каждому морфизму / : А —> В категории С морфизм F(f) : F(A) —> F{B) категории В так, что:

• сохранены тождественные морфизмы:

F(idA) = idF{A)

• сохранены композиции морфизмов:

F(g°f) = Hd)oF(f)

Определение 0.0.16. Категория Set функций и множеств — это категория, объектами в которой являются множества, морфизмами — тотальные функции.

В категории Set универсальный объект — это пустое множество 0, терминальным объект — любое множество, состоящее из одного элемента. Терминальный объект обозначен через 1 = {*}.

Алгебры

Определение 0.0.17. Пусть F : Set —> Set функтор в категории Set функций и множеств. F-алгебра — это пара (М; а), состоящая из множества М и функции а : F(M) —> М. Множество М названо несущим мнооюеством алгебры. f{M1)-^IF(M2) ai Q2

Mx-f-^M2

Рис. 3: Коммутативная диаграмма F-гомоморфизма между двумя F-алгебрами

Определение 0.0.18. F-гомоморфизм между двумя F-алгебрами — это функция / : М\ —> М2, отображающая одну F-алгебру (Mi, ai) в другую ^-алгебру (М2, <22), такая что: о ax = а2 о F(f)

На рис. 3 представлена коммутативная диаграмма ^-гомоморфизма между двумя F-алгебрами.

Определение 0.0.19. Для функтора F : Set —> Set семейство F-алгебр вместе с F-гомоморфизмами между ними образуют категорию Alg(F) алгебр функтора F.

Определение 0.0.20. F-алгебра (/; т) является инициальной если из нее существует точно один гомоморфизм в любую F-алгебру.

Инициальные алгебры одного и того же функтора уникальны вплоть до изоморфизма.

Определение 0.0.21. Пусть задана F-алгебра (М;а). Непустое подмножество R С (М;а) называется F-подалгеброй (или F-субалгеброй), если пара (Я; а) сама является F-алгеброй.

Коалгебры

Определение 0.0.22. Пусть F : Set —> Set функтор в категории Set функций и множеств. F-коалгебра — это пара (М\а), состоящая из множества М и функции а : М —> F(M). Множество М называется несущим мноэ/сеством коалгебры.

Мх-f—*M2

Q 2 i F{1

Рис. 4: Коммутативная диаграмма F-гомоморфизма между двумя F-коалгсбрами

Определение 0.0.23. F-гомоморфизм между двумя F-коалгебрами — это функция / : Mi —> М2, отображающая одну F-коалгебру (Mi, ai) в другую Р-коалгебру (М2, «2), такая что:

2 о / = F(/) о ai

На рис. 4 представлена коммутативная диаграмма F-гомоморфизма между двумя F-коалгебрами.

Определение 0.0.24. Для функтора F : Set Set семейство F-коалгебр вместе с F-гомоморфизмами между ними образуют категорию Coalg(F) коалгебр функтора F.

В этой категории нас интересует прежде всего финальная коалгебра (в случае, если она существует).

Определение 0.0.25. F-коалгебра (Р; 7г) является финальной если из любой F-ко алгебры существует точно один гомоморфизм в (Р; 7г).

Финальные коалгебры одного и того же функтора уникальны вплоть до изоморфизма. Для многих функторов финальная коалгебра существует и известна, кроме того для многих функторов она строится каноническим путем [87].

Определение 0.0.26. Пусть задана F-коалгебра (М; а). Непустое подмножество R С (М; а) называется F-подкоалгеброй (или F-субкоалге-брой), если пара (R',a) сама является F-коалгеброй.

Основные результаты диссертационной работы

В диссертационной работе получены следующие основные результаты:

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

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

3. Для метода синхронных потоков разработана композиционная ко-алгебраическая семантика, т.е. семантика, в которой объединение объектов в систему трактуется как новый объект. Композициональ-ность семантики значительно упрощает работу с ней и облегчает создание алгоритма синтеза моделей и алгоритмов проверки выполнимости моделями временных (темпоральных) свойств.

4. В методе синхронных потоков разработан алгоритм синтеза математической модели системы. По заданной структуре и по моделям составляющих систему объектов строится модель системы.

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

Темпоральная логика использована для строгой математической записи временных свойств возможных поведений объектов и их систем.

6. В методе синхронных потоков разработаны алгоритмы построения фрагментов вариантов поведений объекта или системы объектов и анализа выполнимости ими временных свойств.

7. Методом синхронных потоков разработаны дискретные модели: простого производственного объекта, простого складского объекта, складского объекта с учетом динамики его основных фондов, внешнего поставщика фондов, внешнего заказчика готовой продукции.

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

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

1. Алгебраическая теория автоматов, языков и подгрупп. Под ред. Арбиба М., пер. с англ. Осетинский Н.И. и Бусленко Н.П. "Статистика", 1975.

2. Афанасьеф A.A., Куршев В.Н. Теория организаций. Учебное пособие. Казань: Изд-во Казан, гос. техн. ун-та, 2002. -184 с.

3. Бережная Е.В., Бережной В.И. Матеатические методы моделирования экономических систем. -М.: Финансы и статистика, 2002.

4. Борщев А, Карпов Ю., Колесов Ю. Спецификация и верификация систем логического управления реального времени // Системная информатика, вып. 2 ИСИ СО РАН, Новосибирск, 1993. -40 с.

5. Букур И., Деляну А. Введение в теорию категорий и функторов. -М.: Мир, 1972. 259 с.

6. Бусленко Н.П. Моделирование сложных систем. -М.: Наука, 1978.

7. Ван дер Варден Б. Алгебра. М.: Наука, 1976. — 648 с.

8. Винберг Э.Б. Курс алгебры. -М.: Факториал, 2001. 544 с.

9. Винберг Э.Б. Начала алгебры. -М.: МЦНМО, МК НМУ, УРСС, 1998. 192 с.

10. Воронов A.A., Титов В.К. и Новогранов Б.Н. Основы теории автоматического регулирования и управления. -М.: Высш.шк., 1977.-519 с.

11. Галиев Ш.И. Математическая логика и теория алгоритмов. Учебное пособие. Казань: Изд-во Казан, гос. тех. ун-та, 2004.- 334 с.12 1314