2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 57
Текст из файла (страница 57)
В00 н разлшвнпне Шеннона. Двоичные решающие деревьв и бинарные решмощне диаграммы графически предстаелшот рвзлолмпне Шеннона: У( г "° х )=хгУ1ч г Я которое для любого аргумента х функции у' монет быль записано в виде я' х гйеи я~, еуяе,Г ~,.о. Здесь, фактачески, используется булеза функция Фе от трех булевых ергу де~к,у,~=тултйгпуегявя Лдт-ид Рнс. 9 ласт ( ззгсщ ° юрия ренин функг терни фунщ 307 которая соответствует разлояншшо Шеннонм 1 "3и~л,а) нй ) «хаил1~ е)ша 1а оделяет гушх естся ВРР 1ОЧЕН нгые 00.0,0) 00.0,1) й!,1,1) рис. ОЛ.
двокчнае решаюшш верево шк прелспиленне разлопення Шеннона Бинарная решающая диаграмма является представлением заданной функции а базисе ( О, ), пе ) прн фмксированном порядке переменных. Рнс. 9.5 показывает, что любой узел двоичного решмощего дерева предспшляет собой начялыую вершину направленного ацнкяичсского графа, определающего значение некоторой частично определенной булевой функции. Для корня зтв функция исходим, для нашего примера это,г (р,р,г), лля внутренних вершин соответствующие им функции — зто частично определенные функции с конкретными (О или 1) значениями некоторых переменных, для терминальных вершин — зто константы б или).
являющиеся значениями функции на конкретных наборах значений аргументов. Гласе В 9.3. Свойства бинарных решающих диаграмм Редуцированные упорядоченные бинарные решающие днагршемы имеют мнщкество хороших свойств, которьм делают это представлание булевых функций очень удобным на практике.
ВРР— каноническое представление булепьщ функций. Главным ю свойств ВРР ааллется каноничность. ТЕОРЕВ[А 9.1 Редуцированная упорядоченная бина)швя решакшпщ дишрамма является каноническим представлением булевой функции при любом фиксированном порядке переменных. Таким образом, любая буяева функция имеет единственное представление е виде ВРР при выбранном поредяе переменных, 'по дает возможность эффективного выполнения дяя ВРР такой традиционно трудной операции, как проверка эквивалентности двух булевых функций. Проверка эквивалентносгн функций, представленных в ВРР с совпадающим порядком переменных. сводится к проверке июморфностн [совпадения с точностью до обозначения вершин) лвух графов. В общем случае алгоритм проверки нзоморфностн графов яеляегся Мр-полным, но проверка нзоморфности графов ВРР очень про.
ста именно из-за их специфики; ацикличностн, единственного корня, фнксн. рованиою порядка переменных н наеичия только двух направленных ребер. выходящих ю каждой промежугочной вершины. Сложность этого алгоритма пропорциональна числу вершин бинарной решмощей диаграммы, представюпощей функцию. Если порядок переменных в двух сравниваемых ВРР не совпадает, одну нз ннх следует перестроить. Слщкиоеть ВРР мазах Еще одним вюкным свойством ВРР является то, что сложность представления в форме ВРР многих булевых функций полнномнвльна или дюкс линейка Например, линейный рост показывает ВРР дяя многих аппаратных устройств; ВОР для 4-разрядного сумматора имеет 51 вершину, а для 64-разрвлного сумматора — всего 571 вершину.
Это означает, что ВРР используемых на првкппге функций от большого числа двоичных переменных (десатков и дшке сотен) можно представить очень эффективно в памяти компьютера. Сложность ВРР зависит ет нарядна переменных. Разный порядок переменных дает разные представления функции в ВРР. Для некоторых функций мх ВРР могут существенно отличаться по слщкности лля резных порядков переменных.
На рнс.9.6 пршштввлена ВРР функции Р = а,б, ч а Ь ч ...ч п„б„, кото) схож л,сг Для: пенн~ оптиз щесзз рядка Следг полег смотр л раз) Квжд ремен В [25 экспо предо чисел Одназ функс ельна. ных ы Прем феати еаютс правы часто делаю Явно /= спнсш комли испол~ лезот саых я казнен ~ие в , зфных. ения грапргь жснзбер. нтма 0 не оми' лля мест ззна- юнч- фск- зерскшгй яков эА- которая при порялке переменных а, < ц < аз < Ьз < аз < Ьз., имеет линейную сложность !у нее 2л вершин), а прц порядке переменных а, <аз <аз « .Ь, <Ьз <Ьз. сложность ее экспоненциальна (2ьи вершин).
Дяя заданной булевой функции можно попытаться найти порядок ее переменных, при котором ее ВОР минимальнц но проблема нахождения такого оптимального порядка переменных в общем случае является ХР-полной. Существуют эвристические алгоритмы для нахождения субоптимальиого порядка переменных в бинарных решмоших диаграммах. Следует отметить, что ллл некоторых классов функций нх ВОО имеют экспоненциальную слшкность при любом порядке переменных. Например, рассмотрим функции, представляющие схему умножения двух двоичных л-разрядных чисел: (гнлз...,г,„) =(аг!,~„...а„)к(ЬгА,"-,Ь„).
Каждый разряд произведения представляет собой будеву фующию от 2л церемениьос Р, = Рг(пц...,л„,Ь,,...,Ь„). В (25) доказано, что ВРО по крайней мере для одной ю функций г7' имеет экспоненциааьное число вершин при любом порядке переменных. В [!50) представлен анаяиз ВОО для схемы умножения двух 1б-разрядных двомчиых чисел. Эта ВОО имеет более 40 миллионов вершин. Однако для подавляющего большинства встречающихся на практике булевых функций сложность их представления в форме ВОР линейна нлн псннномиальна.
Наиболее экономно представляются ВОР булевых функций регулярных аппаратных струкгур и структур, в которых есть симметрия. Представзгеиие ВОО. В памяти компьютера ВРО предсшеляипся очень эффективно: их удобно прспстввип таблицей, в каждой строке которой указываются номер вершины, номер переменной и номера вершин, в которые направяены два выхода из этого узла, 0-ребро и 1-ребро. Зтн вершины, которые часто назыщючся 1о л и Ыф, являются корняии решающих подграфов, опре. являющих значения соответствующих частично определенных функций. Явно отмечается корневая вершина.
Для примера на рис.9.7 для функции т! т хзхзха построена ВРО и ее представление е виде таблицы и в виде списка. Сложность представления булевой функции в форме ВЕ О в памяти компьютера пропорционаяьна числу вершин диаграммы. При этом обычно попользуется хеширование. а 6 Ряс.
97. Прелстввпние ВОР твблнцей и ааккам Гяееа Р 9.4. Опврации над ВОО чгклг предс ° ЗЖД! Слово за чис Лля е бннар функо )'(р,д,г) +рГО(д(рог))) ч рд-эг т(р » д) й (дг). По такой формуле вычисление значения этой функции потребует очень большого времени. Использование В00 позволяет выполнить зту операцию очень просто. Фактически, бинарная решающая диаграмма булевой функции представляет собой нвпрввленнмй граф лла вычисления ее значения по значениям переменных. Алгоритм вычисления значения функции, представяенной в В00,— зто неокслько шагов (не более числа переменных) по этому графу.
Любой набор значений вргуменгов определяет путь нв графе, приводящий к терминальной вершине, О или 1. Например, В00 функции Г предссзвлена на рис. 9.2, н твм же покювно, квк вычисляеюя значение этой функции при значениях ее е1нуыентОВ х~ = О хз = 1,хз = О. Дпя вычисления значений булевой функции у; вместо того чтобы двиглться по графу, по В00 этой функции мвкно сгенерировать С-подобный кол, вы- и зак ггы Вернемся к операциям с булееымн функциями, которые перечислены в разделе 90; П найти значение функции на конкренюй интерпретации (нвборе значений аргументов); 12 найти все иншрпретвцни, ца котор19 12 ых функция равна 1; 12 проверить, явлаегся ли функция выполнимой, невыполнимой, общезиачимой; П проверить, совпвдвют ли две булевых функции; П выполнить булевы операции нвд булевыми функциями; 0 провести минимизацию функции в некотором базисе.
Все этн оперении могут быль выполнены очень эффективно, есяи булевы функции предстввлены в В00. Рвссмотрнм их по очереди. Вычисление значении булевой фуикцнп. Вычисление знвчеюм булевой функции от л переменных нв конкретном наборе значений аргументов по таблице истинности требует хранения твбпицы с 2" строками и манипуляциями с нею. Если функция представлена логической формулой, то такое вычисление может вылиться в сложную процедуру.
Например, длв функции у(р,д,г)=(р=эд)г (дг) эю потребует значительного времени. Зтв же функция может быль представлена и более евсиными формулами, например: лений )начи- улсвы (пуляое вы- нкцин ча же имер: 'очень ~и зна- гаться аь вы- НЗ )М4 . Фак- ммен70,— 1юбой арми:на на чнсляюший значение г" при любых значениях аргументов, )йпрнмер, но В00, представленной на рис.9.7. можно сгенерировать следующий текст, причим кюкдвв строка этого кода соответствует одной вершине В00: Ьоо1 Г ( Вео1 х1, х2, хз, х4 ) яосо ао4 О песенок к голоансн весенне я а: зя ( х1-О ! Зюз а( еза 9 Со Ш1 ю4: ал ( х2 1 ! еозо юсг е1ае еоео юзз юз: ЗЛ ( хз О ! ното ю01 е1ее нато ю2! Ю21 ьл ( Х4 О ! 9ОСО НОЗ ЕЗЕ ° еютю Ю11 в1: ° .есюкю (1) г во: кевок» (О) ! ! Слоююсть втой программы линейна: знв4юнне функции вычисляется вседа ш число шагов, не болынее числа перемешмш, от которых зюнюнт функция.
Для вычисления функций, у которых заданы значения не всех аргументов, бинарные решакнцие анаграммы такие удобны: на рис,9.9 лоцманы В00 функции / н получение нз нее В00 функции У'(р, Ф 1). канава Найти ° в би~ анну, ~пфрвв °авно Пестр асс куа °орив вв кот Вхирс вака~ иии д О-нуте лунки Ви.й.й, й ВОН Фуикиин в ВОО акой руиании ири заикина аначаний иазнквраск а~иуасансов Найти асс ивтерирегацвв, ва потерна функции равва 1. Любой пупь на бинарной реювопюй днагрвпю функции из корня а терминальную аершнну, помеченную!, определяет нмпянквпу — конъюнкцию литералов (переменных с отрицаниями пли без них), на которой значение атой функции равно 1. Посгроевве ДНФ в КНФ функции ве ВРР.
ВРР хранит боппую семанеческую информацию о предстялляемой ею булевой функции у . Пути от корня я листу 1 компактно предстааляют асс модели г (т.е. юпсрпрепппю, на которых У'=1). Все пути от кориа к лис!у О компактно предстааляют есе контрмодсли (те интерпретации, иа которых г" О). Далее, если путь от корня к листу 1 рассматриаать как конъюнкцию литералов н асс такие конъкизгь. ции дюъюнктнано объединить, то получим ДНФ функции,/.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
