2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 69
Текст из файла (страница 69)
Вгпннкают следующие вопросы: П Сущестует лн какая-нибудь структуризация множестея неподвижных точек опсраторов7 П Какая ш неподвижных точек является решением проблемы, сеяэанной с этим оператором7 О Как найти эзу неподвижную точку2 Отлеты на эти вопросы дшт теоршв Тарского. тоннг йко числе т(т'(, 10.7. Теорема Тарского о неподеи)кной ~о~~а Теорема Та)юкого устанаелняесг сгрукгуру мгкхкестВВ псшцшилшых точек для операторов, которые удоахепюряют одному дополнительному требова- нию: оператор лолжен быть монотонным. О Опрадпгиншв то.й <мононюнньгй Полне иноки Оператор т иа о нюыааеюя монотонным, если для любых 'полмно- паата Р, О множества 8 аыполвытся соопюшенне: Ц,пр а ( ) (а) +" (1 Таким ЛЕМФ Для м< целые о перст Неформаяьно, монотонный ооерпвр — зто такой оператор, прн применении которого к большему аргумегпу мы получим не меньший результат 1рнс.
10.10). Можно пРовеРить, что опеРатоРы т, -тз пРимеРов 10.б — 10.8 Яалакгюл мо- нотонными, а оператор тс примера Нй9 — неьюнотонный. Действнтельно, те((а))=(а); те((а,й))=с1. Очевишю, что лля любого т и любого а, 8 ~ т(о) . Применим люножонлый оператор т к обеим частям этого отношения.
Поскольку оператор т моио- зее ю тонный, то т(Я) д т(т(Я)), т(т(Я)) Рз(т(т(Я))) н т. дс дая любого вдб ть(Я)р~ь4(Я) По „„м Я число шапа ! применения оператора т, не боль|вес, чем ф, цепочка Я Л т(Я) Р тт (Я) Р тз (Я) Р обязательно прилет к неподвюкиой тачке, т. е. прн некотором ('( ))=~(Я)- "(Я). :нтам чеканную имер, иной очек юва- рас. 19.19. Монотонный оператор на Я мно- Полностью аналопшно, если лолояюилмй оператор т применить к пустому множеству И, то через некоторое конечное число шагов 9, не большее, чем ~Я~, применения 'оператора т „цепочка ш ~ т(сч) ~ тз (ш) ~ тз (о1) ~ ...
обязательно придет к неподвижной точке, т. с, при ншштором к', ф'(а))- "(и)= -(а). Таким обрпам, нами доказана следукпцая ломив. ЛЕММА 19.1 Для монотонного оператора т на конечном множесше Я существуют такие целые г', 1, ие бслыиис !Я(, что т'(Я) и тафд) — неполвюкнме тпчан опе1иторв т . енин ~ьтет ~лый оно- н,г. ° .: .ймевта РЕШЕТКМ е т0.0 Решетка — такой частичный нордиск, в который для каждой пары элементов входит и наибольшая нюкняя грань, и наименьшая верхняя грань. Известно, что каждая решетка имеет единственный максимальный н единственный минимальный элементы. Например, множество всех подЫножеств любого (не обязательно конечного) множества являетса решеткой.
Диаграмма Хассе решетки подмножеств конечного множества (см, рнс, 10.7) показывает, что для любой пары А, В подмножеств существует их наибаяыиая нилсяяя грань (получаемаа пересечением множеств А и В) и яамяенышм верхняя грань (получаемея объединением множеств А и В). Максимвеьным элементом решетки множества 2 является множество В, мийнмальныи элементом этой решвши является пустое множество. Структуру множеапш неподвшкных точек монотонных операторов определяет слелукнпжг теорема Терского, которую мы приведем в применении к конечным множествам. ТЕОРЕМА 10.1 (теорема Тарского для конечшии мншкестна) Все неподвижные точки монотонного оперетора на конечном множестве образуют решетку, поэтому среди ннх есть максимальная н минимальная неподвижные точки.
Максимвяьнвя иеподвюкнаа точка монотонного оператора т нв конечном мнсжестяе б (обозначваюя гЛл(У) ) определяется как предел примененна оператора т. к множеству о:зУт(У) =т~(а). Минимальная неподвнжнэи точка монагонного оператора т на конечном мншкестве б 1обозначаезся РУ.т(У)) определяется как предел применении оператора т к пустому множеству: РУт(с) = т~(И) . Выше мы уже выдели, что последовательности: б д т(а) В тз (В) д тз(а) р ... н И~т(И)~тз(И)~тз(И)~... для монотонного оператора т имеют пределы — неподвижные точки (лемма 10Л й Теорема Тарского упюрждает, что зто соотесгстаенно наибольший н наименьший злемшпы решетки, которую образуют все неводеюкнме точки монотонного оператора т на мнвкестве б.
Даиизательспю Докажем теорему Тарского дхи наименьшей неподвюкной точки. Пусть 8— множество с л злемегпвми и пусть Т т"(И). В соапютспшн с лем- мой 1 поде~ точи Ясно 1 ра т~,' То, ч энаж Паст дени непа, боли песк шзчо гов г опер обри не бг Таки ных зукп минь скоп фиш точк Т ор Тес мазь еа ш ~нстссте рам- азынем енса ным ным мле: ко: аб- иеюра лре- ьная е б ~а т про. что рую з б.
мой!О.1, существует такое лКл, что тг(1сГ) т(т~(йГ)) Т, т.е. Т вЂ” неподвшкшш точка оператора т . Должкам, что Т вЂ” наименьшая неполвижнаа точка. Пусть Те — какая-нибудь другая неподвижная точка оператора т, Ясно, что 1о а Т '. Применим оператор т к обеим частям эрго неравенства Ф раз. Из-за монотонности т имеем: та(ку) ~ т" (Т'), откупа следует, что Т~Те. То, гго т (о) — навбааышш неподвижная точка оператора т, доказывается аналогично. Построим диаграммы Хассе неподвижных точек операторов т, -ть приведенных выше примеров 1О.б — 10,9 1рнс. 10.11). Из этого рисунка видно, что неподвюкные точки монотонных операторов тг -тз.образуют решетки.
Наибольшую неподвижную точку монотонных операторов можно получить за несколько шагов применения оператора ко всему множеству б, а наименьшую неподвижную точку этих операторов можно получить за несколько пяь гов применениа оператора к пустому мноягеству й1. Как видно из примера оператора тю у немонотонных операторов неподвижные точки решетку не образуют, н наибольших и/илн наименьших неподвижных точек моямт вике не быть. Таким сбравзм, теорема Тарского не только определяет структуру неподшскных точек монотонных операторов на конечнмх множествах (асс они образуют решетку), но и ласт простые алгоритмы вычисления максимальной и минимальной неподвшкных точек этих операторов.
Важносгь теоремы Тарского в том, что во многих приложениях, в том числе н в символьной верификации, важны именно максимальные и/нлн минимальные неподвшкньм точки операторов. Теорема Тарского имеет непосредственное практическое применение. Пусть теч — монотонный оператор на мнакестве б. Алгоргмм вычисления макеймааьной неподвшкной точки оператора тес: л :- зг ие в:-лг В; таю 1 В Гг вязе ш» вю раева то Алтарное вмчноленна мннмнавиой неподлинной точка оператора там А: Э' н:-л; л: тао~ в )ю вы в вм автово Л рав тотт.
днатремкне лассе неполвмкнмк точек операторое панаево |ОΠ— ~ Од тч ло нн коне иа зо комн вода~ Верн А(у~ имев мнол окав! непо, Теорема Тарского гармпирует завершение этих алгоритмов эа конечное число шагов, не большее мощности Я. На рис. 10.12 приведен пример некоторой конечной решетки н множества неподвшкных точек монотонного оператора иа этой решетке (затемненные узлы), которое само образует решепгу. Огрел кеми на рисунке показаны пути достижения наименьшей и наибольшей не подвшкных точек этого оператора по вышеприведенным алгоритмам.
Рис. 16.12. Пример ревмтяи исполвюаимх точек меюиеннепз Огнратсрв 10.8. Символьный алгоритм верификации для формулы Ергр Вернемся к анализу темпоральных формул СП;. ЕРО, Арф, Е(ег~11СЗ), А(фгУРТ), ЕСзр и АС~р. Теоретический материал предыдущего раздела имеет непгкредственное отношение к разработке алгоритмов нахождения множеств состояний структуры Кринке, удовлепюрмощих этим формулам: Окаэыыгстся, ссс эти мнОлмстВВ ВВляклса нанмсньшимн нли наибольшими неподвюкными точками некоторых операторов. Рассмотрим сначала формулу Ерр.
Обозначим Оч множество состояний струатуры Кринке, на которых выполняетсв формула чг. Дла формулы ЕЕ~1 гэмее ю щютановка задачи верификации следующая. Пусть ющстно множество со- стоаний Яе. Необходимо найти миожеетво состояний Япе, Вспомним рекурсивное определение формулы Ерр (см. ран)ез З.У)г ЕРгэ = р ч ЕХ(ЕР <р) "существует путь из текущего состояния. на котором формула и когда- нибудь выполнпгся (Ерр) — это то же самое, что нли й выполняегся в те- кущем состоянии (будущее включает иасюящее), илн существует такой пугь, чго в слелующем состоянии этого пути формула ЕРр выполннтся (ЕХ ЕР Сг)".
Аналогичное рекурсяиное определение имеют остальные формулы СП, По рекурсивному определению формулы ЕР р мщкно записать определение множесща Яяпе состояний, на которых выполняегся ЕРР: Я,„,=а, ЕХ(Якз,) Рассмотрим следующий оператор на множесще состояний структуры Кринке: ткгтЯ=ЯеиЕХЯ Оператор тат, по множеству Е сгронт обьединеняе двух множеств: множества Ц и множества тех состояний, нз кмкдого ю которых есть переход в соспииия множеспю 2, являющегося аргументом оператора ткг .
Подставим вместо аргумента с искомое множество Ягл . В соответствии с рекурсивным определением мщимстеа Яйве модно записать Ящ, =таке(Явке), Зто значит, что искомое множество Якг есть неподвюкная точка монотонного оператора таге. Но неподвюкных точек у оперюора макет быть много. Вопрос в том„какая из неподвижных точек нам нужна г Вспомним дяи определения. (П Неющвюкиап точка еиератврв ткве(2) = Я, ггЕХ(2) определяется так; это любое мнщкество состояний л, включающее только такие состояния ю мигпкяствв Я, нз которых ю одни юаг можно достичь состояанй'из Л. Вндг бое, тике толы явлю гаер! ния, й— но щ гонги моно Дека Пуси являе опера ЛЕМ тяге) Доюк Доки г'кге' верно (П) Семавтака формульг ЕР р опредежмтев твк: зто всв таас состояния, из которых сушествуат путь в состояние, на котором формула р выпол- З„р б Е21.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
