Оптимизация метода логического вывода делением дизъюнктов на основе определяющего элемента для обработки выражений темпоральной логики линейного времени

Тип работы:
Реферат
Предмет:
ТЕХНИЧЕСКИЕ НАУКИ


Узнать стоимость

Детальная информация о работе

Выдержка из работы

ОПТИМИЗАЦИЯ МЕТОДА ЛОГИЧЕСКОГО ВЫВОДА ДЕЛЕНИЕМ ДИЗЪЮНКТОВ НА ОСНОВЕ ОПРЕДЕЛЯЮЩЕГО ЭЛЕМЕНТА ДЛЯ ОБРАБОТКИ ВЫРАЖЕНИЙ ТЕМПОРАЛЬНОЙ ЛОГИКИ ЛИНЕЙНОГО
ВРЕМЕНИ
Чистяков Геннадий Андреевич
аспирант, Вятский государственный университет, РФ, г. Киров
E-mail: gennadiychistyakov@gmaiL com
OPTIMIZATION OF INFERENCE METHOD BY DISJUNCTS DIVISION
BASED ON DETERMINING ELEMENT FOR LINEAR TIME LOGIC
EXPRESSION PROCESSING
Gennadiy Chistyakov
postgraduate, Vyatka State University, Russia Kirov
АННОТАЦИЯ
В работе предлагается несколько оптимизаций метода логического вывода делением дизъюнктов на основе определяющего элемента, являющегося одним из составляющих подхода к верификации алгоритмов на основе техники проверки моделей. Рассматриваемые оптимизации базируются на предположениях о структуре посылок в базе знаний, сделанных с учетом заранее предопределенного выбора способа описания требований к объекту исследования — формул темпоральной логики линейного времени. Оптимизации позволяют упростить некоторые шаги метода, что повышает его эффективность в конкретном случае.
ABSTRACT
The paper proposes several optimizations of inference method by disjuncts division based on determining element, which is a component of the approach to algorithms verification with model checking techniques. Considered optimizations rely on assumptions about the structure of premises in the knowledge base, made taking into account a predetermined selection method of describing the requirements for the object of research — the formulas of linear time temporal logic. Optimizations simplify some steps of the method that enhances its effectiveness in the particular case.
Ключевые слова: формальная верификация- логический вывод- деление дизъюнктов- темпоральная логика линейного времени.
Keywords: formal verification- logical inference- disjuncts division- linear temporal logic.
Введение. В работе [3] предлагается подход к формальной верификации параллельных алгоритмов на базе техники проверки моделей (model checking) и математического аппарата теории логического вывода. Ключевой особенностью подхода является использование на этапе сопоставления модели и требований к объекту исследования метода логического вывода делением дизъюнктов на основе определяющего элемента (МЛВДДОЭ).
Базовые сведения о проблеме верификации программ и алгоритмов представлены в обзорной статье [2]. Техника model checking наиболее подробно рассматривается в монографии [1]. Полное описание МЛВДДОЭ содержится в работе [3]. Полезными для понимания метода могут оказаться также работы [5, 6], в которых излагается обобщенный метод логического вывода делением дизъюнктов в логике предикатов первого порядка и логике высказываний.
МЛВДДОЭ хорошо зарекомендовал себя при проверке корректности алгоритмов, модели которых не могут быть эффективно представлены в символьном виде. К его наиболее важным особенностям следует отнести, во-первых, высокий уровень параллелизма, а, во-вторых, регулярность операций. В силу этих особенностей, временные затраты на решение задачи верификации могут быть значительно снижены путем аппаратной реализации ускорителя для выполнения МЛВДДОЭ.
При этом большое значение имеет специфика выбранного способа представления требований к объекту верификации. В некоторых случаях, учет этой специфики позволяет упросить отдельные шаги метода, что в конечном итоге приводит к получению более специализированного и, следовательно, производительного аппаратного решения.
Структура требований, выраженных в виде формул темпоральной логики линейного времени. Предложенный в работе [4] способ формирования базы знаний на основе структуры Крипке и формулы темпоральной логики содержит значимую вариативную часть — таблицу правил сопоставления подвыражениям формулы предикатов логики первого порядка (предикатную таблицу). В зависимости от конкретной модификации темпоральной логики, применяемой для спецификации требований к объекту верификации, используются различные таблицы. В работе [4] предлагается предикатная таблица для требований, выраженных с помощью логики линейного времени (ЬТЬ).
В ходе построения базы знаний не используется информация о конкретном методе вывода, который будет применен в дальнейшем. Целью является лишь сведение задачи верификации к задаче логического вывода в наиболее универсальной форме. МЛВДДОЭ же в определенной степени обобщен, и позволяет получить решение задачи верификации, не принимая во внимание то, какая именно предикатная таблица была использована на этапе построения базы знаний. Таким образом, способ формирования базы знаний и метод логического вывода являются обособленными и независимыми составляющими предлагаемого в работе [1] подхода. Схематичное изображение соотношения между ними представлено на рисунке 1.
Особенности выбранной предикатной таблицы влияют на структуру секвенций базы знаний. Этот факт может быть использован для оптимизации МЛВДДОЭ за счет его ориентации на обработку спецификаций в виде формул только одной, заранее определенной, темпоральной логики.
Анализ предикатной таблицы для ЬТЬ-логики показывает, что все посылки, содержащиеся в базе знаний, будут соответствовать одной из представленных ниже структур.
Способ формирования базы знаний
Преобразование модели объекта верификации
1_Т1_ СП
СИ* …
-К V
База знаний
А V
Метод логического вывода
Определяет соответствие модели и
требований путем определения выводимости целевого утверждения. Не обладает информацией о логике, в которой была записана спецификация. Примерами подходящих методов могут служить метод логического вывода делением дизъюнктов на основе определяющего элемента или модифицированный метод резолюций
Рисунок 1. Соотношение между способом формирования базы знаний и
методом логического вывода
1) 1 ® р© V 0ЕуеМ (с, ф)
2) 1 ® Р© V р (с)
3) 1 ® Р© V0Pj (с)
4) 1 ® Р'-© V0Pj © V0Pk (С)
5) 1 ®0Р© V 0ЕМ (С)
6) 1 ® 0Р© VРагеМ (с, у) V р (у)
7) 1 ®0Р© V Р (С)
8) 1 ® ^Р,© VРагеМС, у) V Р (у)
9) 1 ®0Р© V ^Епё© V р (с)
10) 1 ® 0Р© V 0Рагеп1(с, у) V Р (у) V Р](с)
11) 1 ®0Р© V Р © V Рк (С)
В приведенных структурах Р, PJ и Рк — соответствуют предикатным
константам, причем их индексы попарно различны, с и у — предметным переменным из области состояний модели, а ^ - предметной переменной из
области свойств модели. Для каждой структуры определяющий элемент является первым литералом.
Оптимизация шагов МЛВДДОЭ. Анализ представленных структур позволяет сделать следующие выводы о ходе реализации процедур МЛВДДОЭ.
При выполнении процедуры ограниченного образования остатков логический вывод не может быть завершен с положительным результатом. Данный факт связан с тем, что минимальное количество литералов в структурах посылок равно двум. Таким образом, при первом построении матрицы остатков не может быть получен нулевой остаток, так как необходимое для этого условие невыполнимо — литерал посылки не является единственным. Следовательно, анализирующие условие досрочного завершения шаги могут быть исключены из алгоритма процедуры.
При построении матрицы остатков не может быть получено более одного отличного от единицы остатка для каждого литерала выводимой цели. Данное утверждение обосновывается тем, что ни одна из посылок не содержит двух литералов с одной и той же предикатной константой (при этом контрарные предикатные константы следует считать различными). Следовательно, в ходе выполнения процедуры ограниченного образования остатков, в состав остатка-делителя имеет смысла включать только те литералы, в строках которых были получены единицы. Прочие литералы не смогут образовать какой-либо не единичный остаток при построении матриц последующих уровней.
Также можно заметить, что во всех структурах первая предметная переменная предикатов-фактов End, Event и Parent совпадает с предметной переменной определяющего элемента. Это означает, что литералы дизъюнктов, полученных после выполнения процедуры ограниченного образования остатков, будут содержать только найденные в ходе построения унифицирующих подстановок предметные переменные.
Данное наблюдение позволяет организовать эффективную выборку фактов из базы знаний для дополнения дизъюнктов-делителей, полученных после выполнения процедуры ограниченного образования остатков. Очевидно, что на
конкретном шаге вывода целесообразно оперировать только фактами, связанными с содержащимися в текущем целевом утверждении состояниями модели. Таким образом, может быть сформулировано следующее правило: «Остатки-делители, полученные в ходе выполнения процедуры ограниченного образования остатков, следует дополнять только инверсиями фактов о тех состояниях, которые содержатся в соответствующих данным делителям остатках-делимых».
Применение указанного правила позволяет значительно сократить объем обрабатываемых данных. Кроме того, это правило определяет алгоритм функционирования блока предобработки [3], задача которого и заключается в фильтрации неперспективных фактов.
Заключение. Перечисленные особенности получаемой базы знаний для требований в виде формулы темпоральной логики линейного времени приводят к упрощению используемого метода вывода. Это, в свою очередь, способствует получению более специализированного и, соответственно, более производительного аппаратного ускорителя для реализации логического вывода.
Список литературы:
1. Карпов Ю. Г. MODEL CHECKING. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. — 560 с.
2. Кулямин В. В. Методы верификации программного обеспечения // Всероссийский конкурсный отбор обзорно-аналитических статей по приоритетному направлению «Информационно-телекоммуникационные системы», 2008. — 117 с.
3. Мельцов В. Ю., Чистяков Г. А. Формальная верификация параллельных алгоритмов с помощью техники проверки моделей и методов логического вывода // Вят. гос. ун-т., Киров, 2013. 140 с. Деп. в ВИНИТИ РАН 10. 12. 2013, № 358-В2013.
4. Мельцов В. Ю., Чистяков Г. А. Формирование базы знаний на основе структуры Крипке и формул темпоральной логики // Фундаментальные исследования. — 2013. — № 8−4, — с. 847−852.
5. Страбыкин Д. А. Логический вывод в системах обработки знаний. СПб.: Издательство СПбГЭТУ, 1998. — 164 с.
6. Strabykin D.A. Logical method for predicting situation development based on abductive inference // Journal of Computer and Systems Sciences International. September 2013. Volume 52, Issue 5, — pp. 759−763.

ПоказатьСвернуть
Заполнить форму текущей работой