Теоретико-категорное исследование семантики областей Скотта параллельных моделей с реальным временем

• Автор: Дубцов, Роман Сергеевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2008
• Место защиты: Новосибирск
• Количество страниц: 116 с. : ил.

Содержание
Введение.

1 Известные результаты

1.1 Элементы теории категорий

1.2 Области Скотта.

1.3 Структуры событий .

1.4 Системы переходов с независимостью .

1.5 Сетипроцессы и сети Петри

2 Семантика помеченных областей временных структур событий

2.1 Категория помеченных областей Скотта

2.2 Категории временных структур событий .

2.3 Взаимосвязи категорий временных структур событий и помеченных областей .
2.4 Выводы
3 Семантика помеченных областей временных систем переходов с независимостью.
3.1 Категории временных систем переходов с независимостью
3.2 Развертка временных систем переходов с независимостью
3.3 Взаимосвязи категорий временных систем переходов с независимостью и помеченпых областей
3.4 Выводы
4 Семантика помеченных областей временных сетевых моделей
4.1 Категории временных сетейпроцессов
4.2 Свойства категорий временных сетейпроцессов .
4.3 Взаимосвязи категорий временных сетейпроцессов и помеченных областей .
4.4 Категория временных сетей Петри.
4.5 Взаимосвязи категорий временных сетей Петри и помеченных областей .
4.6 Вывода.
Заключение.
Список использованных источников


Цель диссертации состоит в развитии и обобщении теоретнко-ка-тегорных методов спецификации и верификации параллельных систем реального времени. Методы исследований. В рамках данной работы использовались методы ті понятия теории категорий, теории множеств, теории графов, теории автоматов и теории частичных порядков. В качестве формальных моделей параллелизма применялись первичные, расслоенные и стабильные структуры событий, сети Петри н системы переходов с независимостью и их временные расширения. Научная новизна. В результате выполненных исследований автором разработаны оригинальные методы решения задач построения семантики «истинного параллелизма» и установления взаимосвязей моделей параллельных систем реального времени. Разработаны временные расширения моделей с семантикой «истинного параллелизма» — временные нервич-ные/расслоенные/стабильные структуры событий, а также временные системы переходов с независимостью. Построена семантика помоченных областей Скотта для временных структур событий, временных систем переходов с независимостью и временных сетей Петри. Определены и изучены категории введенных временных моделей, между которыми установлены строгие взаимосвязи в терминах существования коррефлекснй. Практическая ценность. Полученные результаты носят в основном теоретически характер. Тем не менее, они могут быть применены при разработке модулей автоматического построения семантических представлений, эквивалентных преобразований и верификации параллельных процессов, а также оптимизации параллельных программных систем. Личный вклад автора. Все результаты, представленные в диссертации, получены автором лично. Постановки задач выполнены научным руководителем И. Б. Вирбицкайте. Апробация работы. International Workshop «Concurrency, Specification and Programming» (Gross Vaeter See, Germany, ). Кроме того, доклады no теме работы были сделаны на ряде семинаров Института систем информатики СО РАН (г. Новосибирск) и кафедр Новосибирского государственного университета. Публикации. По теме диссертации опубликовано 9 научных работ, в том числе 1 — в изданиях, рекоммондуемых ВАК, 1 — в научном журнале, 6 — в трудах международных и отечественных конференций и семинаров. Структура и объем работы. Диссертация состоит из введепия. Во введении обосновывается актуальность рассматриваемых вопросов; формулируются цели исследований, представленных в диссертации; описываются научная новизна и практическая ценность работы; приводится краткое описание содержания диссертации ио главам. Первая глава содержит базовые понятия, определения и результаты, используемые в последующих главах. В разделе 1. В paedejie 1. Скотта. В раздыс 1. В разделе 1. В разделе 1. Петри и сетями-процессами. Вторая глава посвящена теорегико-категорному исследованию различных классов временных структур событий и построению для них семантических областей Скотта. В разделе 2. В частности, вводится понятие нормы элемента области и устанавливается связь между нормой и первичными элементами области. В разделе 2. В частности, устанавливается, что временные конфигурации всех трех моделей образуют’ области Скотт. В разделе 2. Доказывается экпивапентности категорий первичных структур событий и помеченных областей. Дат ее, устанавливливается существование корефлекспй между категориями временных расслоенных и стабильных структур событий и категорией временных первичных структур событий. Третьи глава иосвещена исследвашпо временных расширений систем переходов с независимостью в рамках теорегн-категорного подхода и построению семантики помеченных областей данной модели. В разделе 3. Также строятся соответствующие категории. В разделе 3. В заделе 3. Построенная цепь корефлекспй связывает категории временных временных систем переходов с независимостью и помеченных областей. Глава 4 посвещена изучению временных расширений сетей Петри. В разделе 4 { вводится определение понятия временной сети-процесса, строится соответствующая категория. В разделе 4-2 изучаются свойства построенной рапсе категории. В частности, формулируются необходимые и достаточные условия, ири которых морфизм является эпи- или мономорфизмом.