2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 74
Текст из файла (страница 74)
Количесмеемыд влмюз сисемм вуют 7) и гий. Ианом асть 3:2; 4 е»1гЗ;2:2; 3:1 3 5 с»1:4; 2:3; 3:2; 1:4 4 б с»1:5; 2:4; 3:3; 4:2; 5:1 5 7 с»1:6; 2:5; 3:4; 4:3; 5:2; б;1 б 8 со2:6; 3:5; 4:4; 5:3; 6:2 5 9 с»3:6; 4:5; 5:4; 6:3 18 с»4:б; 5:5; 6:4 ' ' ' ' ' 3 11 с»5:б; б:5 .2 12 ссб:б 1 Переход из состояния ггагг в состояние иол 'помечен вероятностью 8/36, потому что на первом зпше выигрыш дмот выпавшие суммы 7 или 11, по вазможно при 8 благоприятных исходах из общего числа исходов 36. Пере- ход нз состояния млм в состояние /созе помечен вероятностью 4/Зб, потому что вмпаденне ив первом зтапе сумм 2, 3 или 17„приводящее х проигрышу, возможно прн 4 благопрюпиых исходах нз Зб.
Подобным образом подсчиты- ваются вероятности всех переходов структуры. Задачей пешего анализа ввлвстся подсчет варозтности выигрыша, т. е. веро- ятности того, что из начального состовииз существует путь в выигрышное состояние. Иными словами, для этой вероятностной струатуры нужно опре- делить веровтность темпоральной формулы пути р®мол, шш, что то же самое, формулы пути съеП(фмол. Определим множества Я"», У"' и Я.: Я~ = (/огмв),8»м )мол), бл 81)8»» ь/Зги) )заач,4, 5 6, 8, 9, 10~ Здесь, несмотря на то, по формула /пм выполнаеггл во всех соспмниях струк/урн, состояние !ооге вюпочено в множество Я"', шккольху из зтого состояния недостижимо состояние, помеченное мои, Обозначим х, вероятность вмигрыша из сооговнив /.
Очевидно, что х,— зю вероятность выполнения в иктояннн 1 темпоральной формулм р®мол=лигу®ион, Составим систему уравнений лля вероятнссгей к,, учитывая, что з „=1.0,а х ь --О: х =8/36+3/Збхг+4/Збхз+5/Збхз+5/Заза+4/Збгз+3/Збхс хз = 27/Збзз + 3/36 рлзш и зэ 26/36«з + 4/36 «с = 25/Зб«с+5/36 «з = 25/36«з + 5/36 .«е 26/36«з + 4/36 «!е 27/36«!с+3/36 Решение сисгемы легко находится вручную. Резуяьтвт « „= 244/495 определшт вероятность перехода нз начального состгжния ялвт в сссюяние мал. Это значит, что шансы [выиграть: проиграть] на ставке "Тйе Рож йе/" без мошенничества и при идеальных игрельных костях составляют [244; 251], т.
е. выигрыш казино в среднем больше выигрыше игрока на этой ставке приблизительно ня 3 1ь Очевидна ограниченность описанной здесь техники: в кялаом состоянии вероятностной структуры мы можем подсчитать вероятность толыго простейших формул пуси, подформулы которых — втомернме предикяты. В результате згих вычислений получаюзоя значения вероятвктей выполнения этих формул, я не логические значения "исшнла" илн "лозсь" выоолннмостн темпорвльной формулы в конкретном состоянии, что ввлястся основой аягоритмов мвркнровки, которые используются в анализе выполнимости формул темпоральной логики СП. на обычной струкгуре Кринке. Поэтому использовать зти численньк результзты дыме прн проверке выполнимости сложной темпорвльной формулы СП.
невозможно. Очевидным решением здесь явлштся требование включить в сему темпорвльную форыулу пороговое значение вероятности выполнения формулы в конкретном состоянии. Прн анализе можно сравнить численное значение подсчитанной вероятности выполнения формулы в данном состоянии с этим пороговым значением. В результате такого срзвнення в кшкдом состоянии получатся нстинностные значения "исмена" нлн "лоске", покззыеякхцие, удовлепюряется или нет темпорелыпш вероятностная формула в этом состоянии, Полученные истннностные результаты могуг быль мспользоеаны дпя дальнейшего анализа. Пр ер 55.6 Запишем нвйденные в примере!1.5 вероятности Уе(янйВр) для всех состояний еерозтвктной струкгурм М, (см.
рис. 11.1): УЬ(яс,4 Вр) = 05, Уз(ям 9Вр) = 06, Уе(~,9Вр) 1, Уз(зз, фВр) = 1. У ( „еВр)-0. В бе! чение рн может го сос селим ВО«мы мелью 11.2 И Вб где -е Каки~ Рр Оф 1м Ц, Ри ей- льгих смаул до- зой Выберем в качестве порога выполнемна формулм РПР в нашем примере зшь чение Жб. Пусть запись ~сь(г,ОПр) обозначит следующее угвсрлшение: "с вероатностыо по.б формула пути СПр выполняется в состоянии з ".
Такое угверяшение молит быть либо истинным, либо ложным. Для структуры агг: Яоь(ге,ОУр)=уста — в гс формула рбр ле выполняется с верояг постыл Ж61 ~ь(г! ОУР) а"ие в г! формула ЯПР Выполнаетта с асйоаг пастью сб.б. В общем виде формула У р(а), где ъ,ноф, з. р н [О, 1] — нсюлормг вероятность, '- ' н (>,щс,я» — зшщ отношения, а — темпоральная формула пути. может рассматриваться как формула новой темпдрвтьной логики для текуще- го состояния. Тммя логика, которая носит наивные "Вероятлостнойлоглкан еелмжсегася ерсмелн", нли РСП.
(РгоЬаЬйьйс СТЦ, явлаетса одним нз возможных расширений Обычной логики СП, Определим зтрг логану фпр. ,ПО- ыв ние гим пни аис, СО- аны со- 11.2. Вероятностная логика ветвящегося времени (РгоЬаЬИ(або СТ1„РСТЦ и верификация вероятностных моделей Формулы логики РСП. являются формулами состояний н имеют следующий еид: йнмО~-,Р1<Р! и!Рз ~яр(а), где -а (с,б,,щ>», а формузщ а — формула пупс ах Хаг1вг$ЛРз. Как и в поппе 1.Тр операторы Р и О выражшотся через Ппй1: угри Угие1ур ~ри 11 !р гласе ы Смысл этого определения такой: в состоянии з структуры М аероатностная мера -р выполняется для формулы луги а тогда и только тогда, когда с этой мерой будет выбран такой путь нз состояния з, на котором выполняется формула а.
Подобно тому, как в логике СП. кмклый темпорааьный опера- торХ, П, Р или С предварен ментором пути А (всеобпгностн) нлн Е (существованвг), в логике РСП. мщщый темпоральный оператор предварен вероятностным оператором У„„который монне назвать вероятностным "кмыторам". В РСП. нег квапоров путей, которые используются в логике СП;. вместо формулы СТ1. Аа с квантором всеобщности (вьпюлненне формулы а йа всех путях) монет быль использована формула РСТ1, У„, (а) . Семантика формулы У„,(а) такова, что формула а выполняется "почти всегда". Формулу РСТ1 У,е (а) часто момно использовать вместо фгюмулы ва с квантором существования. Семантика формулы У,е(а) следующая: с неюторой, не равной 0 вероятностью из текущего сосгоания момст быль выбран путь, нв котором формула пугн а выполняетсл.
Однако формулы Аа и У~(а) не эквивалентны. Попелем зто на простом примере. не н~ не в~ лени По с рис, в это Пост лыр Пуст опер Спрв отно~ аеро3 буде Н р П У, х,=1 дает х, =1. Таким обрезом, при любых значениях р, не рваных б, для состояния з этой структуры выполняется формула Уы(йа). В то же время существует путь з — бесконечный цикл в состоянии з . нв котором никогда Рис 11А Пр мр всрояпквтмзй структуры Преплир 11.$ Рассмотрим пример вервпнсстной струщуры рис.
11эй Полсчитаем верою- ность выполнения формулы ра для состояний этой структуры. Мномества оы, б н ет здесь таковы: Ям И, б (г), и ет =(э) . Система уравнений: т, =(1-р)л,+р+х егг евв хм. Е рен ~ым ике ор- Се- :о- не наступит л . Следовательно, формула Ара в состоянии э этой структуры не выполнаекл. Отсюда следует, что формулы дра и У,(ра) не эквивалентны.
По аюйству дуальности можно утверждать, чт формулы Еба н 5~э(Оа) также не эквивалентны. Дейсшншльно, на той же всроягноопюй структуре рнс. 11.4 формула ЕО а в состсинии э выволнястся, а формула У,э(О а) в этом состоянии не выполняется. Посгронм алгоритмы вычисления истинности формул логики РСП, Формулы РСТ1, инюрпрстнруются нвд помеченными аероятностнымн структурами. Пусть М = (Я,гс, Р,АР, б) тшшя структура (см. определение 11.1). Семантика операторов РСТ1. такова: М,я)=Р 11Р т пь(г) М,я( ир 1р М э1ир М,э~ щ»рт 117 М,э~=и~ иянМ,г~ иэ.
М,э1=У (и) ф' Рт(ттхвраГ7им,)к1ва)-р Справедливость трех первых соотношений очевидна. Смысл последиего соотношения следующий. В верокпюспгой структуре М., находящейся в оо. стоянии э, будет выполшпься формула У р(а) тогда м только тогда, когда вероятность того, что на вычислениях, начиншощнхся в г, формула пути а буд уд р реб - р. Например: а Ушэ(Хб) — р я, нэ д ущ у реход в состояние, в котором выполняется б, не больше О.1; П Усат (тП г) — вероятность того, что на путях нэ данного соспмння вмполннтся формула пути (РП г), больше 0.7; П Ушэ(УшэХР)Ю г — вероятность того, что на путях иэ данного состояния выполшпся формула пути (фэ тХР) 6-», меньше, чем О.З.
Алгоритм вернфикапин для РСТ1. Рабопшт так же, как для СП.: О с помощью синтаксического шшлиеа определмотся подформулы формулы Р; Главе П бр ешпвксическое дерево формулы 0 логики РСП. проходитсв снизу вверх; П для юпклой подформулы состояния и формулы 0 определяется множество Йп(Ч~) тех состояний, которые удовлетворяют формуяе состояния чг ' г г если Яг У р (и) 'ю ВВРОЯТ'ВОсгп Всех тех и) ~мй кз сас'юЯниЯ 3 ИВ жгга" рых формула пути и истинна, вычисляются н сравниваются с вероятностной границей — р, давая в результате лля формулы Чг в конкретном состоянии з значение грие или~аЬВ. Как н в логике СТ)., будем считать, что темпораяьнзд формула 0 логики РСП.
выполняется лля всей структуры тогда и только тогда, когда и выпол- няется в начальном состоянии егруктуры. Обозначим Яаг(О): Я-+ (О,1) — вектор, который для состояния з ВЯ дает истннностиое значение ! (Оие), если Мя Рчр, н 0 гуа)зе ) в противибм слу- чае. Тогда: Йп(У (Ха))=(Чзпб1хг-р), где х, =Рхйгз(0).
При р15.У Вычислим Яат(УН,В(ХР)) для вероятностной структуры М, примера 11.1, т. е, вектоР истинностных значений лла фоРмУлм У па(ХР) на этой стРУктУ- ре. На рис. 11,5 показано, что для этого необходимо матрнну Р вероятностей переходов структуры м, умножить на вектор Явт(0), т. е. на велюр, опре- делающий дяя кюкдого состояния, выполняется формула 0 в этом соспмнии ини нет. В результате пояучеем вектор Уе(ХВ) = (0.7; 0.4; 1.0 0.0; 1.О) верокнвктей выполнения формулы Хй на сасгоаннвх структуры Мы Фор- НУЛВ состОЯний Уме(хд) Удавлствойястая В СРУктУРВ м~ В сОстОЯниЯ» зс, Зз И 44 У л(хр) =(1;0;1101) Вычисление вектора Яат дия формулы луги У р(01)Р) выполняегая с по- мощью линейных уравнений, еаставмнных нв основе определенных выше МиожЕСТВ гчр, Я И ЯТ, Рнс.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
