2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 55
Текст из файла (страница 55)
пути, прохоллшего точно по одному разу через кмкдую вершину, мшкет быль сформулирована в виде проблемы проверки модели для некоторой формулы (,Т(.. Действгпельно, пусть О =()гй) — направленный граф с и вершннамн: Р = ~тпгз, ...,т„~. Поместим в кюкдую вершину г, атомарный предиквт р„истинный только а этой вершине. Построим (,П формулу, которая будет истинной в том н только в том случае, когда в 0 существует такой путь, что все атомарные преднкаты на нем истинны точно по одному разу (т.
е. р, когда-нибудь в будущем будет истинным, и в любом состоянии этого пути если утверждение р, стало истинным, то со следующего состояния оно все время будет лакным). Поскольку нам невюкно, с какой вершины начнется гамильтонов путь и в какой вершние ои закончится, введем дополннгельную вершину — источник, из когорой направлено по ребру в каждую вершину О. н дополнительную вершину — сток, в который направлены дополнительные ребра из каждой вершины О. Постройте такую формулу. гл~ Би ре) Бинар ионна ацикл листы сотен ны в функ( При ( решат тур д лрсдс ры да дирол осью( ленив става авели нов р гл. 10 ных ( аа2кд( ных, ВПП с ним "Бил( риО ( ГЛАВА 9 Бинарные решающие диаграммы Бинарные ргшаюшы дилграммы (В! лагу Рос!яоп Ргвйгштм, В00) — это экономная форма представления булевых функций в виде ориентированного ациклнческого графа.
Вершины графа представляют аргументы функции, листья — ее двоичные значения. Булавы функции а форме В00 от десятков, сотен и дюкс тысяч двоичных переменных могуг быть экономно предспшлены в памяти компьютера, и операции с такимн функциями выполняются очень эффективно. Поэтому многие задачи, в которых используются булевы функции, могут решаться весьма эффективно. При представлении булевых функций в форме В00 окязюккь аозмохгным решать многие проблемы, которые при традишюнных предстмшениях структур данных являнтшя неразрешимыми из-за большой размерности таких представлений и сложности операций над ними. Поскольку баювые струкгуры данных (в частности. конечные мншкества н отношения) могут быть закодированы булевыми функциями, а операции нвд ними можно определить с помощью булевых операций, то многие алгоритмы на конечных структурах данных становятся очень аффективными, если зти струхтурм данных предсгавить в форме В00.
Одно нз самых удивительных применений В00. позволившее увеличить сложность анализируемых систем в миллионы миллионов рвз — зто верификация методом шогйг1 сйгсягнй. Этой теме посвяшена нс 10. Однако ырнфикацня — не единственны область применения бинарных решающих диаграмм. В00 могут с успехом применяться фактически в каждой области, в которой требуется обработка дискретных структур данных, в частности, в комбинаторике. Можно без преувеличенна сказать, чго В00 совершили революцию в предспшленни ланных и алгоритмах работы с ними. "Быорлме решающие диаграммы (ВРР) — удамгшгльлы, и чгм больше я играю с инми, шгм бельгия я иг люблю. Окало 15 месяцев я быя кпк ребенок раева в Бюия]ю+ с новой игруитой, тыучие воэможность решать такиг нреблгмы, а которых л нвимда лю думая, что оии могут быть решены" — пишет Дональд Кнут о В00 в препршпе сваей новой книги 188].
В двиной главе ввоапся основные определения из этой области, а также кратко рассматриваются теоретические н пракпгческие аспекты, сввзаниые с В00: их свойспш, операции над ними и примеры их применения. Эта глава может чгпаться независимо от остального материала книги. 9.1. Проблемы с представлением булевых функций Фермы предсгввлеввн буяевьп фувкцвй. Булевы функции игрыот фундаментальную роль в информатике. Они широко применяются уже более полувека, на булевых функциях основана теория синтеза аппаратных систем вычислительной техники, их свойства исследовались несколько десятилетий.
Казалось бы, в этой области трудно придумать что-то радикавьно новое. Однако несколько лет назад была предложена новая эффективная форма представления таких функций — бинарные решмошие диаграммы, которая позволяет по-новому, очень зффеативно решать зааачи во всех областях применения булевых функций. Булевы функции могут быль представлены многими различными способами.
Стандартное представление для любого конечного отображения — это таблица соответствия, которая каждому набору значений аргументов сопоставлает значение функции на этом наборе. Для булевых функций такая таблица называется таблвисй ястиллостм мпкдому набору двоичных значений аргументов сопоставляеюя О или 1.
Другое широко используемое представление булевых функций — бинарное решмощее дерево (В! вту 0есЬюп Тюе). Приывр 9.1 Булева функция от трех двоичных аргументов г (хпхз,хэ) представлена на рнс. 9.1, а своей таблицей истинности, т. е. оютвстствием результата из множества ]0,1] кюкдому набору значений трех двоичных аргументов. На рис. 9.1, б представлено бинарное решающее дерево этой же функции. о ение 91 1бии юиюе дерево! Бинарное решакицее дерево булевой функции — это предстзлленне функции в виде ориентированного дерева с одной корневой вершиной.
Корень н другие внутренние вершины этого дерева помечены переменнымн функции, а листья (терминальные вершины) — значениями О или 1. гвен 9 юрьи Кнут ниже нные глава га на ение ~ной. мен- ми О гнда1олу г выетий, овос. орма "ориг гатях )ами. таб- ставлица й ври). б рве.р.1. Формы нрааеавмнна бумиой булавин: а) табьгиви нстннноеги н б) бинарное ремаюшае дерево Главе в 5. К б. П Для < (и п< рави< мой < рави< приап С лру Бинарное решающее дерево часто наэмвают семалшкческим деревом [170) На каждом ярусе такого дерева сюит одна н та же переменная. Из каждой внутренней вершины выходят два ребра — одно (штриховое) для значения переменной, равного О (его назовем О.ребро), другое, сплошное, дая значения этой переменной, рваного! (его назовем!-Ребро).
НапРавление Ребер— сверху вниз, стрелки на ребрах обычно не указываются, поскольку порядок вершин определяется высотой их расположения. Любой путь ат корня дерева к листу соответствует какому-либо набору значений двоичных переменных и завершается значением функции (О или 1) на этом наборе. Поэтому вычисление значения функции может быть выполнено спуском по семантическому дереву от корня к терминальной вершине.
На рис. 9д,б выделен путь ма бинарном решшошем дереве, который соствагствуьт следующему набору значений переменных: я< =О. ха =!,хз О. Этот путь ведет в термимальную вершину, помечемную 1. Действию<тьма, значение функции г примера 9.! на наборе (0,1, 0) рзпно !. Макно считать, что бинарное решающее дерево — зто графическое представление алгоритма вычисления значения булевой функцян по заданному набору ышчеммй аргументов. Существует много других форм задания булевых функций. В частности, функцию мояшо задшь аналитически, с помощью различных логических формул.
Приыпр 9.2 Функция У, предспзвленная рна.9.1, мажет быть задана кшшитнческн различными формулами, например: 1, Произвольные логическме формулы: ,г (х<,хз,хз) = -<г< ч хз Ф хзхз(х< ч хз) =(,Ф(Ь(;Фхз)))ч;Л зч(х<;)й-(хз д) 2.
Совершенная дизьюнктивнвя нормальнав фариа (СДНФ): .Г(х< хз'хз) Ч< тз тз ч т< тзхз ч азх< тз чхзх< тз д н р фор (СКНФ): у(х<,хз,хз)=(х,ч-азч-кз)(а<чхзчхз)(-<т<чхзч тз)(-а<ч кзч-пз) 4. Днзьюнвтившш нормаяьнв< форма (ДНФ): у(хг «з «з) т< хзч~ *зч ч тз х< хзчхз"пэ Очем< двух с<ишь савла верит скис < до н< имен< двух < Легко канон мвкш класс< (!то). ° идой ° ения ~ения !ер— задок среза инх н исле'хону гь на !бору ьную ж 9.1 дере.
5уле- «з) 5. Конъюшпмвная нормаяьная форма (КНФ)г .г(х! ~ хз)=("'тгчхз)(г~ч тз) ( тг уха)(я!ч гзч"«з)( «зч 'хз), 6. Полипом Жепакина: У(х!,хз,хз) =16 х, 9 хгхз 9 хзхз Е ГУ рабвпвнив й.й(неаыпопнимыа, выпил иные, общезначимые б павы фун ии) Булеаа функция называется невыполнимой, если на всех значениях аргументов онв равиаО. Булеза функция наэывавюя выполнимой, если оуществуют такие наборы значений аргументов, нв которых она ранив 1.
Булеза функция называется общезнвчимой, если на всех значениях аргументов она равна 1. Для невыполнимой булевой функции все ее значения в таблице истинности (и пометки на терминальных вершинах в ее двоичном решающем дереве) равны О. Для обшезначимой функции все зги значения равны 1. У выполнимой функции существуют наборы ее значений, на которых значения функцан равны 1, е ие 9.3 (ианоничасяов представление) Каноническим называется такое представление булевой функции, ко. торос явлются дяя функции единственным.
Очень чаою решение проблем информатики своднюв к проверке совпвлення двух обьекмв, и ташш проверка основана иа сравнении канонических представлений сбьеитов. Две функции равны (эквивахенгны), если их значения совпадают на всех наборах аргументов. равенство двух функций можно проверить по-их каноническому представлению: они рваны, если их канонические представления совлалмот (обычно с точностью до порядка членов нлн до изоморфизма). Каноническое представление булевой функции важно именно потому, что оно шпволяет проверить равенство (эквивалентность) двух функций. Легко видеть, что ДНФ, КНФ н произвольная формульнвя запись не являются каноническими представлениями булевой функции Любая булева функшкя мажет иметь множество рлшичных представлений в классах ДНФ, КНФ н в классе произжшьяых логических формул, Для функции г примера 9.1 выше прнведенм совершенно различные ее праволишения в классах таких формул.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
