2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 21
Текст из файла (страница 21)
докшкем, что формулы языка Ез глубиной я нлн меньшей одновременно истинны или ложны В Ссстояниях зГ и г~ пун Ока' яЕ . Рассмотрим возможные типы формул языка Ел. Формулы тг= риля и=О,чрз. Поскольку р, П,и Фз — формуяы глубиной к' илн меньшей, по ннаукшвному предпсяакению истннностные значения этик формул в состспннях з и г совпадают. Поэтому н формулы е я О, ч Оз будут одновременно испшны нли ложны в эт~щ состояниях. обые ~ нли . До- Формула Ч~ ЕХф. По индуктивному преаполомешио, исгинностные значения любой формулы е глубиной я' или меньшей, в состояниях зги г~, так ме,кзки всостояннах з ~ н г ысовпвлают: вэтихсостоянияхоин илнодновременно истинны, или одновременно ломим. При истинности у = ЕХр в состоянии г., формула Е истинна нлн в ~~ „нли в зг ы или в г'(вследствие шшла г -+г ).
Если она истинна в г,, то, по инлуктивной гипотею, оиа истинна и в з,; если она истинна в г, то, по индуктивной гипотезе, она пстиниа н в з . В соответствии с рис.3.5, м истинна н в зГ, т.е. г ~ ЕХЕ ~ зг~=ЕХЕ. Доказательство того, что зг~=ЕХе =ь г,(=ЕХдг ана.- логично. Формула у = ЕРЕ. Все соспмнна, дсстюкимые из зг, достижимы такие н ш г, и наоборот.'Поэтому зГ~ Е3ариг.| ЕРЕ. Формула у Д(~р,е~рз) . Если зу ~= Д(ябрз), то формула Ез в сопим»кн э, выполняется (пэ зг есть вычисление, соспмщсе только нз сосгояний аз Е По индуктивной гипотезе, тогда Ез истинно и в г~.
Теперь возьмем любую формулу у' языка Тз Пусть И равно к. На структуре Кринке (рис„3.5) в соответствии с доказанным выше, если у В я, то з ! Г тогда и только тогда, когда гг! у. Однако очевидно, что СП формула Е(асс) выпапшсюя в г~ и не выполнясгся в з,. Следовательно, выразительная мощшють язьпш Ья строго меньше выращтельной мощности СТЬ: никакие формулы языка Ья не различают состояний г, и г, в шютро. анной нами структуре Крипке, а формула СЛ. нх различает. На основании этой теоремы мшкно утвершлать.
что рис.3.4 атраизет все зоэмомиые эависшиостн между комбинациями "квантор пути, темпоральная формула" логики СТЬ. Поэтому все бвзнсм СП. макло построить из зависимостей, пощзанных на рнс. 3.4. Иными гловамн, СП. имеет голыш шесть базисов, перечисленных выше. З.В. Алгоритм пто43е! сЬеоНпд для СТ1. Основшм идея этого алгорпгма — для кюкдой подформулы заданной формулы СП, опредшппь, в каких состояниях заданной струкгуры Кринке М зта подформула выполнается.
Этот алгорипя называется аыориммом ягауилуюе- глаа з (»ез) рею») )г ( еез) раь(з) )г ( зев) Р»Ь(е) нмг Ч»Ь(е) 1/, з с ах (р) ) в»с вг(р)г а»с ко(р,ч)с з»ст:- з»ь, з»ьг .. з»ст г- яаст . взтт г- и(рнч) Фун) ки) дяя кшкдой подформулы заданной формулы СП начнйвл с простейших подформул, этот алгоритм помечает все те соспмния струкгуры М, в которых эта подформула выполняеюя. Пусть задана прон)шшьная формула Ф логики СП. н струк)ура Кринке М.
Для кшклой подформулы чг формулм Ф ш)горнтм маркировки выполняет следукицне шаги; 1. Вычисляется множество шич состояний структурм Кринке М. в которых выполняешя Чг. 2. Вводится новый атомарный предаат рт. 3. Этим атомарнмм предикатом помечакпся все сосюяния М нз множества Ятг„. Поскольку обрвбоша кшкдой формулы Ч) закан»иваска введением нового атомарного предиката р„н маркировкой этим предикатом всех состояний, на которых выполняется Чг, то можно считать, что на каждом шаге алгоритма маркировки злементамн подформул впаянная только атомарные предикатм. По завершении алгоритма, если начальное состояние структуры Кринке М помечено атомарным предикатом Ре, то формула Ф выполняется на М.
Очевидно. чго достаточно рассмотреть алгоритмы разметки только для формул какого-нибудь (любого) базиса СП.: все другие формулы мо)уг быль выршкены через формулы бшиса. Выберем, например, базис (ЕХ, АР, ЕП) . Следующий алгоритм находит множество Лие таких состояний структуры КРншш М =(Б,уе,й,АР,()1, в кстоРмх истинна кшкдш полфоРмУла Чг фоР- мулы Ф, и помечает эти состояния атомарнмм предшспом Р„.
нш»зз сс ( я )е) ес ни' »зз ч'еасв(е) чзсь )ч~) з 4» / лл» ммх лолэзрсм ч' глзсьнса з / / все та»»е псшх(пегим Ч' вьи»»»итс» ели))ятл»ш с»изин»и»»ского»иамгза семени е / ° »ЗМШ (Ч'): (к ф' 'иь ъ)з лы ° (и йс: кс рах Ф)з КХ рис. ° тв ° мел лянвиагщ лкшм с/ сть /' зэс кх, зас ьг и эвс ко- эю Ьнкции, сввелеленвмэ ниве */ / ° васкам новик атоюармж срелккат рт н всэмчвен мэ есе состояния мюеестэа Звтт */ Гсе в11 эе Ээст П» Ыаы Ыэ1н(рт! ец еа (е М. шняст ового яний, орит- диказинке а в/.
фор- быть туры фор- Рис.З.б. Графическое прелсщвяение правюи размена ннопеспа соснмний сгрукгуры Крапке лщ фсрмулм ЕХ р Функция, возвращающая множество соответствующих состояний. приведена пмсеэс» эвс кхмер~ /* всэврвнает мкиистэо оютсявня, ва коням» мЕЗсщяется якр '/ мких чак т> Поясним работу алгоритма Алгоритм неявно выполняет синтаксический аналю формулы СП., который на каящом шаге выделяет очередную подформулу исходной формулы Ф, начиная с самых внугренних (здесь ~Ф~— число подформул формулы Ф).
После выделения очередной подформулы управяение передастся переключателю эщссв, который обрабатывает различные типы подформул Ф в зависимости от вида этой подформулы слелуюшнм образом. Еглн подформула ч/ — зто атомарный преднкат, илн отрицание атомарного предиката, нли дизьюнкщщ двух атомарных преднквтов, то построение мно. жества йнч состояний, на которых этн подформулы выполняются, совершенно очевидно. Если подформулой чг яаяявтся ЕХ, АУ нли ЕУ, то влгормпе обращается к соответствующим функциям, которые возвращают иножество состояний, на которых зтн полформулы выполняются.
рассмотрим зти функции по по. рядку. Функции йн ЕХ(р). Множество состояний, на которых выполняется ЕХ р, строится из тек состояний, хотя бы один из преемников которых ужв помечен р. Графически процедура наипкдения этого мнщкестаа показана на рис. З.б: если хотя бы один из преемников состояния э уже помечен р, то в этом состоянии выполнается формула ЕХ р. т: ( з( (Вз1: 3-ге1) пес(з1))г /* з т амнзмпяся сссзояння,нз нзпжем есть переход з огсео щ, пом ~~~ц~се р */ замни т ° па яппсаясн Ююсг)я / поз~ 2) Псеясипн () Пснеапь Ж Ю риа 3.7. ГреФичагдпе предсмммнве м(пднпма автозаза(м мжжистаа состояний, не ютсрнх пыжжнеетса АГ р Фунинии йи АР(р). Множество сос)ояний Т, на которых выполняетсв Арр, строится в два этапа.
Сначала в множество Т о)бнраются те состояния, которые уже помечены р. Затем в Т дсбавлмотся все состояния, у которых жж преемники уже прннадлмкат Т. Этот жвг повторяется многократно до тех пор, пока в Т можно дсбав(пь хотя бы одно новое состояние. Графически эта про(мдура показана на рис. 3.7. пннндса пас дг(р) /' поверенная нноаесеео соогоянзп, на зсесиж миомзмеся длр) */ 1ссз1 зан Х, тг Вес(а х: лг гс ( зеа( рес(з) .) /* з т пмамеаяся гз сссеоззня, мгздпм жяючмея р / яаяеаа песах Х тг /' пока а т пояапяаеся поена сосеожпж */ Велас хФ тг т: т ы ( з ( (тз1:з-езц з1ат ) /* ж д, атдо(м н,вс прем нгндзак тза нанодегся з т */ Фуике Форму собира Е(рЦ( тс сост дсжнг столин Функннн Йи ЕГ(/г). Мнодмство состояний Т, на которых выполняется йя р, таске работает в д(а этапа.
Сначви в мвоанж)во Т собирапэгея те со- Е)м Сть стояния, которме у)ке помечены р. Затем в У добавлянпся все состоянив; у которых есть хотя бы одни преемник из мнакествв У. Этот шаг повторяется ло тех пор, пока в У появляются новые состояния. Ипзстьсп ЛВС КУ)Р) / воввривввт пхохество состояпха, ЯВ «очсзви ммоххяется иур '/ Усова чах Х.
У! Веу)п У! ) ВВЗ) рВЫЯ) ) / в У вмпмвозоя сосзоявхя, сия!нивам р '/ ХВВВВС 3ЮСЗЗ Х У! . / ВО33В В У ООЯВ33ЯВЧСЯ ХОВЬИ СОсзсяис3 */ ьввзп Х! Х! У ы ) я ) )ЗЯЗЗВ-+в)! СЗВУ /* хв хахясм визе В У яс)ымсюзся зчю)В сооясяхпя я Вв хоихзш суивсзиувс переход мстя см в олво ссстоис/мя . уве хвхолиыеся в у*/ ° В3а! мвспхп у ° ВЗ ЯВОССЗОП нна, ястся у ко. крю- Гр- 1) !Ъмвзвзв Сс/ (Я~ Рнс. хэ. Графммское )пмдшавлевяе ВВ!Орнпяв нвхожкеюм мизвиствв сссзсянн)д нв ипорых выповнястся Е(рУ)д) 3 / 63уикпии О)н ЕУ/(р,3/). Миожеспю состояний У, на которых выполняетса формула Е(рз/р), также выполняезся в два яапа, Сначала в мне)рсствю У собирмотся те состоюиш, которые помечены р 3 в зтих состояниях формула е(р))д) выпслняешя, поскольку в ннх истинно 3) .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
