2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 22
Текст из файла (страница 22)
затем в У дсбзншютса те состояния, помеченные р, у которых хоп бы один преемник уме принадлсхшт У. Этот шаг шюторяешя до тех пор, пшш в У пшвишютса новые со3' стояния. Графически зта проивлура показам парне.,Зуд 3 СО- глеев э ЯЧ Сь Э С Ко(р,с) / вгик«и« всзммкнат ыкевстко Осе«сянка не в«гоген енлОкняегся и (р(э() / эооа1 тв«в, Х, Тг ваези и: ( зез! реь(з) ) /* з Н вкк«емися состояния, ж«ычемвм р */ х:- ш х: ( ееа! чаь(в) ! /* в т вмнназтгся Оостомош, псегечмкем ч */ швеек чееьь Х тг Ьае(н х:-т( тФ х ы ш Iъ( е ! (Зе1: е-ы1) 31ат ! ) /* в т сосирезтся тапка состояния, «стогне ксеечекн р и из «ото)ем есть вере«оп в состояние, гзе иаколякиеся в т */ )аож Сложность алгоритма шоде! Ойес(ппй мала: О~~Ф~ е)М~ ) ! алгоритм липеен исто! ° ЫПО относительно слшкиости (числа подформул) формулы Ф и кеадратичеи атпосительио сложности структуры Крипке М (числа ее состояний и числа ее переходов).
Действительно, алгоритм иужио выполнять лля каждой подформулы Ф, а дяя формулы Арр нужно лля кзждого иэ состояний М проверять, помечены ли все преемники этого состояния формулой АРр. !. С К! К Н! з. и Об су( вых к Схож Крип! (зптл! с)рук Фуикиии Й)г Ей(р) . Множество состояний у, иа ксторьш выполняется формула ЕС р, работаег также в два этжш. Спачаэа в множество У собираются те состоянии, которые шнвечеиы р. На егором этапе иэ этого множества, У выбрасываюгсв все состояния, у которых иет ни одного преемника а У (т е. помеченных р).
Этот второй шаг првгоряется до тек пор, пока в у уыеиьшявша число состояний. О()Ф~ Сложность этою алгоритма можно уменьшить, выбрав другой базис СП.. Поскольку формулу АР молов вирши)ь через ЕС, то вместо бикса (ЕХ, АР, ЕП) моягио выбрать базис (ЕХ, ЕС, ИЦ. Напомним, что я сошэмт(ии э сгруктуры крипке м выполняется формула ес р, если в м существует бескоиечпый путь, пвчипжощийся в э, все состояния которого помечены р. рассмотрим алгоритм построения мишкеспэа состояний структуры Крипке, иа которых выполиявгся формула ЕП р.
Рлаеа Э кжы ШмСГЬ и атамг зат ка(р> зтззрзщззт иизвестзс ссстсззза, вз изтс(вм мжшозмтсз В(р '/ зтсвх тзт х, т( вз(пз х: шг т: ( зев( рех(з( ( /' з т — состсязия, вснтченние р */ ° т вава,х т( ьзга» х:-т( т: т ( ( з ( гкзыз-мц ззвт ( /' «» Х ми(рзсишвтсз тезиз ссстожвм, зз «свозы» (ттг верззсяз в ссозсзнвз, иэзиззз Гзз вринвявшат т */ шч( */ р / Можно построшь н другой алгоритм пометок для формулы ЕО р, слшкиость ° оторого пикейна относительно слшкиости структуры Крипке. Зтот алгоритм ° ыпспияетса в три этапа (рис. 3.9).
1. Стро(пся структура Кршше Мр, явжпошеяся о(раиичеиием структуры Крипке М иа множестве тех состояний, которые уже помечены атомарным предикатом р. (и ивен ен отела ее шфор- троее- 2. На множестве Мр строятся все ССК (сильно сшшиые компоиеи(ы). в со(/ суго по>ух(у- бираяв у в У О(~Ф~'()б(+ Я)). 3. Искомое множество состояний, иа которых выполняется формула ЕО р, образуют все состояния из этих ССК и те состояния из Мр, из которых сушествуст путь хотв бы в один сильно связный компонент.
Каждый из этих шагов имеет лилейную сложность. Нахшкдеиие сильно связных компоишпов производится с помошыо алгоритма Тарьяиа. Сяожиость авгоритма проверки СТЬ выполиеиия формулы Ф иа структуре Крипке М=(Я, Уе, й, ЛР, Е) для базиса (ЕХ, ЕС, ЕЩ лииейиа как отио. сительио сложности формулы Ф (числа ее подформул), так и сложности структуры Крипке (чигла шютояиий и числа переходов). Оиа равна Гласа З в рна З.р.
Трн этапа вылолнвннт алгоритма вычислснна состолний. уловлстаорниинл ЕС р Ъеюг 3 (М ОллСт( 3.7. Пример выполнения алгоритма тоде! сйес(дпя Нроверим, выполняется лн формула Ф=Е1(ЕХ р)ЮАУ10тг)) на структуре Кринке М, представленной на рнс. 3.10.
Рис.3.10, Пример структуры Крнпке лля мнюнза Для удобспю выделим все подформулы формулы Ф с помощью обычного вягорнпна синпюсического анализа 1! 00). Дерево синтаксическатг анализа этой формулы представнено нв рис. 3.1! . (! а((акр)нар(етг)] Рис. 3.11. Сюпвкснчкскнй анализ формулы логики СП. Будем последовательно выпалив(о алгоритм маркировки для структуры Кринке М (рис. 3.10) всеми подфорыулами формулы Ф, начиная с простейюик. Струатурв Кринке М с помеченными состояниями представлена на ° нс. 3.12.
рлвеа 3 а Ь=г Рис 3.12. результат работы аагорнтма модеь свссИая иа струвтуре Кринке М Последовательно строим: з 1=Р 'лиг! (з! зз зз зь ззг згг'з 1з01 гь Уз=ЕХгг с'нуз=М з4 гу уя =т ' изгуз =(зяб ззигз (зз~ ~> уь уа"згз йнуь =ггзезззз П Ут АРДь. Формулой Ут сначала помечаем те состояния, которые уже помечены Д~. Это состояния (зызД . Затем в цикле ищем те состояния, из которых все переходы ведут в состояния. уже помеченные З~. Это только состояние зы Таким образом, озгггт =(знзызз~ .
П Ф Уа =ЕЯПУ~). Формулой /~ сначала помечаем те состояния, которые уже помечены гг . Это состояния (зная,аз ~ . Затем в цикле лобваляем к ннм те состояния, помеченные Я~, из которых хотя бы один переход ведет в состоание, помеченное Уз. Это сосюЯние зз и зз. Таким обРазом, ~,з-~зг„з,зз,з4,з51. Поскольку начальное состояние зс не принадлнщзт множеству тех состоя- ннгь в которых выполняетсв Ф, то формула Ф не выполняется на струкгуре Кринке яг .
Ал Э. Дл Эт жв сц Пр [34 вр Дяпымпм пюсы ' бпя Сть гласа з 3.8. Заключение Темпоральнав логика ветвящегося временн (СТ1.) — это подкласс обобщен° ой темпоральной логнкн ветвящегося времеви СП.». В обеих этих логиках арнннмастся "ветвящаяся" модель времени: будущее не опрелслено одноммчно, в кшкдом состояннн вычнсленнй существуют ряшгнчные альтернатн° ы рязвнтня вычнслення в будущем, хотя только одна нз этих аяьтернатнв действительно реалнзустся. Такой взгляд на время широко используется для спецнфнквцнн свойств днскрстных дннамнческнх систем.
В СП. каждому темпоральному оператору ( Х, О, я, В ) должен непосредсг° евно предшествовать один нз кванторов луга (А нлн Е). Вследствие этого .мобяя формула СП. является формулой состояння, т. е, приниМает истинное пчн ложное значенне на кюкдом состоянии струатуры Крнпке, Такое ограннченне существенно упрощает алгоритм проверки выполннмостн спецнфнкапнй на структуре Крнпке. Наиболее удобным лля проверки выполнення формулы логики СТС на структуре Крнпке является так называемый алгоритм (мзмсткн сосгояннй: все состояния структуры Крнпке помечаются земн подфсрмуламн формулм СТ(., которые истинны в этнх состояннях.
Такую рзэ. мепсу можно вьшолшпь для рязлнчных базисов логики СП.. Аягорнтм любе( соесЫпй для формулы СТЕ лннеен как относительно слом° зстн этой формулы (чнсла ее подформул), так н относительно сложщктн структуры Крнпке (чнсла состояннй н переходов). Такая удивительная простота алгорнтмов проверки выпслннмостн формул СТЕ привела к "фонеме° альному" (140) успеху методов аернфнющнн, основанных на СТЫ ге уже только 3.9. Заиечания , кото. шляем юд веразом, Алгорппя тоде! сбеоЫвй для формул СП. был разработан в начале 80-х голов прошлого века неэавнснмо двумя группами: группой профессора Э.
Кларка (Е. М. Сйл щ) пз университета Карнегн-Меллона, США, н группой Лк. Снфакнса (Д 81ЙЫз) нз нсследовательского центра ЧЕК(МАО, Францня. Этот алгоритм оказался очень полезным для анализа тонких редко проявлаюшнхся ошибок в параллельных системах, поскольку сбслелуст все пространспю состояний снстемы, представленной моделью с конечным числом «сстояннй. »чзнведенные в ягой главе алгоритмы для обработки подформул СП. представляют собой моднфнкацню алгоритмов, предспшленных в монографнн Р4). Оценки слшкностн алгорнтмов проверки модели для СП. былн сделаны ° работе (31). 714 Р З Дщ 3.10. Задачи к главе 3 3.1.
Докюките, что следующие мнакества комбцвнцнй "квантор пупе, темпоразьный оператор" ле явлаотся базнсаыи Сви СЗ (ЕХ,АСз,ЕЩ П (АХ,АУ,АЩ 3.2. Выразите все комбинации "квыпор пути, темпоряяьный оператор" логики СП. а) через базис (ЕХ, А7), ЕЩ б) через базис (ЕХ, ЕС, ЕВ) 3,3.
Следующие формулы СП. предощвьте с помощью щюраторов базиса (ЕХ, ЕС, ЕП): а) М(р1)(ЕХ7)) б) АО(рчЕХл) з) АХ(ЕРрчА((ЕХО)Юр)) ЗМ. Для слелующих формул постройте сщггакснческис деревья, опредеяващие структуру нх подформул в соответствии с граммМикой формул СП.: а) А(р1)(гю(-рюАСО))) б) АО(рчЕХ7) 3.5. Постройте процедуры проверки моделя для., формул,АХР, Еро, А(47)г), а также грззрическое предспиление соачъстсщующнх процедур. анелопгчяое рис. 3.7. 3М.Пус М=(або,йдрь) — пщв отру ураКр щю: 3 =(зз зпзз зз) бе =(зг зз) ((зз зз).(зз.зс) (зеьб) (з~ зз) (зз зе) (зз зз)) МР=(оЬ),й(зе) (о), Цз|)=(об),Цзз)-"Ез.
а) В каких состояниях М выполняется формула СП. ЕХ АХЬ 7 б) В каких состояниях М выполняегтл формула СП. А((ЕХЬ) 0 а) 7 в) Выполняется ли формула ЕС А(Ь 1) а) на структуре Крепке М 7 а) 6) М З.Р. ) Крищ 3.19.! а) б) з) . г) 1 д) 1 е) 1 аюоег ' ел сгь емпо- аписа Заданная структура Крнпке нмает дяа начальных состояния. В такой структуре Кринке формула логики СП. выполняется, еслн она выподняегся в впкаом начальном состомюн атой стуукгурьь 3.7.
Пусть М = (о;Яе, Я,АР,ь) — такая стр)сггура Кринке: (яе з~ зз зз) бе (яе) ((зе з3) (а$ з|) (зз зе) (яегзз) (зз аз)»(аз ае)) Известно, что фоРмУла ЕРР аыполнлеЮЯ а состоЯнии зз. БУДет лн ЕРР аыполнятьсявгс7'В з17В зз7В М7 33). Пусть М = (о, Яс, й, ар, ь) — твим структура Крнпкв:, Я=(р, с, г,з);В> =(р,г); а = ((р, з)(с, г)(з, а), (е, я), (з, а), (г р), ( р г) ) АР = (а, Ь, с) Ь:Б — ьйлг;Ь(р) (а,Ь);Ь(а)=(с);Ь(г)=И;Ь(з)=(Ь), а) постройте графическое пркястаяяенне структуры Кринке; б) проверьте нстннность: М~ АУЕХ-а М!=ЕХАР(а» Ь) М~=АС(с»ЕРЬ) 39. Доказать, что формулы: (АСР)» р, р»А(цУр), р» Еур яаявстся тавтологнамн, т.е.
онн нстннны в вмгдом састояннн любой структуры Крнпке. 3.16. Какие нз следующих пар СП формул являются томдественнымн: а) АКАЕВ н АУАХВ б) ЕХЕЕр н ЕРЕХр в) АХАСо и АСАХВ г) ЕХЕСФ н ЕСЕХр д) ЕРЕСр и ЕСЕЖр е) ЕСн нрчЕХЕСр зтв ж) ЕСр н рлЕХЕСгр з) Ерр и цоЕХЕЕр и) ЕЕр и рлЕХЕЕ р 3.11. Дана формула Ст). ЕХА(оба) Постройте структуру Кринке, на которой зта формула истинна, н другую, на коюрой зта формула лакна, 3.11, Постройте структуру Кринке, на которой одна из формул, уявзанных в перечисленных ниже парах, вьюолняется, а друпи формула — нет: а) ЕЕВр н ЕСн б) Е)г(рлтг) и Е)грлЕйтр в) ЕС(ром) н ЕСнтЕСЕ г) АС(~рлйг) и АСНлАСтг 3.13.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
