2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 73
Текст из файла (страница 73)
Каждое подмножество А ~ () миожества й называется "случайным событием" нлн просто "сабытием". С событиями А и В можно выполнять любые теоретико-множественные операции: объединение А ю В, пересечение А гэ В, дополнение (А, Каждому событию А ~ й стаанюя в соответствие его вероятностная мера Рг(А) — пслвкительное вещественное число. Тройяи (й, 2ц.
Рг) называегса сярсилтослтмт лростраиствомэ если: (2 Окрг(А)к( длятобого Ав2; С( Рг(И) = О н Рг(й) = 1 (нормировка вероятноспг); (2 Рг(вяз,А„) Еяэ1рг(Аз), если события А„попарно не перссекаююя (аддитиеность вероятности). Вероятностные структуры попользуются как конечные модели реагирующих систем, которые функционируют бесяонечно. Для анализа таких структур следует определить вероятностное пространство, позволяющее выполнить анализ множеств бесконечнмх вычислений в вероатнотиых структурах. Пусть задана вероятностная структура М с вероятностной матрнпей Р. Введем понятие Лиландра (или конуса).
о 11.3 лопая эсй Цилиндром конечной цепочки о зеэ1зз ...г„состояний вероятностной структуры М ( па РаЯ зря(М) ) назовем все такие возмакные бесконечные вычисления М, префикс которых совщщаст с р; С)д(а) = (я и РЫ1и(М)(а и ргвГ (я) ) ую юй ту- М На рис. 11.1, в выделен цилиндр папочки з„я з . СУ((эсэззз) = (Явзззззззз (зэзз) - эвззззз1 (Яоззззз1 ) Каждый цилиндр вероятнос1най структуры М играет роль случайного события сигма-алгебры, ассоциированной с М.
Два собьгпт этой сигма-алгебры независимы, если соответствующие цилиндры не перссттются. Мнткестао всех возмткных событий будет здесь представлено всеми тжможнымн ко. печными префиксами вычислений структуры М. Вероятностная матрщщ Р структуры М ляя кщкдого щщечного префиксе'и Ршйзуь(М) вычислений втой структуры, о=лез!зз ...з„, позволяет определить его вероятностную меру Рг(п) тек: Рг(п) 1, если префикс и состоит из единственного сосгояния зс, Рг(п) 4 Р(зс,з!)!з(з!,зз) ...Р(зе !,зз), если на!. Пр вр 74.2 Нз рис. 11.1, е показан нвчельнмй фрагмент развертки вычислений структуры М, из начального состояния зс. Верозтностнвя мера отрезка зегззз равна Р(зе,зз) х Р(зз,зз) = О 2х1.0 О 2 . Вероятностная мера отрезке зсз~зз: Рг(зол~за)=05х02 =О.! Итак, помеченную вероятностную структуру можно рзссмзтривать кзк расширение структуры Кринке, нв переходах которой заданы вероятности этих переходов.
Дяя сссгояний такой структуры можно спщнть следующий вопрос: "с какой вероятностью в данном состоянии выполнжтся некоторая формула пути темпорзльной логики" 7 Обозначим Уе(з,й) еераизщосмь того, что в состоянии з заданной вероятноспюй структуры выполняется формуле О темпорельной логики, Рассмотрим сначала только формулы вида ХР и РПО, где р и С вЂ” атомарные предиккгы. Для состояния зс, например, вероятность выщнщения формулы луги ХР равна О, поскольку нз зс нет переходов в состояние, в котором выполняется р. Вероятносп выполнения формуяы ХО в состоянии зс равна сумме веролпкктчй переходов в соспжння зз и з„т. е, 0.7 (см. рис.! 1.1, в).
Для того чтобы определить Уе(з,ХР) — вероятность того, что атомарный преднкзт р выполняется в состоянии; в которое есть переход из состояния з, нужно просто сложить вероятности переходов из сос~ання з во все такие состояния, в которых выполняется р. Из примера структуры М, (см, рис. 1!.1, а) видно, что Уз(зе,ХР) =О, Уе(зсХО) О 7, Уз(з!,Хр) =0 4. Пусть Ягг(з,р) — функция,равнзя 1, если р истинно в з, в противном случве Ли(з Р) = О. Тогда вероятность Уз(зс ХО) определится так: Уе(з,ХО) = ь чзр(з,з) хщи(з,р). й г(р Уз! Для щ ится а 0 0.4 0 0 0,2 Обрил Прмм Из рщ !2вт Позтщ взроет В сост верою сщъ с1 Уы Уз! ую гу ~на Более формально, пусть Оа!(р) есть вектор, зая(р): Я -е (О 1) саре!плиев!я так: Яат,(р) =1, если р истинно в з, в противном случае Зат,(р) О.
тогда вектор Уе(яс,Х!) равен произведению матрицм Р нв векюр столбец Бат(р): Уе(яс,Ху) Рябе!(р) Для примера вероятностной струк!урн яя! (рис. 11.1) вектор ®(Ху) строится так: 0 0,5 0 0.2 03 1 0.4 0 0.4 — 0.2 1 О ОЗ О ОУ О х О - < О.У; 0.4; !.О! О.а; !. 0 0 1.0 0 0 1 02 0 0 О 8 0 0 Обратимся теперь к формуле ОПр грассмотрюя ее вналзп на примере. зт- ео Р ю- ю, Пример 11.3 Ит рнс. 11.1, е видно, что молвю непосредственно подсчитать значение верня ятностей выполнения фврмулы ОПр в двук сяучисп !2 в тех состояниях, в которых вывюняезся р, аероятвкть Выпалив!изл формулы ОПр равна 1; С! в тех состояниях. в которых не вмполнмотся ни р „нн 1, аероятнодь выполнения формулм ОЮр равна О.
попому Ям(зз, О!!р) =1, Уе(ямтпр) =О. поскольку в соспмнии зз амповиястся Е, и с верояпнютмо 1 нз яз позмдмнз в состояние яз, в юпором ага веровтносзь равна 1, то Уе(зз, 4!!р) = 1. В состоянии яс вероятность выполнения формулы 01!р зависит от подобной вероятности в состоянии з,, н наоборот. Псзтому по рнс. 11.1, а молем написать свззываюпню ик уравнения: Уе(зс, АР) = 0,2 х Уа(зз, ОПР) + 0,5 х Уь(зз, ОПР) + 0.3 х УЬ(Я„, 41!Р) .
Уе(знее)=ОАхУе(лз,4Ър) +014х Уе(яз, ОЮр)+0 2хУе(ямдПр). Кол ревмя ээу снстему линейных уравнений, получим УЧ1яе, дВР) = 0,5, Ус~ап дВР) = 06. Более формально, определим дяя вероятностной струэпуры М трн непересекающихся подмножества состояний: ям, огм н ог, П очг — это мноямство такпк состояний, в которых нн формула р, нн формула 0 не выполняются, н таких состожвй, нз которых состояння, помеченные формулой Р, вообще не достижимы. В этих состояниях вероятность выпсяненгм формулы 0ВР равна О.
1э Ягм — зто множество таких состояннй, в которых вероятность выполнеем формулм ар равна 1. Это состояння, в юторых формула р выполняется. О л' — зто мнмкество твкнх состояний, в которых формула дВР может выполняться с некоторой вероятностью нэ интервала рг,!], Это те состояння, в которых выполняется только формула 0 н нз которых достижимо хотя бы одно состояние, в котором выполняется формула р.
Вмчнсленне вероятности вылолнення угаерясюння М,я) р для формулы пути ОВР состоит в вычнсленнн суммы вероятностей всех таких конечных путей вероятностной структуры М, которые начинаются а состоянии э, проходят через состоання, помеченные 0 н не помеченные Р, н эаканчнвакггся в каком-либо состоянии, помеченном р. Вычисление вероятностей выполнения этой формулы в состояниях верояпюсгной струкгурм связано с ременном снсгемы линейных уравнений. Система линейных уравнений даа пгщсчста вероятностей х, вмполнення формулы аВВ в состояннях я -азрщпсл после опредммння множеств 8 и бг х, О,сслн эаб х, =1,еслн янФм х, = Еэ чэргтэ,з ) х хач еслн э а Я Дяя решення снстемм лннейных уравненнй мсжмо использовать жобой численный метод. Пр~ Прс суш Ир (рнг оьт косг Рал очж нгрг псзг брог игрь выв Для ~ ворог струя Есоэе этапе 4,5,б веа 11 Нрныпр 44.4 Нроанвлнзнруем одну нз азартных нгр — игру в кости (Крепе).
В этой игре существует около 40 различных ставок. Найдем вероягность выигрыше лля самой простой нз ннх, ставки "Тйе Ргиэ Вег" — "Проходят". Игрок делает свою ставку "Т)м Розг Вег", помещая фишки на поле Рлзз б(не (рнс.! 1.2). Игра актонт нз двух этапов, нюываемых Персий бросок (Соте онг гор) н Исковое очко (Ролл).
На первом этапе бросаются две игральные кости н подсчитывается сумма очков, выпавших на обенх гранях. Ставка "Тйе Разя Вег" срезу выигрывает, если выпавшая сумма равна 7 нлн 11, н пронгрмввст, если в сумме выпадает 2, 3 нли 12. Если выпала любая другая сумма очков (4, 5, б, 8, 9 нлн 10), то она запоминается как Пгэгодлое очко — Роыг (на игровом столе набранное значение отмечается фишкой в соответствующей позиции поля Ро!лГ), н игра переходит ко второму этапу. На втором этапе бросанне двух костей продолжмтся многократно. Ставка "Х)м Рази Вег" вынгрываст, если значенне Рот! выпадет раньше, чем выпадет 7. Как только выпадает сумма очков 7, ставка "Тйе Розг ВгР проигрывает.
э, нн мння, алне- юлня- иаулы вчных ян г, ~чива- юстей юзано некая Рнс. ! 1 2. Игровое поле лля нгры в косги Для определенна еероятностн выигрыша по ставке "Тйе Раи ВеР шютронм веролпкктную структуру модели игры (рнс. 11.3). Иэ состояния жаи этой структуры мшкно непосредственно попасть в состояние кол (выигрыш) нли йхие (проигрыш), что соответствует выигрышу нлн проигрышу на первом этапе. Из состояния магг глюке можно попасть в промежуточные состояння 4,5,0,8,9,10 (онн нумеруются суммой очков, не прнаодящнх к выигрышу нлн глава ы Количе 4 < 6 7 12 Задачь ятнас1 состоь делит! Здесь, проигрышу не первом этапе). В этих промежуточных состояниях существуют перевалы в состояние мол (если в одном нз повторных бросков вышшст то же очко), в состояние (ооге (если в одном нз повторных бросков выпвдет 7) и возврат в зто же состояние при всех других нсходях.
Рне. 11.Э. Вероятяаспмя сгрукгуре ляя анализе игры в пити Переходы струхтурм помечены веровтноегями саопатствуюших событий. Верозтвкти определаатся числом благоприятных исходов нз множества всех возможных исходов нв каждом шаге игры в квждом нз состояний. Например, выпадение 2 прн бросании двух костей возможно только при одном исходе — выпадении 1 у первой кости и 1 у второй.
Сумма 3 может выпасть при двух походах (1:2 н 2:1), число 5 выпадает при 4 исходах (1:4; 2:3; 3:2; 4:1) нт.д. Благопривтные исходы пэ возможных 36 исходов: 2 сь1:1 число блегопршпных 1 3 са(:212:1 2 Персы патою вазмв ход из чта вь возим вяютг.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
