2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 30
Текст из файла (страница 30)
Допускающие состояния искомого автомата Бюхи Условия приема входных м -слов автоматом Бюхн допкно быть определено юя кюкдой подформулы исходной формулы ГД. Это требование реализуется следующим обрзюм: искомый автомат Бюхи будем строить как Обобщенный автомат Бюхн В, с множеством принимающих состояний г (Уч ~ цгвс1(Гд)(. Каждое множество У„будет включать все те состоявия, в которых Обязательства выполнения формулы Гр будут реализованы. Дяя атомарного предиката р обязательства его вмполнения реализуются невГкредстаенно в том состоянии, которое вкяючаст этот преднкат. Поэтому в искомом автомате Бюхн не будет состояний, в которых не реализованы обязательства выполнения р.
Поэтому множество принимающих состояний У„ автомата В будет совпадюь со ВСЕМ мНОжЕСтВОМ СсетОяиий В . Аналогично строится множество прннимакиких состояний дкя ХГд: по построению, это обязательство выполнения формулы Гд будет реализовано в кюкдом следующем сосгоании любого вычисления и во всех последующих состоанивх. Поэтому перечисленные формулы можно вообще не учитывать при щютрееини допускающих состояний обобщенного автомата В„.
Более сданными случаямн явллнпся формула рГПГДГ н выводимые формулы рчг„счГГ , например, для калщой формулы а, = Гдгсчг„каторая встречается ° замыкании формулы Гд, в искомом обобщенном автомате Бюхи В множество У, допускмощнх состояний составляют все атомы формулы ГД, кроме тех, которые определяют нереализованные обюательстяа выполнениа формулм а,. Множества У, допускающих сосгояний для формул РЧГГ н СГдГ определянгюя аналогично. Построение автомата Бюхи по формуле (.'П. ! Построение искомого автомата Бюхи мяполннть теперь очень просю. Очевидно, что автомат Бюхи, допусюиощий асе ы -слова, нв которых выполняеп ся формула е, может ныеть только те состояния, которые могут быть поыеченм атомами формулы е.
Поэтому все внппя формулы ф, определяемые локвльными прввиламн 81 — Йй, мы и должны принять зв состояние искомого ввтомвтв. Переходы этого автомата определяются правилами Реагюации обвзамельаюм С1 — С4. Начальными состояниями искомого автомата Бюхи должньь очевидно, содержать обязательства вмполнения этой формулы р. . Ф Опредвлвлже474ввщомми Бюхн В 7 Обобщенный автомат Бюхн В „допускаощий всн а слове, нв которых выполняеюя ЬП формула й, опрелвляетсв следующим образом: В,=(О,г ',Д,,Б,Р), гас: ° множество Д состояний В, аютавнкгг всв атомы формулы йп д 2че1, е влфщиг 2ллввтомвтв В„сосюит из подмножеств атомарных предиквтов, над которыми определена формула Е; ° мнвкество 12э начвяьиых состояний В состввямот те втомы формулы Е, в которые входитсвмв формуле р; ь функпня переходов Ь: Д х 2" ь 2о согласована с семантикой формул 1.ТЕ и определяется так: для квждого состояния АиД и множестве Ащ2"г атомарных предиквтов из АР, включенных в атом А, переход 8(А, Агэ2 ) — это максимальное множество твких атомов лгт А'в Д, которые удовлетворяют всем правилам Реааюащю сбяэажельсае С 1 — С4; ° Р= ЦАвД~Е,Пц~( и А няни! еА~ ~в)ПЦI~ встр)»: множество Р=(81...,У„) подмнщкеств допускающих соетоещй обобщенного ввтомвтв Бюхн В, строится тас Р1: Лля квэаой формулы а, ф,11р,, юмора ветре щемя в замыкании формулы р, миоииство Я, в Рсоставяжот такие атомы Пояс~ П1зиь дзя 4 восгр Миов змее 4 поме- яемые формулы р, в которые нли нв входит сама формула п„или вхор Р2: Для халдой подформулы аг Рчг1 замыкания формулы р мНОлмстзю Уг Уг и Р сосзввлякж тамы атомы формулы р, а ко"' торые или не входит сама формула и, илн входит гуг, 03: Дяя каждой подформулы пь Свгь замыкания формулы р мпожеспю У» и В сосшвляют тмпге атомы формулы р.
в жпорые нлн входит сама формула и, кяи не вхолит Чгя. :комо- Оо~ВИ Бюхн 9 юм: Доказательство того, что построенный автомат допускает в точности все те и -слова, нв которых 1.Т3.-формула р выполняетсл, приведено в (191. Поясним построение обобщенного автомата Бюхи В на примерах. рных юхол омов зного в за- гомы Пример 4.1 3 Дяя формул~ % = УР недстерминнроевпный обобпгенный автомат Бюхи В, построенный по привваенным выше правилам, представлен на рнс. 420.
Множество его состояний составляют три атома А', =О, Аз 1Рр~ и Аз = ( р, рр1 (см. пример 4.12,!). Мнсхмспюм начальных состоаннй является ~Аз, Аз~ — именно зтн соспжния помечены формулой Рр. лаю Слева 4 При Авт< пуск ко о Мнакестао допусяакнцих соспжний здесь одно, В (У1~, поскольку в формуле Рр только одна формула вила Рр . Состояние А,жюбще ие включает формулу Рр, а состоаяие Аз включает р, поэтому У, (А,, Аз). Поскольку множество допускающих состояний одно, этот автомат является не обобщенным, а обыкновенным автоматом Бюхи.
Переходы автомата помечены теми наборами атомарных предикатое. которые истинны в исходящем состоянии, точно так же, как в автомате Бюхи, построенном по структуре Кринке. В автомате нет переходов нз состояния Аз в сосгоание А, н переходов нз А, в Аз и Аз (они противоречат правилуСЗ реализации обязательств). Пример 4.14 Автомат Бюхи В . допускающий все бесконечные входные цепочки. на которых выполняется формула р ОРр (см.
пример4.12,2), показан на рис. 4.21. Состояниями этого автомата являются пать атомов формулы ПРр. Начальные состояния этого автомата — Аь и Аэ, те, жпорые помечены формулой Срр. Три состояния недостижимы нз двух начальных состояний (по правилу С4 реалюаяли обюательсме). Множество допускающих состояний автомата состоит ю двух множеств, $ дяя формулы рр, н уз для формулы СРР .
Я1 =Щ в соопютствни с пРавилом 02, Уз (А4, Аз~ в соответствии с правилом (уЗ. рне. 4.21: Автомат Бюхи, лопускиощпй есс ю слоев, ла ипормх вьоюлияется формула СРр Автомат  — обобщенный автомат Бехи. Допуспвяые цепочки автомюа Впг — это все цепочки, которые бесконечное число раз проходят через состояние Аз и через одно из состолвнй множества (Аг,Аз~.
Поэтому этот автомат нмщвяленген обмчному автомату Бюхн с единственным допускмощим состоянием Аэ. Бюх в~(, сбяэ реха рые Гласа е зючаст кольку бщен- ьи, но:я Азв щу С3 на ко- стени т ав- зн на Пйр. ~ фор~й 1по мнил мулы Пример 4.1 6 ь Автомат Бюхи Ве, допускаощий все входные цепочки, на которых выпапмется формула (р чу)П(рлй) (см. пример 412,3), показан на рис. 422.
Допускмощие состояния сбрюуют одно множество, поскольку в формуле только опия подформула вида ф,Пфз. Поэтому автомат Ве — обычный автомат Бюхн. В соответствии с правилом Ш, допускакнцие состояния здесь — все те, которые не включает формулу ф,бфз, и те, которые наряду с формулой ф,йфз включюот формулу рз, Переходы определены правилом реааизаепи сбязажельсюе С2. Пометки на переходах опущены для простоты: каждый переход из состояния А помечен мновюством тех атомарных предикатов, которые истинны в А. рве. 4Л2. Автомат Бюха, лонускмоюнй есе и слова, на которых выполняется формула ф=(рч 4)П(р л й) Пример 4.16 Построим автомат Бюхн для формуяы Е=Хр. Мнщкество соспиний этого автомата —, все подмножестве множеспа (Р,Хр»: Л, к1,4э =(р», .4э =(Р,Хр», еи =(Хр» 1см. пример 4.12,Я.
Множество начваьиых состоЯний автомата Яе =(дэ, 4и) — именно этн два состояние помечены формулой Хр . Функция переходов ограничена единственным правилом выполнения обюательств С1. Множество переходов этого б(4, й1 )=(Л,,Аг)1 б(лц. (р))=(,4,.4»; б(лэ, »р))=(4э,лэ); б(Е„, И )=(Л .4) ° поскольку в формуле р нет ни одной поп»юрмулы вида е,$1еэ, ру или Ср, то в построенном обобщенном автомате Бюхи иет ни одного подмножества лопускающих состояний.
По определению, бесконечное вычисление и допускается в обобщенном автомате Бюхн тогда и только тогда, когда ((ИГ9,нг )1пГ(а)гэргиВ) Прн пустом множестве Р квыпор тг $н Р становится истинным. Поэтому любая бесконечная цепочка в построенном автомате Бюхн допускается. Пример 4.17 Автомат Бюхи, допускающий и-славь на которых выполняется формула РСа (см.
пример 4.12, б), представлен на рис. 4.23. Два состояния, И', н йэ, (а» явл: Са При Авт тор! 9 со ЭВэт лу с лам~ доп1 пуси Рази кото мали тома ряэы авци моли цело Ь,п тома иий долу ги дза хинсг, этого недостижимы из трех начальных состояний Аз, Аг и Аз. По правилу 02 двв фоРмУлы РСл допУсквющим состоЯнием Явлаетса Аз — только в Аз входит формула Са. Для формулы Са по правилу ПЗ допускающими состояниями являются Аз и Аз, потому что в атом Аз не входит а, а в ятом Аз входит Са. Поэтому множество заключительных состояний г"=(э1,рз~, где Я, =(А ), а ~ (А„Аз). Этот автомат мшкно РассматРивать как обычный автомат Бюхи с одним допускакнцнм состоянием Аз . р нли ~ноже- ние о >этому >рмула и Аз, Пример 4.4В Автомат Бюхи Бе, допускщощий все бесконечные входные цепочки, на кп.
торых выполняется формула р (ачЬ)ЮСл (см.пример4Л2,7), имеет 9 состояний. Этот автомат показан на рис.4.24. Начальными состояниями автомата валяются атомы Аз — Аз, потому что только они вкшочшот формулу яг. Переходы авюмата определяются ограничениями, дикгуемыми правилами 42, С4. Нз состоаний Аз,Аь переходы могут вести только в состояния Аз, Аз н Аг, из состояния Ае — в состояния Аз — Аз, а из состоаний Ая и Аг переходм могут вести только в состояния Ав и .4э. Поэтому состояния ~ — Ач являются недостижимыми. Множество гт содержит два множества допускшощнх состояний: для формулы (ач Ь)ПСа это множество (Ав, Аз), а лла фоРмУЯы Са — это множество (Ае, Ая, Аз) .
Отсюда слелУет, что этот автомат можно рассматривать как обычный автомат Бюхн с множеством допускающих состояний (Ая, Аг) . Размер автомата Бюхи, построенного приведенным выше алгоритмом, в некоторых случаях не очень велик. Так, в примере 4.14 нами построен миннмальный автомат Бюхи для формулы Сйр. Однако почти всегда размер автомата Бюхн, построенного этим методом, экспоненцнален относитглыю размера (чишш подформул) формулы 9. Верхняя граница сложности такого автомата 2о(гй) . Минимальный автомат Бюхи, допускающий тот же ззык, может быль значительно меньшим. Например, авюмат Бюхи. допускающий цепочки с бесконечным числом вхождений а н конечным числом вхшкденнй Ь, показан на рис.
4.11. Он имеет тояько два состояния. Эквивалентный автомат Бюхн, пошроенный по приведенноыу здесь алгоритму, имеет 5 состояний (рис. 4242 На рис. 4.15 приведен автомат Бюхи с двумя состояниями, допускающий все папочки, удовлетворяющие формула (р ч д)П(р л9), для 464 Гласа с Аящ матс проз пока пред данн В ча< го яз сына числ~ К,с лесю полн| новы "нмк( нсп1я Имен 4.10. Заключение отнес ными комю нина| шпорой в примере 4.15 построен слакный автомат с шестью состояниями (см.
рис.4.22). Существуют примеры автоматов йохо, дяя которых граница слакнасти 2офЕ не молит быть улучшена. рис 4.24. Автомат Бюхи, лопусмаошнй асс яознюжные е.сама, иа юторых выпояияетея формула (а ч Ь) 0Са Алгоритм якн141 сйесЬ1пб для формул П"з. принимает на вход структуру Кринке М и формулу р логики ьТ1., н в том случае, когда 44 Ьн ф, алгоритм выдаст контрпример — одно из вычислений Ьу, на котором формула р нс вышшнястся.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
