УДК:
658.012.011.56:658.512
Шарипбаев А.А., Куандыков А.А.
ФОРМАЛИЗАЦИЯ ПРОЦЕССОВ ОБРАБОТКИ СИТУАЦИЙ
ОБЪЕКТА УПРАВЛЕНИЯ ДЛЯ ЦЕЛИ ПРИНЯТИЯ УПРАВЛЯЮЩИХ РЕШЕНИЙ
Введение
В
последние время все большее применение находят методы теории формальных систем (ФС)
для решения практических инженерно-прикладных задач.
Авторами
этой работы были применены аппарат теории ФС в решении задач верификации,
корректности работы вычислительных систем [1] и задач управления сложными
объектами, одним из представителей данного класса объектов являются
компьютерные системы различного типа [2]. В данной работе авторы применяют
аппарат теории ФС для формализации процессов обработки ситуации, возникаемых на
объекте управления для цели принятия решений в ходе управления им.
Аксиомы формальной системы процессов
управления объектом
Основные
аксиомы по обработке ситуаций, возникаемых на объекте управления, в частности,
на распределенной компьютерной системе следующие.
Определение 1. Объектом
управления является структура, состоящая из совокупности узлов (Y) и отношений (R¢) между
ними O = (Y, R¢).
Определение 2. На
объекте происходит технологическая операция ТП = (Тпi, R²), где Тпi - единичная технологическая операция, которая
выполняется в узле Yi; R² - отношения между технологическими операциями {Тпi}.
Аксиома 3. Состояние
узла Yi характеризуется значением параметров (или координат) Xi = (xij, j=1,n).
Аксиома 4. Воздействие
Dk на Yi
изменяет его состояния, которые проявляются в изменении значений {xij, j=1,n}.
Аксиома 5. Воздействие
Dk на неавтономный узел Yi не является локальным и приведет к изменению
состояния {Yj : j=1,q, j≠i, q≥1}.
Аксиома 6.
Воздействие Dk на автономный узел Yi является локальным и не приведет к изменению
состояния других {Yj}.
Постулат 1. Обобщение
значений контролируемых параметров состояния объекта. Постулат об обобщении значений параметров состояния ОУ.
Для объекта с
непрерывным параметром.
Пусть для непрерывного
параметра Pi выполняется
условие:
(DPi1, Pi1¢) ® (U1 = dk) и (DPi2, Pi2¢) ® (U2 = dk),
где: DPi1 и DPi2 – интервалы значения параметра Pi; Pi1¢ = dPi(t)/dt, Pi(t) Î DPi1 и Pi2¢ = dPi2(t)/dt Pi(t) Î DPi2 -
тенденция динамики (т.е. знак направления изменения значений - первая
производная) изменения значения Pi в заданных интервалах; U1, U2 - принимаемые решения в соответствующих
интервалах значения Pi, dk – присваиваемое
содержание (или значение) принимаемое решениями U1, U2 по управлению, которые нормализуют
значения Pi в
заданных интервалах. Пусть Pi3¢ = dPi(t)/dt, Pi(t) Î (Pi1, Pi2)
значения Pi с внутренней стороны двух интервалов DPi1 и DPi2.
Тогда, при
si1¢ºsi2¢ºsi3¢ºsi° и U1 º U2 можно обобщить (значения интервалов параметра) значений параметра
Pi: Pi1 Å Pi2 и оно будет равняться DPi1 + DPi2 + D(Pi2 - Pi1), т.е.
Piоб = Pi1 Å Pi2 = DPi1 È DPi2 È D(Pi2 - Pi1),
где по обозначению si1¢ = {1, если Pi1¢ >
0; 0, если Pi1¢ £ 0}, si2¢ = {1, если Pi2¢ >
0; 0, если Pi2¢ £ 0}, si3¢ = {1, если Pi3¢ > 0;
0, если Pi3¢ £ 0}; Pi1
= DPi1,
Pi2= DPi2;
Å - знак операции обобщения.
Отсюда, выражение:
(Piоб, si°) является обобщением [(DPi1, si°) (DPi2, si°)] с точки зрения принимаемого решения U = dk, (обобщением [(DPi1, si°) (DPi2, si°)] является (Piоб, si°).
Для объекта с
дискретным параметром.
Пусть для
дискретного параметра Pi выполняется условие:
DPi1 ® (U1 = dk) и DPi2 ® (U2 = dk),
где: DPi1 и DPi2 – интервалы значения параметра Pi; U1, U2 - принимаемые решения в соответствующих
интервалах значения Pi, dk – присваиваемое содержание (или значение) принимаемое решениями U1, U2 по управлению, которые нормализуют
значения Pi в
заданных интервалах. Пусть (Pi1, Pi2)
значения Pi с внутренней стороны двух интервалов DPi1 и DPi2.
Тогда, при
U1 º U2 можно обобщить значения
параметра Pi: Pi1 Å Pi2 и оно будет равняться DPi1 + DPi2 + D(Pi2 - Pi1), т.е.
Piоб = Pi1 Å Pi2 = DPi1 È DPi2 È D(Pi2 - Pi1),
где по обозначению Pi1 = DPi1, Pi2= DPi2.
Отсюда,
выражение: (Piоб)
является обобщением [DPi1, DPi2] с точки зрения принимаемого решения U = dk, (обобщением [DPi1, DPi2] является (Piоб).
Следствие 1 постулата 1. В частности интервалы значений Pi могут стягиваться в точку DPi1 ® Pi1 и DPi2 ® Pi2.
Следствие 2 постулата 1. В частности интервалы значений Pi могут быть близкими друг к другу: Pi2 - Pi1 ® 0.
Свойства 1.
Для обобщения различных интервалов значений параметра Pi: DPi1, DPi2, DPi3 выполняется свойство коммутативности: (DPi1ÅDPi2) ¹ (DPi2ÅDPi1) и ассоциативности: (DPi1ÅDPi2ÅDPi3) = (DPi1ÅDPi2)ÅDPi3) = (DPi1Å(DPi2ÅDPi3)).
Постулат 2.
Постулат, который является более сложной аксиомой
имеет два варианта ее формулировки.
Вариант
1. Для
описания S,
соответствующего описанию состояния объекта по значениям P = {Pi1}, i = 1, n с характеристиками c(S) = (c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14) в
требованиях [1-4] выполняются условия аддитивности. Иначе
говоря, семантика S равнозначна
объединению семантики описания каждого Pi по отдельности, т.е. S = ÈDPi [Pi1], которое является предложением Хорна [1-4].
Однако,
такое представление описания состояния объекта является не всегда
технологичным, поэтому рассматривается также вариант 2.
Вариант
2. Семантическая сила
(т.е. однозначность интерпретации, полнота и точность описания состояния ОУ)
всех вариантов описаний состояний объекта S по значениям P = {Pi1}, i = 1, n с характеристиками c(S) = (c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14) в [1-4]
равна семантической силе описания (представления
описаний) состояния объекта в виде S= ÈDPi [Pi1].
Свойства 1. Вариант представления состояний в виде S = ÈDPi[Pi1] является рабочим для процедурной обработки, но не технологичным
с точки зрения принятия решении по ним.
Теоремы и правила выводов формальной
системы
процессов управления объектом
На основе приведенных аксиом докажем истинность следующих
утверждений и теорем
Утверждение
1. Формула/теорема G называется логическим следствием
формул/аксиом F1,F2,...,Fk, если для любой
интерпретации j из того, что j(F1)=j(F2)=...=j(Fk)=1
следует, что j(G)=1.
Утверждение
2. Множество формул/аксиом {F1,F2,...,Fk}
называется выполнимым, если существует интерпретация j такая, что j(F1)=j(F2)=...=j(Fk)=1.
Перед тем, чтобы приступить к доказательству теорем
предварительно приведем лемму, которая определяет условия доказуемости теоремы
в рамках исходных утверждений.
Лемма 1. Формула/теорема
G является логическим следствием формул/аксиом F1,F2,...,Fk
тогда и только тогда, когда множество формул/(аксиом и теоремы) L={F1,F2,...,Fk,
¬G} невыполнимо.
Доказательство. Пусть формула G является следствием множества формул F1,...,Fk.
Предположим, от противного, что множество L выполнимо. Это означает, что
существует интерпретация j такая, что j(F1)=...=j(Fk)=j(¬G)=1.
Но если j(F1)=...=j(Fk)=1, то j(G)=1, поскольку G —
логическое следствие формул F1,...,Fk. Полученное
противоречие j(¬G)=1 и j(G)=1 доказывает, что множество формул {F1,...,Fk,
¬G} невыполнимо.
Пусть теперь множество формул L невыполнимо.
Рассмотрим интерпретацию j такую, что (F1)=...=j(Fk)=1.
Поскольку L невыполнимо, то j(¬G)=0. Если j(¬G)=0, то j(G)=1. Следовательно, из
равенств (F1)=...=j(Fk)=1 следует равенство j(G)=1. Это
означает, что G — логическое следствие множества формул F1,...,Fk.
Доказательство теорем сводится к доказательству того,
что некоторая формула G (гипотеза теоремы), является логическим следствием множества
формул F1,...,Fk (допущений). Т.е. сам текст теоремы
может быть сформулирован следующим образом "если F1,...,Fk
истинны, то истинна и G". Такой метод доказательства теорем называется методом
резолюций.
Как было показано ранее, задача о логическом следствии
может быть сведена к задаче о выполнимости. Формула G есть логическое следствие
формул F1,F2,...,Fk тогда и только тогда,
когда множество формул {F1,F2,...,Fk,¬G}
невыполнимо. Метод резолюций как раз и занимается тем, что устанавливает
невыполнимость такого множества формул.
Теорема 1.
Теорема об обобщении - «обобщение пар ситуаций».
Если даны
ситуации S1 и S2, описания которых совершенны и структура которых такова: S1 = {DPi1[Pi1], i =
1, n} и S2 = {DPi2[Pi2], i = 1, n}, соответственно, то их обобщение S1 Å S2 имеют вид
S12об = {DPi[(Pi1
Å Pi2)],
i = 1,n},
где DPi – информационная часть переменного Pi; [Pi1] – значение Pi в составе описания ситуации.
Доказательство теоремы 1. Необходимое и
достаточное условие прямого
доказательства. Описания ситуаций S1 и S2
состоят из значений измеряемых параметров P = {Pi1}, i = 1, n.
Поэтому,
согласно аксиоме 4 их описания можно представить виде предложения Хорна S1 = {DPi1[Pi1], i =
1, n} и S2 = {DPi2[Pi2], i = 1, n}.
Согласно аксиоме 5
результат обобщения описания в формате Хорна также представляется в виде Хорна S12об = {DPi[(Pi1 Å Pi2)], i =
1, n}, что и требовалось
доказать.
Доказательство от противного. Пусть S12об = {DPi[(Pi1 Å Pi2)], i =
1, n} не является
результатом обобщения S1 и S2.
Это может
быть только тогда, когда описания S1 и S2 не являются совершенными и не сводятся к предложению Хорна. А это
противоречит условиям теоремы, что и является не допустимым.
Утверждение 3. Обобщенная ситуация S12об имеет
те же свойства, что и исходные S1 и S2, если у них свойства совпадают, иначе для
свойства обобщенной ситуации S12об выполняется операция объединения исходных свойств.
Следствие 2. Если исходные ситуации S1 и S2 совершенные, то обобщенная ситуация S12об также
является совершенной.
Приведенные
аксиомы, теоремы и их следствия позволяют построить процедуры и алгоритмы,
обеспечивающие корректное описание текущих ситуаций на микро-уровне и обобщение
ситуации и формировать класс ситуаций и решения на макро-уровне, а также
правильно определить управляющие решения для текущих ситуаций. Эти процедуры и
алгоритмы, входя в состав метода ситуационно-группового управления СО, тем
самым составляют его основу.
Теорема 2.
Теорема инвариантности структуры обобщенной ситуации S12об структуре ситуаций S1 и S2.
Обобщенная
ситуация также является совершенной и инвариантной по структуре к исходным
ситуациям.
При
обобщении описания ситуации S1 и S2 преобразуется в предложение Хорна: S1 = {DPi1[Pi1], i =
1, n} и S2 = {DPi2[Pi2], i =
1, n}, а полученный
результат также в формате предложения Хорна будет представлен: S12об = {DPi[(Pi1
Å Pi2)],
i = 1, n}.
При этом
операция обобщения состояния состоит из объединения по координатного
(параметрического) обобщения значения переменных DPi[(Pi1 Å Pi2)]
без переноса величины результата обобщения по одному компоненту на другой
компонент при его обобщении. Отсюда, вытекает, что количество элементов не
изменится, изменится только их диапазон значений.
Тем самым
теорема доказана.
Теорема 3.
Вторая теорема обобщения «обобщение произвольного количества ситуаций».
Если даны
ситуаций SJ = {S1,
S2, S3, …, Si, …, Sn}, описания которых
совершенны (т.е. сводимо к предложению Хорна) и имеют следующую структуру Sj = {DPij[Pij], i = 1,n; j = 1,m}, соответственно, то их обобщения ÅSi имеют вид: SJоб = {DPi[(ÅPij)], i = 1,n; j = 1,m}, где DPi – информационная часть переменного Pi, [Pi1] – значение Pi в составе описания ситуации.
Доказательство теоремы 2. Доказательство проведем методом индукции.
1. Случай 1.
Пусть SJ = {S1, S2} состоит из пары ситуаций. Тогда доказательство теоремы
2 сводится к доказательству теоремы 1.
2. Случай 2.
Пусть SJ = {S1, S2, S3}
состоит из трех ситуаций. Тогда теорему докажем для пары {S1,
S2} также
как, для теоремы которая доказана путем сведения к доказательству теоремы 1, в
результате которой будет получена первая ступень обобщения S12об.
В связи с тем, что
ситуации {S1, S2} совершенные, то их обобщение S12об согласно следствия
2 также будет совершенной ситуацией и инвариантной по структуре.
Далее требуется
доказательство теоремы для пары {S12об, S3}. Обобщение этой пары будет имеет вид: S123об = {DPi[(Pi1
Å Pi2)],
i = 1,n}.
Согласно теореме 2
структуры описания обоих ситуаций S12об и S3, совершенны и тождественны по структуре. Поэтому
результат обобщения будет S123об и доказательство сводится к теореме 1.
Тем самым доказательство
справедливости результатов обобщении доказано для случая 3-ех ситуаций, т.е.
для описания 3-ех состоянии объекта.
3. Случай 3.
Пусть SJ = {S1, S2, S3,
…, Si, Si+1} состоит из i+1
ситуаций. Пусть теорема доказана для i количества ситуаций и результатом обобщения будет: S1-iоб = {DPi[(Pi1 Å Pi2)], i =
1,n}.
Тогда теорему докажем
для пары {S1-iоб, Si+1}. Доказательство будет сводится к
доказательству теоремы 1, в результате которой будет получена первая ступень
обобщения S1-i+1об или S2-iоб.
Тем самым доказательство
справедливости результатов обобщении доказано для случая i+1 описаний состояний объекта.
Отсюда вытекает полное
доказательство теоремы 3.
Заключение. Приведены аксиомы, теоремы и правила выводов прикладной
формальной системы, которая формализует процессы управления в проблемной
области управления сложным объектом.
Литература
1.
Шарипбаев А.А. Доказательство
правильности программных и аппаратных средств компьютеров. – Алматы: НИЦ
«Гылым», 1996. с. 240.
2.
Куандыков А.А.
Аксиоматическое основы формальной системы управления сложными объектами. Вестник
КазНТУ, № 6/1(70) 2008. – С. 90-94.