2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 70
Текст из файла (страница 70)
Видно, что определение неиодяллпяю мочки оператора ткв (2) более слабое, чем семантическое определение: в нем отсутствует информация о семантике формулы Ерр и следующем из нее аягорпмме построения множества акте. Поэтому неподвижной точкой оператора ткг„(2) может быль не только искомое множество Я~те, но и те множества состояний, которме Ие являются решением нашей проблемы.
В частности, все множество Я удовлетворяет определению (1): действительно, Я вклкимст и йе, н все те состояния, из которых за один шаг можно достичь состояний из Я. Очевидно, что Я вЂ” наибольшая неподвюкнвя точка оператора ткз, (2)=Я ~.~ЕЕ(2). Ясно цозтому, что искомое множество йкв — зго наимеиыилл неподвижнвл точка оператора ткв (2) . Докюкеы зто. Докюкем сначала, что оператор тяв, монотонный. г со- ~утгь нтся ение ЛЕММА 14И Оператор тазе мошппииый.
Доказательство Пусть 2 ~ 21. Тогда мшхкество состояний, из которых есть персию в 2 является подмножеством состояний, у которых есть переход в 21 . Поскольку операция объединения множеств монотонна, то оператор ткя,, хак компози- шм монотонных операторов, монотонен. ол В пта- ЛЕММА 10З Мнакесгво Даве,— эго нянмзньшвя йеподвмкнвя точка оператора газ, (2) = йе и ЕР(2) . Доказательство Дохвштельство леммы 10.3 проводится по шшукшш. Докажем сначала, что т'кве (Э) ~ Даве при любом 1.
Поскольку т кве (И) ~ И, зто соотношение верно для 1=0. Прелполаюгм теперь, что т"яве(Э)~йкв при некотором Гпеев $0 натуральном л. Поскольку, согласно Лемме гй,2, оператор тс„„монотонный, применив его к левой и правой части соотношения т"кр„(8) с дар, пш$Учим таре(т крс(З))отаре(Дррс). На Дррс $юпаДВижнва тОчкв т.е. ткрр(Дрр )=Даре.
Отсюда получаем справедливость вндуктшюого шага: 'рле(а9а Дкр,. Йпэжем теперь, что дср ~ т"рве(ц$) . А нмеию, покажем, что если для не$ютайаго з$ а Я Всйна, 'пО 5$ =дррр, та з$ НРниадлсжит 'пиоВВ и т кр ($с$). ЕСЛИ З$ =Даре, та На СтРУКтУРЕ КРНПКС С ППЮШЕНИЕМ ПЕРЕХОДОВ й СУШЕСтВУВТ такой НУгь з$,гз,зэ, ... К$, 'ПО з$ =Де. ДОкю$юм па индркцип, чта пйи яюбой длине этого отрезка пут» также справедливо и з$ и т'вр, ($с$) . Зто очевидно лля $=1, шюкальку т'кр (И$) дс.
для обоснования инаукпюнога И$ш» ПРслпала$кпм, чта нв О$РУК$УРс КРИН«е СУпюашУВТ НУ$» Р$,зз,зэ, ... з„ ИРП нскОтайам ПВЗУР$шьнам и 3» ПДВ и пйи Ртам Р$ с т крс(10). Покюкем, что если из з, существует путь К$,гз,зэ,...з„,, з$ =Дар, и р„,$ВДс, то верно и р$ат$кре(8). По иилувтнвному предположению, заст"кра(Я). Но поскольку (з„зз)сй, та н з, ст $вр (8). Лемма доюззана. Таким образом, множество Дср является минимальной неподвюкной точкой этого оператора, т. ес Дькр = $$У.ткр (2) = РЕ. Дс $.$ ЕХ(У) Поскольку оператор ткр монотонный, то в соответствии с теоремой Тарского.его минимальная неподвюкная точка мгскет быть вычислена простой "аппроксимацией снизу".
Приведем символьный алгоритм вычисления наименьшей неподвижной точки монотонного оператора тки (У) = Д $эЕХ(Я), который н являеюя алгоритмом верификации для подфармулы КРО. Этст алгорьпм оперирует харюггеристическими булевыми функциями множеств, предспюленнымн в форме ВОО. В алгорипее у ЭТО ХВ КОТОР чески ЕРО, Опера шеню стнчм Прим Расом ТВОРВ$ ао со тару ( З~Т$ лом ш торых ДОСП$' трн д< у$ке Ь добаю ление миалсе шину помеч$ множа ЛОПОЛ $ ~ прн оче- зто харшпернстнчесшш функция множества состоаннй структуры Крнпке, на которых аыполнаетса темпойальнал фоРМУлв Р, Хате — зто хайахтейнстн ческаа функция множества состояний, на которых выполняется формула ЕРФ,- Х*ч — функцня, залающвя вспомогательное множество состояний, Оператор тач аю вычнгляет опервцню "Обратный образ" ограниченна отношення й на множестве состояннй структуры Крцпке, ъщанном харнгшрнстнческой фУншвшй Х че ° «ч»: Газэеч // Вначале ссреяеаячм сзсяае ыкнеозве ссогсяяяа ае х':- х Узн .
Х,ч Эх', ...,х'„чзч1хм...,х„х'н..., х',1 ь Х (Я'о...,к'01/ // тес гх"! ° Вям 1жч е Х'зч звеаан Хчч ~ного н нню, юкя- чкой про- чног)- 'рж- ммн Пример 10.10 Рассмотрим пример вычисления состояний структуры Крнпке, удовлетворяющнх темпоральной формуле ЕР/, если уже построено множась во сосгояннй Д~, удовлетворяющнх формуле / тряс. 10.13). это множество Дкв/ строится как наименьшая непспвнжнав точка оператора тхг/(2) = Д/ ь/ЕХ(У) — предел последовательнсстн прнблнженнй И ~ ткв/(Ы) К тзш/(И) ~ тзкв/(И) ~ .... Рнс. 10.13 показывает, что на кшкдом шаге к множеству помеченных состояний добавляются состояннв, в которых выпслняеюа / н все те состовння, нз которых за одни шаг макно достнчь какого-лнбо уяге помеченного амтояння.
На первом шаге помечакп.- ся состояния Д/. Вычисление ткв/ (И) = ткь/(Д/) в нашем примере дает трн дополн~пельных состояння — нз каждого нз ннх существует переход в уже помеченные состояння. Явные алгормгмы маркировки состоаннй будут добавлщь нх последовательно, снмвольные алгоритмы используют предспшление ВПП характернстнческнх функций, опнсывающнх соотвагствующне множества. На третьем шаге вычнсленне т хг/(И) добавляет еще одну веря шину к ранее помеченным: нз нее за однц переход попадаем в множество помеченных ранее состояний. Последующее прммененне преобразоевння к множеству уже помеченных состояннй нашего примера не добавит нн одного дополнкгельною ссспжння. Алгоритм завершается: мм прншлн к непопвшк- тг(а) а, ьэ ЕХтэа (йЗ) 4 Рие !0.10, эь !!а троение наименьшей ваподеижноп тсч«н оаереюре твяе(2)=Д ьэЕХ(У) !к примеру !О!О) иой точке преобразования.
Поскольку пронелура была начата с пустого множесгва, пспученная неподвюкнал точка — наименьшая. На рис. 10.14 показана диаграмма Хассе всех неподвижных точек этого огмратора (множества затемненных вершин). Для примера! ОЛО таких рашичиых множеств шпъ, все они образуют решетку. Одной из неподвижных точек является все множество Я вЂ” оно включает в себя как множество Дг, так н все состояния, из которых доспскимы любые уже помеченные состояния. Это наибольшая из неподвижных точек оператора твгг (Е) . Решением задачи примера ! 0.10 является наименьшая из этих неподяюкных точек. Алгоритмы построения нанболылей и наименьшей неподвижных точек монотонного преобраюавния т на мшвкестве Я дает теорема Тарского — зто последовательности прнблшкений т~(Я), т!(Я), тз(о),...
и "РВЗе чу ле 0 оп П мь Реху1 дея 2. те(И), т'(8), тт(0)„... Остальные неподвижные точка махно построить перебором. Здесь онн построены по следукюыму правилу, лнатуеьюму видом оператора тха. (Е): неподвижная точка оператора тхву (Е) п Ду ьи ЕХ(У)— это любое множество амтояннй М, которое включает в себя множество Оу, н еслн в М входит состояние я, то в М входят н все те состоання, нз катормх я доспскнмо. Рнс.
19д4. Решена нелсавнанмх точек оверысра тхв прямера 1О. 1О Два 1 хацм! на м~ мнон мноз ме В1 В де1 кото1 (кх~ ИЪЩИ ву Я обрю во Я Все ~ нанй лля б балы струя идом ')— ' 0г кото- 10.9. Определение темпоральных формул СТ(. через неподвижные точки операторов Для друпсг формул СП также разработаны итеративные алгоритмы верификации, находящие нужную неподвижную точку соответствующего оператора на мноямсгае состояний структуры Крипке. Все алгоритмы построения этих множеств манипулируют не отдельными состозннямц множеств, а целымн множествами, заданными характеристическими булевыми функциямн в форме В00. В действительности, необходимо построить лишь алгоритмы для тех формул, которые составляют спин ю возможных базисов СП., например, (ЕХ~р, ЕСкр, Е(рк0крз)) .
Алгоритм длз формулы Ехкр построен выше, он не итеративный и исходит множество Дкх сосюяннй по заданному множеству Я состояний простыми операциями (в часпнктн, операцией "Обратный образ" ) ющ В00 харакюристических булевых функций, задающих мншкест- воЯ. Все искомме неподвюкнме точки для темпорзльных формуя СТŠ— либо наибольшие, либо наименьшие. Построим, например, итеративный алгоритм для формулы ЕСкр: зтст ви'оритм интересен тем, что он будет искать наибольшую неподвижную точку некоторого оператора нв мноясестве состояний структуры Кринке.
Покажем, что: П мнвкество Дяп состояний структуры Кринке, удовлетворяющих формуле ЕПкр, явлжтся неподвижной точкой мекогорого оператора тзд нв множестве состояний структуры Кринке; 0 опеРатоР тгд монотонный; ГУ множество Я~~ является нанбольшей неподвюкной точкой оператоРа тасе н, следоаательао, по тсоРеме ТаРского, оно может быть найдено простым алгоритмом — "аппроксимацией сверху": (я) т~ (я) тз (я) Рекурсивное определение темпорвмной формуям ЕСкр следующее (см раз- дезйугл. Л: гневе щ ЕСф = ф л ЕХ (ЕСф) < ~ущ~~~вует такой путь из текущего состояния, ео всех состояниях которо.
го темпоральная формула <р выполняема — это то же самое, что ф зыполняетса в текущем состояние и существует такой путь, в следующем состоании которого форыула ЕСф выполняется. На основании этого определения мщкно записать: (',Гасе=О г<ЕХ(Дап ) множество соспмний, на которых формула ЕС<р истинна — это толы<о такие состояния среди состояний Яе, что нз них существует переход в состояния, в которых формула ЕСф истинна, Отсюла сразу следует, что можно построить оператор та~ ва мщпкестве соспмннй структуры Кришне тгл„(Е) = йе г< ЕХ(2) такой, что искомое мнакество (уао состояний структуры Кринке, на которых выполняеюя формула ЕСф, язляетсв неподвижной точкой этого оператора: ткп (Дао )=Д г<ЕХ(Дво )=Дкп Но какой из возможных иеподвюкных точек является искомое мнщкество? Рассмогрнм два определенна.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
