2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 65
Текст из файла (страница 65)
Однако позншюнная система счисле. ния позволяет экономно представить огромные числа (такие представлениа растут логарифмическн прн россе чисел) н выполшпь над ними операции клава а очень эффективно. Поэтому преимущества позиционной сисгемы счисления очевидны, хотя, например, операция сложения для позиционной сисюмы счисления намного слояшее, чем для унарной системы счисления. Следует, однако, помнить, что использование В00 не всегда позволяет представить булеву функцию эффективно. Хоти известно, что ВРО являются компшггным представлением для большинства булевьш функций, встречающихся на практике, нет гарантий того, что для вновь расематриваемой булевой функции ее В00 будет линейка или полиномнааьна относительно числа ее аргументов.
Слшишкть В00 зависит от порядка переменных, и хотя длл большинства булевых функций представление в В00 линейно или полиномиально прн лкбых порядках переменных, для некоторых функций число вершин в представляющих их В00 может существенно различаться прн разных порядках переменных. Бс1лее того, найдены классы булевых функций, для которых представление в В00 зкспоненцнально для любых порядков переменных.
Одним нз основных применений В00 является представление конечных структур данных на основе непользования булевмх характеристических функций. Это привело к новому классу алгоритмов: так называемых "слмпыьлых" или "лааельи" алгоритмов, Одной из областей, в которой символьные алгоритмы исполиуются наиболее широко и успешно, является аатоматтпированное проектирование больших интегральных схем. Другая область — верификация дискретной аппаратуры н программ. Этой теме посвящена следующая глава.
Некоторые исследователи называют эффект применения симшшьных алгоритмов революцией в обработке дискретной информации. В наше время работа с булевыми функциями, представленными в форме В00, является фундаментальной техннкоК прнмешюмой ао многих областях вычислительной ла) ки. 9Л2. Замачания Бинарные решмощне диаграммы как структурм шшных дла представления булевых функций были ааедены рэнделом Брайвпгом (Капда) Е.Вгуалг) в работе [2э1. По некоторым источникам, публикация [25] явлщтая самой цитируемой в информатике, что показывает огромный интерес исследователей к этой теме и широкое применение этой структуры данных.
В работе [25) было показано, 'по при фиксированном порядке аргументов булевой функции В00 яшгяютги «е каномнческнм представлением. Брайант ссылвеюя на рабо- ту 1 отру цнй. гр 4 двух иост нейг рецл обсу Пою найт дока изсб [87), горн след нери Исп< прин мер, зуюь [192 отно сиоп В кл ЪЪТЬ, ваап вас~ дсяе! опис наль, "Иск боко георг ломб ния гмы мд. гся аю- лесла грн елках ~ых ых шх за гной ия ж" ~к ло ки ту 1.ее [98) как на первую работу, в шпорой преялвгвегся нспольюаать структуру бинарных решмоших дим рамы для предсгавления булевых функций. Работы Б. Асхмз [Ц н В.
Могег [114] также обсркдаот возможиосш графического представления булевых функций. Но именно ввелеиие в [25] двух дополнительных требований к бинарным диаграммам — редуцированпостн и упорядоченности — сделаю эту форму широко используемой. Линейный алгоритм редукции был предлшкен в [138]: Сравнение БАТ- решателей и подхода к решению проблемы выполнимости с помощью ВОО обсуждается в [18Ц и [28). Постановки задач в парадигме "Программирование в ограничениях" можно найти, например, в [167].
Проблема ЯЗВБЕТ-81)М исследуегся в [97], там же доквзыммтсв, что эта проблема ХР-полна. Использование ВОО для решения задач программирования в ограничениях обсуждается в [134). Компрессия нзобракений нв основе ВОР исследовалась многими авторами, например, [87), [126]. В работах [57), [147] представленм эффективные символьные алгоритмы обработки графов, основанные на ВРО. В рабате [42] проведено исследование эффективности представления в ВОР разреженных случайно сгенерированных графов.
Использование ВОО для анализа н синтюа логических схем уже стало общепринятыи. По этой теме написано несколько обзоров и монографий, например, [110), [118], [! 19). Существует несколько программных систем, использующих ВОО дпя автоматизированного синтеза т'1Л1.
Например, в университете Амхерста разработана система ВОЗ (ВРО-Ьашг) Еоб)с Яупгйез)з зуммп) [192). Разработаны программные системы эффективного маиипулированив отношениями на основе ВОР для решение разнообразных задач, например, система Сгосоры [173], В качестве вводного обзорного текста по ВОР н их применению макно указать, напрймер, [9]. Бинарные диаграммы с подавлением нулей ЕРР были введены в рассмотрение Яип-юй1 М)аио в [109). Их применение рассматривается во многих работах, в частности, для представления неполностью определенных булевых функций. Материалы работы [107], в которой подробно описываются области примененив 200, использованм в раздеяе 9,10.
Дональд Кнут а новом препригпе [88) одного из раздавов его очередного тома "Искусства программирования", высташмином в Интернете, представил глубокое исследование этой структурм данных. Им представлено множество теоретических результатов и применений квк ВОР, так и 200 а области комбинаторики. Гласе я 9.13. Задачи к главе 9 9Л. Для лшическихформул Я =хо-а и Я=я А,хну): а) построить двоичные решающие деревьв; б) по зтим деревьям построить ЖЮ дяя кюкаой фушщии; в) построить ВРР функций Я Е Я н Я ~ уг по ВРР дяя компонентных функций.
92. Постройте ВРР для компвратора — функции сравнения двух битовых слов: гт =(хг ну ) А(~ муг) А...л(т„му„) для я = 2 и 3 для двух разных порядков переменных х1<х2<хЗ<у1<у2<уЗ и х1 <у1<х2<у2<яЗ<у3. Заметьте, что при одном порядке переыенных рост слшкности ВРР пилсен, при другом — зкспоненциален. 9З. Мнннмнзируйте функцию у =(ррг)= рчреп)(рчг) примера9.1. 9.4. Постройте ВРР кз двоичного ршпмощего дерева для двух функций: Я =-а1чхЗ н гг х2лхЗ.
Постройте ВРРфункпии Я~ чЯ по полученным ВРР для кюкдой мз зтих функций. 9.5. Представьте в форме ВРР слелующее отобрахшнле Г конечного множеспа Х =(аЬсгг.е, р» в конечное мнпяпошо У= (а()уб» г /(а) = а, Г(Ь) = у, г(с) Рюу(г)) = бюг (е) ()У(б) = гх 9.4. Представьте в форме ВРР хврактеристнчешэе булавы функнии дяя ко- .4-(б,Х,б,,б, Р):8=(,,з„зг, д», Хч(аб», бс-( „зг», б=((зс,а,за),(ЪЬзг),(зг,а,зс),(з~ Ьзг),(зг.азз) (зг Ь з1)л(ззуазг),(зз,б,зе)» < (зз». ГЛФ Си( Успею сложи1 ными~ Ал гор~ юг с я~ назым шоде1 задами сгоянг еольнг ботакг булевг зариф~ слесфб наз ве ных п1 з вопию з коню снеге ю Алгор струю преобз рый я гумен лодзи лла С .як: ГЛАВА 10 ных Символьная верификация вмх ных уЗ.
Успешность применения техники тане! сйесй)лй для анализа больших н сложных систем в значнтелыюй степени обуславливается именно символьными алгоритмами верификации, которые рассматриваются в этой главе. Алгоритмы проверки модели дяя логики СТ(ч рассмотренные в гл. 3, работают с явным представлением состояний структуры Кринке, н поэтому их часто называют "яенымн" алгоритмами (ехрбсй маге воде! сйесЫнб — алгоритмы воде! сйесЫпй с явным представмнием состоаний). Для кюквай подформулы заданной темпоральной формулы эти алгоритмы вычисляют множество состояний структуры Кринке.
на которых эта подформула выполняется. Символьные алгоритмы верификации фактически делают то же самое, но онн работают с неявным представлением множеств состояний структуры Кринке булевыми функцнямн в форме бинарных решмощнх диаграмм. Символьную верификацию методом люде! сйесЫпб часто определяют как тосИ сйес!пнкьбннарные решотнгне диаграммы (шаде! снесЫпб+В00з), Символьная верифйкация является одним из самых элегантных и самых удивительных применений ВОР— этой формы представления двоичных функций, позволившей значительно повысить сложность анализируемых систем, что в конце концов привело к возможности применения верификации для анализа систем, разрабатываемых промышленностью. Алгоритмы шабе! с)мсЫнб выполняют преобразования множеств состояний структуры Кринке итеративно до тех пор, пока множество, к которому эти преобразования применяются, не перестанет изменяться.
Такой объект, который является результатом многократного применения преобразования к аргументу до тех пор, пока аргумент не перестанет изменяться, называется ненодвнэснай точкой нреобргмаеоння. По сути, все алгоритмы люде! сйесЫпй для СТЬ вычисляют неподвижнме точки, представляются ли они симапвыю ~лвев го или явно. Теория неподвижных точек преобразований дает теоретическое обоснование таких алгоритмоа. Именно теория иеподвюкных точек операторов на конечных множествах составляет основной материал этой главы. Другим вопросом, рассматриваемым здесь, является вопрос о том, как может быль построена дяя проверяемой сложной системы структура Кринке. содер.
яшщал астраномичеакае число состояний. Очевидно, что вручную строить также структуры Крипке невозможно. Необходимы методы построения двоичных функций, представляющих структуру Кринке, непосредственно из текста программ. 10.1. Необходимость символьных методов в верификации Классические алгоритмы верификации реагирующих систем, рассмотренные в гл. 3, являкпся аягаритмоми с явным представлением состояний структуры Кринке. На современных компькперах они могут использоваться для верификации систем, содержащих миллионы состояний, Представление каждого состояния требует обычно нескольких сотен байт, скорость обработки таких структур данных — порядка сотни состояний с секунду.
Казалось бы, этого вполне доспи очно для верификации систем. Однако реальные системы описываются моделями с огромным числом состояний. Хотя вычисления любой реальной системы в процессе своей жизни могут пройти лишь ничтожную полю возможных состояний, обычно заранее неизвестно, какие именно состояния и переходы необходимо проверять. Преимущаство верификации в том и еосюнт, что она позволяет иачерпывающе проверить все возможные трвекгории поведения систем. Рис.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
