Автоматика и телемеханика, № 3, 2014
© 2014 г. О.В. ГЕРМАН, канд. техн. наук, О.И. САДОВСКАЯ
(Белорусский государственный университет информатики и радиоэлектроники,
Минск)
ЛОГИЧЕСКИЙ СИНТЕЗ УПРАВЛЯЮЩЕГО АЛГОРИТМА В СИСТЕМЕ С БУЛЕВЫМИ ПЕРЕМЕННЫМИ
Рассматривается задача синтеза управления в системах, описываемых булевыми уравнениями с временным параметром. Предлагается алгоритм решения задачи на основе метода подстановок, связывающих значения переменных состояний в последующие моменты времени со значениями на текущем шаге. Преимущество предлагаемого метода в сравнении, например, с методом на основе булева дифференциала состоит в том, что нет необходимости искать все решения исходной системы дизъюнктов, а также в возможности получить подстановки заранее один раз и использовать их для различных исходных и целевых состояний системы.
1. Введение
Задача синтеза управления актуальна для ряда приложений, связанных с поведением интеллектуальных роботов, синтезом программ, управлением движением автоматических транспортных средств, например для построения маршрута движения при совершении маневров и т.п. Решение этой задачи может быть получено несколькими способами, в частности, с помощью техники, использующей двоичный дифференциал [1]. Однако эта техника требует, вообще говоря, строить граф достижимости состояний, размеры которого могут оказаться столь значительными, что данный подход окажется практически неприемлемым.
Решение можно искать на основе процедуры логического вывода в системе с изменяющейся моделью мира, как описано в [2]. Состояния описываются формулами логики предикатов, и механизм вывода не обеспечивает гарантированную финитность процесса в общем случае, так как не всякая истинная формула логики предикатов может быть выведена из непротиворечивой системы посылок [3, с. 159]. Это обстоятельство, в частности, не позволяет решить проблему автоматического синтеза программ в общем случае. Поэтому естествен интерес к получению метода синтеза управления при представлении систем формулами, допускающими только конечное множество состояний. Финитность процесса синтеза для таких систем достигается полным перебором состояний. Вопрос связывается с поиском методов, которые в значительной степени сокращают перебор и могут быть использованы на практике. В частности, в этой работе рассматриваются системы управления, описываемые булевыми уравнениями (продукциями) с дискретным временным параметром, играющим роль номера шага (такта). Такие продукции в общем виде
представляются следующим образом:
состояние_системы (Ь) & управление (Ь) — состояние_системы (Ь + 1),
где состояния_системы (управление) описываются булевыми формулами; временной параметр Ь определяет, что значения булевых переменных рассматриваются для данного шага Ь. Проблема синтеза управляющего алгоритма в рассматриваемой далее постановке связывается с отысканием конечной последовательности управлений, переводящих систему из заданного начального состояния в заданное конечное состояние. Поскольку состояния системы в таких описаниях представляются двоичными векторами конечной длины, то число всех возможных состояний конечно. В общем случае требуется, чтобы конечное состояние достигалось либо за минимальное число шагов, либо не превосходило заданного целого положительного числа, либо вообще было достигнуто в принципе, если это возможно.
Отметим подходы из [4, 5]. Подход из [5] взят за основу и развит в настоящей работе. Однако в [5] процесс синтеза управляющего алгоритма был ограничен жестким допущением о характере связей между состояниями системы, так как считалось, что из начального состояния в конечное мог вести один единственный путь или ни одного, что не имеет места в общем случае. Таким образом, излагаемые в статье постановка и решение задачи расширяют рамки [5].
Конкретизируем постановку задачи следующим образом. Состояние системы на шаге Ь свяжем с вектором < жх(Ь),..., хг(Ь) >, где хг(Ь) представляет г-й двоичный разряд вектора состояния системы, определяемый в момент Ь (Жг называется разрядной переменной). Для описания поведения системы вводим булевы уравнения с временным параметром следующего вида (используя общепринятые обозначения для булевых операций: & - для конъюнкции, — -для импликации, V - для дизъюнкции и " - для отрицания):
(1) &(ЖР(*),...,Ж,(Ь)) & Уз(Ь) — хк(Ь + 1),
где £г(-) - булева формула над разрядными переменными и уз- (Ь) соответствует управлению на шаге Ь. Управление уз- применяется на шаге Ь, если Уз (Ь) = 1, и не применяется, если уз- (Ь) = 0. Значения разрядных переменных и управления в (1) должны обеспечивать истинное значение формулы (1) и в общем случае заранее не известны.
Формула (1) интерпретируется таким образом: если в момент Ь состояние системы есть (т.е. формула истинна для значений разрядных переменных в момент Ь) и применяется управляющее воздействие (оператор) уз-, то переменная хк устанавливается в единичное значение на следующем такте Ь + 1. Заметим, что запись S¿ & Уз(Ь) — Жк(Ь + 1) определяет, что значение Жк на такте Ь + 1 есть "0".
Если уз используется только в состояниях Sjl, Sj2,..., Sjw, то включаем в описание поведения системы также продукцию:
Sjl & Sj2 & ... & Sjw —У уз.
Кроме того, требуются вспомогательные продукции, которые устанавливают, что необходимо выбрать как минимум одно управляющее воздействие на каждом шаге и изменить значение как минимум одной разрядной переменной.
Задается начальное состояние системы £0 =< ж^О^ж^О),... ,жп(0) > и целевое состояние =<ж1(к),ж2(к),...,жп(к) >, где к - фиксированная константа. Требуется построить (если это возможно) последовательность управляющих воздействий (операторов) С =< уп1, уп2,... >, Я ^ к, такую, что выполнение операторов в указанном в С порядке переведет систему из состояния £о в состояние Отметим, что описанный в этой работе подход позволяет отыскивать управляющую последовательность С = =< уп1, уп2, • • •, Упц >, Я ^ к, если таковая имеется в действительности.
Как и в [5], будем последовательно искать системы подстановок, выражающих значения разрядных переменных в моменты Ь +1, Ь + 2,..., £ + к — 1 от значений разрядных переменных в момент Ь. Обладая такой системой, например, для пары моментов < Ь, Ь + ^ >, можно проверить достижимость целевого состояния за ц тактов, решив простую вспомогательную задачу. Этим обеспечивается достижение цели работы.
Некоторые доказательства полученных в статье результатов содержатся в [5] и в указанных в 5] работах, так что они опущены.
Потребуется изложить модифицированный метод подстановок для решения задачи ВЫПОЛНИМОСТЬ (ВЫП). Этот метод является центральным для всей работы. Задача ВЫП хорошо известна [6] и формулируется так: дана система дизъюнктов с булевыми переменными ж1, ж2,..., жп (дизъюнкт представляет дизъюнкцию логических переменных, Ж1,Ж2,... , жп, взятых с отрицанием или без него). Требуется выяснить, совместна ли эта система (имеет ли она хотя бы одно допустимое решение). Система дизъюнктов совместна, если имеется набор значений для участвующих в ее записи переменных, на котором каждый дизъюнкт системы истинен (имеет логическое значение единица). Для иллюстрации сошлемся на следующий пример:
Можно получить подстановку для любой переменной этой системы или ее отрицания. Выразим, например, жэ. Для этого выпишем дизъюнкты, где содержится жэ:
2. Решение задачи ВЫПОЛНИМОСТЬ на основе модифицированного метода подстановок
(2)
= ж1 V ж2 V жэ, = ж1 V ж2,
= Ж1 V жэ, = ж2 V жэ V ж4,
= жэ V ж4, = ж1 V ж2 V ж4,
= жэ V ж4, = ж1 V жэ V ж4.
(3)
= жэ V ж4, = ж1 V жэ V ж4.
В [6] подстановка для жэ формировалась в виде:
(4)
жэ = ж4 & (ж1 V ж4).
Общее правило получения подстановки для Жг таково: выпишем из заданной системы дизъюнктов дизъюнкты, содержащие Жг:
Жг V Жг V ^2, . . . , Жг V Ггд,
где Ггг - дизъюнкция других литер из дизъюнкта ^г, содержащего Жг. Тогда подстановка
(5) Жг = Гг1 & Гг2 & ... & ГгД
сохраняет как минимум одно допустимое решение заданной системы дизъюнктов. Это утверждение, доказанное в [5], тем не менее допускает в общем случае потерю других допустимых решений. Поэтому в данной работе предлагается строить подстановку для Жг, видоизменив (5):
(6) Жг = Гг1 & Гг2 & ... & ГгД & £Ь
введя новую булеву переменную. Проследим дальнейший ход преобразований, который в общем случае требует применять следующие правила упрощения формул, получаемых при выполнении подстановок (см. [4, 5]), а именно:
А V (А V В V Г) & С = А V (В V Г) & с, А V (А V В V Г)& С = А V с.
Так, подставив вместо (4)
(7) Ж3 = х4 & (ж1 V Ж4) & е1, получим из (2):
(8) х1 V х2, Ж1V х2, Ж1V е1,Ж1 V х4, х2 V х4,Ж1 V Ж2 V х4, х1 V Ж4,Ж4 V е1. Выразим
(9) х4 = х1 & е1 & £2.
Снова использована дополнительная переменная £2. Получим
(10) Ж1 VЖ2, Ж1 VЖ2, Ж1 V£1, Ж1 V£2, Ж2 V£1, Ж2 V£2, Ж2 V£1, Ж2 V£2. Далее заменим Ж1 :
(11) Ж1 = Ж2 & £1 & £2 & £3 с новой переменной £3, что даст систему
(12) Ж2, Ж2 V £1, Ж2 V £2. Получим, наконец,
(13) Ж2 = £1 & £2 & £4.
Система (12) примет такой вид: {£1,£2,£4}. Выполнимость последней дает: £1 = 1, £2 = 1, £4 = 1, ж2 = 1. Из (11) можно найти для £э = 1 ж1 = 1 и £э = 0, ж1 = 1. Здесь уже содержится отличие от [5]. Из (7) и (9) получим два итоговых решения:
< ж1 = 1, ж2 = 1, жэ = 1, ж4 = 1 >, < ж1 = 0, ж2 = 1, жэ = 0, ж4 = 0 > .
Легко проверить по таблице истинности, что других решений нет. Метод [5] теряет решение < 0,1, 0, 0 >, в чем нетрудно убедиться, положив все дополнительные переменные равными "1".
Итак, суть модифицированного метода подстановок изложена. Имеет место следующее утверждение.
Утверждение. Подстановка (6) сохраняет все решения (если они есть) исходной системы и не добавляет новых решений.
Доказательство. Действительно, данная подстановка предполагает, что к заданной системе дизъюнктов присоединен дополнительный дизъюнкт
(14) ж, V £1,
причем переменная £1 входит только в этот дизъюнкт и ни в какой другой. В самом деле, получаем (6) из дизъюнктов:
ж, V ^1, ж, V ^2,..., ж, V ^д, ж, V £1.
Для наглядности представим исходную систему таким образом:
ж, V
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.