ОПТИМИЗАЦИЯ  МЕТОДА  ЛОГИЧЕСКОГО  ВЫВОДА  ДЕЛЕНИЕМ  ДИЗЪЮНКТОВ  НА  ОСНОВЕ  ОПРЕДЕЛЯЮЩЕГО  ЭЛЕМЕНТА  ДЛЯ  ОБРАБОТКИ  ВЫРАЖЕНИЙ  ТЕМПОРАЛЬНОЙ  ЛОГИКИ  ЛИНЕЙНОГО  ВРЕМЕНИ

Чистяков  Геннадий  Андреевич

аспирант,  Вятский  государственный  университет,  РФ,  г.  Киров

E-mail: 

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]  предлагается  предикатная  таблица  для  требований,  выраженных  с  помощью  логики  линейного  времени  (LTL). 

В  ходе  построения  базы  знаний  не  используется  информация  о  конкретном  методе  вывода,  который  будет  применен  в  дальнейшем.  Целью  является  лишь  сведение  задачи  верификации  к  задаче  логического  вывода  в  наиболее  универсальной  форме.  МЛВДДОЭ  же  в  определенной  степени  обобщен,  и  позволяет  получить  решение  задачи  верификации,  не  принимая  во  внимание  то,  какая  именно  предикатная  таблица  была  использована  на  этапе  построения  базы  знаний.  Таким  образом,  способ  формирования  базы  знаний  и  метод  логического  вывода  являются  обособленными  и  независимыми  составляющими  предлагаемого  в  работе  [1]  подхода.  Схематичное  изображение  соотношения  между  ними  представлено  на  рисунке  1.

Особенности  выбранной  предикатной  таблицы  влияют  на  структуру  секвенций  базы  знаний.  Этот  факт  может  быть  использован  для  оптимизации  МЛВДДОЭ  за  счет  его  ориентации  на  обработку  спецификаций  в  виде  формул  только  одной,  заранее  определенной,  темпоральной  логики.

Анализ  предикатной  таблицы  для  LTL-логики  показывает,  что  все  посылки,  содержащиеся  в  базе  знаний,  будут  соответствовать  одной  из  представленных  ниже  структур.

Рисунок  1.  Соотношение  между  способом  формирования  базы  знаний  и  методом  логического  вывода

1) 

2) 

3) 

4) 

5) 

6) 

7) 

8) 

9) 

10)

11)

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

Оптимизация  шагов  МЛВДДОЭ.   Анализ  представленных  структур  позволяет  сделать  следующие  выводы  о  ходе  реализации  процедур  МЛВДДОЭ.

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

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

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

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

Применение  указанного  правила  позволяет  значительно  сократить  объем  обрабатываемых  данных.  Кроме  того,  это  правило  определяет  алгоритм  функционирования  блока  предобработки  [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.