Закирзянов Илья Тимурович Методы генерации детерминированных конечных автоматов с использованием сокращения пространства поиска при решении задачи выполнимости

Короткий опис

Закирзянов Илья Тимурович Методы генерации детерминированных конечных автоматов с использованием сокращения пространства поиска при решении задачи выполнимости
ОГЛАВЛЕНИЕ ДИССЕРТАЦИИ
кандидат наук Закирзянов Илья Тимурович
Реферат

Synopsis

Введение

Глава 1. Обзор предметной области

1.1 Задача выполнимости булевой формулы

1.1.1 Постановка задачи

1.1.2 Методы решения задачи выполнимости

1.2 Генерация детерминированных конечных автоматов

1.2.1 Базовые понятия

1.2.2 Изоморфные автоматы

1.2.3 Задача генерации детерминированных конечных автоматов по заданным примерам поведения

1.2.4 Расширенное префиксное дерево

1.3 Эвристические и метаэвристические методы генерации детерминированных конечных автоматов

1.4 Методы генерации детерминированных конечных автоматов, основанные на сведении к другим NP-трудным задачам

1.4.1 Метод, основанный на сведении к задаче раскраски графа

1.4.2 Методы, основанные на сведении к задаче выполнимости

1.5 Подход уточнения абстракции по контрпримерам

Выводы по главе

Глава 2. Сокращение пространства поиска при генерации детерминированных конечных автоматов с использованием

сведения к задаче выполнимости

2.1 Предикаты нарушения симметрии на основе кодирования алгоритма обхода в глубину

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

в ширину

2.2.1 Определение родительских переменных

2.2.2 Задание порядка детей с помощью родительских переменных

2.2.3 Определение переменных минимального символа

2.2.4 Задание порядка детей одного родителя

2.3 Подходы к сокращению пространства поиска, основанные на особенностях автомата дерева обхода в ширину

2.3.1 Полное дерево обхода в ширину

2.3.2 Зависимости между номерами родительских вершин и

детей

2.3.3 Минимальное расстояние в дереве обхода автомата в ширину

2.4 Реализация и экспериментальные исследования методов, использующих разработанные подходы к сокращению пространства поиска

Выводы по главе

Глава 3. Генерация детерминированных конечных автоматов по

избыточным примерам поведения

3.1 Масштабируемость предложенных методов в зависимости от размера расширенного префиксного дерева

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

3.3 Реализация и экспериментальные исследования разработанного метода

Выводы по главе

Глава 4. Генерация всех неизоморфных детерминированных конечных автоматов, удовлетворяющих заданным примерам поведения

4.1 Мотивация и постановка задачи

4.2 Метод генерации всех неизоморфных детерминированных конечных автоматов, соответствующих заданным примерам поведения, основанный на сведении к задаче выполнимости

4.3 Реализация и экспериментальные исследования разработанных методов

Выводы по главе

Заключение

Список литературы

Приложение A. Публикации

Реферат