2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 85
Текст из файла (страница 85)
Дав всех состояний д вычисления и, возмотных до состояния дз,+4, вы. полнястсв д ~ т ч л. Действительно: П для всех состояний де+с5', где 7е (онх 0) и 4'а[0 О 7], выполняется де+4 Нт; П дая ВСЕХ СОСГОШШй д~+ЬГ„Гдс д, (ООХч07) Н И'И[00], аЫПОЛНястеа 4~+4'Нтчл; П ллл всех состояний ~+4', где дз=(л;х О) и й е[О,И] [0,0.5], выполняется дз ег7'Нт л. Временной автомат А яшшется моделью формулы состояний Ф логики ТСТ1. тогда н только тогда, когда формула Ф выполняется в,его начальном состоянии (1осс," тс): А ~ Ф ф' (!осе,ге) 1= Ф. О), вы- Введенне формульньш чшэв На рнс. 12.17, 6 видно, что для проверки выполнимости формулы Ф ф;Вуф' на вмчисленни а = Яет-Ас -ь Я~ -А~ -+ зз -+ ...
вР менного автомата Ат, начинающегося с состовния яе, необходимо вычисление о представить в реальном времени г, которое протекло с момента прихода временного автомата в соспжнне яс. Но зто время могут отсчитывать дополнительнме локальные часы, шпорые должны быль сброшены в О в начальном состоянии вычисления и.
Для проверки выполненна формулы Ф на вычислении и введем ео временной автомат А новые локаяьные часы я с единственной целью — измерение временного интервала, прошедшего с начала вычисления. Эти новые часы нюывыотся Формульлымн часами. Ограничение времени У, стоящее у темпорального оператора 11, может быть теперь представлено как ограничение ге Л, наложенное на эти локаяьные часы. Формулу луги ОЯ,фз логики ТСТ1. можно представить как формулу (ф1 о фз ) В(фз л я е А) логики СТЕ прн условии, что часы з сброшены вО в начальном состоянии этого пути.
Выполнимость формулы соспжний Ф = Е(ф,б,фз) логики ТСТЕ в состоянии я временного автомата при наличии "формульных" часов я определяет. ся так: з!=Е(О~Вгфз) Щ' я(яч0) ~ Е((ф~ мфз)В(фа лап,У)) — в состоянии з выполняется формула Ф = Е(ф16зфз) логики ТСП. иногда п только тогда, когда при сброшенных в этом состоании формульных часй я выполняется формула Фсгь = Е((р~ ч фз)В(фз л а п,У)) логики СП.. Анвлогично определяется вмполннмость формулы А(фб,фз) .
Для выводимых формул Р и С, при условии, что часы я сбрвсышжпся в начальном состоянии того вычисления, на котором проаерясшя формула, имеем соотношения, позволяющие любую формулу логики ТСП. свестп гуаме 12 к формуле логики СП. при введенных спепивяыю двя этой формулы дополнительных "формульных" чесма Рзф=атмПзф =Р(фл(зи г)) Огф= Уэ-ф=-,Р( фл(зпр)) Р-((за.У)пьф)=О((за.у)кзф) Ограничение зеу можно рассматривать как атомарный предикат графа регионов, построенного по автомату А с введенными дополнительными формульными чжжми я, сбрасываемыми в том состоянии, в котором проверяется выполнение соответствующих формул сосгояннй.
Такой временной автомат нюовем А Э з . ЛЕММА 122 Пусть два состояния э н О системм переходов Т(А Э з) находятся в отношении и, т, е. И [С]. Тогда для любой формулы Ф логики ТСП.'справед- Т(АЭя),э~чф ф' Т(АЭз) д~ Фстс. Спрммдлнвость этой леммы очевидна: "формульные" чаем я ничем не отличаются от других локальных часов временного автомата А. Таким образом, проверка выполнимости формулы Ф логики ТСТС дяя временного автомата А может быть сведена к проверке выполнимости преобразованной формулы Фсгз логики СП. на графе репюнов й(А Э г) автомата А Э я с добавленными "формульнымн" часами *.
При условии, что формулы ф, и фэ не содержат подформул, временные интервалы которых отличны от [О,ю), для проверки выполнимости формул Е(ф|бзфз), Д(ф~б~фэ) (н выводимых из нпх формул Еузф, АРзф, ЕО гф, Дбзф ) во вРеменном автомате А необходимо выполнть слелУющие Шаги: 1. Для формулы Ф логики ТСП» содержащей временной интервал У, в ав.
томат А добаввяютса формульные часы з. Потолок С, часов з определается максимальной константой в интервале у. Новый временной автомат назовем А Э я . Условие з ар является дополнительным ограничением в множестве Г ераниченнй на локальные часы автомата А Э э. 2. Формула Ф логики ТСП содерямюая временной иючрввл ахи[О, с), эамевмтся на формулу Фсгс логики СП.
по правияам: ЕО Н! ф 4. В ж Прп Прог 1. В к< 2. Ф О ыми ове!ной Е(фзбн/фз) изменяется ив Е[(ф$'Гфз)5(фзлхв.У)) ЕРхф заменяеюя нв ЕР(ф л(х е.У)) ЕС ф звменястсяив ЕС((хе.У)юф) Формулы с кввнтором всеобщности преобразуются внвлогично. 3. Обычный влгорипе проверки модели двя формул логики СП. применяется к трефу регионов Й(АФх,хв(х=О)). Сосюянне хс является нячильным состоянием графа регионов Й(А), в нем проверяется выполнением формулы Ф для временного автомата А. 4. Во временном автомате А формула Ф логики ТСП. вмполнястся тогда и только тогда, когда формула Фсгь выполняется в состоянии хс(хм О) грвфв регионов Й(АЭх,хв(х=О)): А! Ф ф3г хе(хшО)~.Фсзз аи- вре- брв- ин- мул !хф.
, ве- зде- Пример 42ЛА Проверим, выпслияетсв ли формула Ф = ЛСя,л логики ТСТ!. для временного автомата Ат, представленного нв рнс. 12.17, а. Формуяв Ф будет выполшпъся для временною автомате, если онв булет выполняться в его нвчввьном состашии. Проверку будем выполнять по шагам: 1. В автомат Ат вводим дополнительные к х формульные чясм х, звдвчв которых — измерять отреши времени, прошедший шиле стерта ввтомвтв из начального состояния. Потолок С, этик чвсов равен 1 — это мвшамвльнпьконстянтв в о~рвиичении У формулы Ф.
2, Формулу Ф ЛС !л логики ТСТ1.заменяем формулой Фсгь. Флэт ЛС((х51)юл) ЕР ((хя1)»и) ЕР((х51)л — ш). Ограничения нв формульные чвсм представлены здесь атомарным предикатом (хь1). 3. Строим граф регионов Й=Й(А!Эх,хс(хшб)) (рис.12.!РР Этот граф строится для двух чясов, х и х, с потолками С„=! и С 1. Поскольку формуле Фстз проверяется для начального состояния Аг, "формульные" часы х уствновяинм в О в начальном состоянии графе рштшнов Й, "Фор- Влояи Пусть чвюив ми у цедур лами, случэ автом ла лся спето. регио в алгс Будок сОсто време Ф не гионс граф нов г Приз Пров Пост1 подф гное в аг г В ссх она ~ стош пнем Ер подб Рис. 12.13.
Граф регноиов Я(Ат 9 я) втммеиюго автомата Ат. с добавленными формульвыми часами, сброиввиыми в иачввьисм состоянии мульные" часы я в том графе не сбрасывыотся, они просто отсчитывают время, прошедшее в вычислениях после того, как были установлены в О в состоянии ге. 4. Проверку выполнимости СтЬ-формулы Фстс Ер((я<1)д н) лля гртфа регионов й(Ат 9 г, ге(я ы О)) проведем обычным образом: последовательно находим множества во состоаний, удовлепаряшших подформулам формулы Фсгс (см. рис.
12.18): у;=(як1); Бн(Х)=(зе зг гз гз зя ят гтс) Уг= % ши(Уг)=(яс т~ зз.зп зш я~з) - .рз=у(.Л: ~ (Л)-(яс'и яз) У4 ЕРГЗ тг(Л) (зе з! гз) Фстс Св: бш(Фсп)=(яз-Нз) Формуле Фстс = — ЕР((с «) и -и) не выполняется в начввьном состоянии графа репюнов й(Ат Юк,яе(яг О)), и, слеловательно, формула Ф=АС тл не выполняется во временном автомате Ат. мист явО ~иии !я!и Вложенные формулы ТСТЕ Пусть формула Ф логики ТСТАВ содержит вжвкенные подформулы, включающие темпоральные операторы ь1, Р или С с временнмми ограничениями l, отличными ст [О,ю) . Классический алгоритм, используемый в процедуре люде! сйссй!лб лля пометки состояний структуры Кринке подформуламн, которые истинны в этом состоянии, могут быль использованы в этом случае тяк. При проверке выполнения формулы Ф в состояниях временного автомата А можно использовать граф регионов А, поскольку любая формула логики ТСП.
будет иметь одно и то же истинностнос значение для всех состоаний автомата А. принадлежащих одному и тому же состоянию графа регионов Й(А) автомата А. Поэтому граф регионов временного автомата А в алгоритме щобе! сйес(п1пй будет играть роль его структуры Кринке. Будем считать, что формула Ф логики ТСП„проверяемая на выполнение в состоаниях графа регионов Й(А), не содержит полформул, которые имеют временные ограничения,У . Для того чтобы проверить выполнение формулы Ф не только в начальном, но также и в любом другом состоянии графа регионов, необходимо лля каждого состоания з графе регионов А строить граф регионов Й(АЭг,э(я-О)), рассматривая состояние з графа регионов А с лсбавленным значением з = О как начальное госюяние этого графа.
Пример 12.16 ПРовеРим длЯ вРеменного авюыата Ат выполнение фоРмУлы ЕР„ДСя,п. Построим граф регионов автомата Ат (рис, 12г19, а). Проверим выполнение подформулы уз АСя!и= ЕР((ях1)л н) во всех состояниях графа регионов Й(Ат). В сосювнни Ос = (мг(х = О)) зтв формула проверена в предыдущем примере, она не выпслнвстсж Проверим ее выполнение в состоянии Оз =(гх(.с=О)) . Дпя этого вютронм граф регионов Й(А, Эя, 1з(зжб)) (рис. 12.19,61, со. стояния которого стличмотся от состояний графа регионов Й(Аг) добавлением значений "формульных" часов я. Для подформул формуяы — ер((г х!) л- и) построим щмдующие множества состояний, в которых эти подформулы выпслнмотся: У! =(Я э 1)' сги(У!)" (эс.
эг гз) гз "'л ' и(гз) (яя сы зе) Гласа 12 у)-я*л; л (л)-() А =~%' ~н(А) =( ) .6"-А' ~гг(Фси)=(гс-ггг) ннн ного г ч Р и л Посс регм р 12.1р.Грарр й(1 ) яП рр й(Лгая,рс( -О)) ченн Формула Д~ АС гп выполняется в начальном соонмннн графа регионов й(Аг Ю г, рг (к О)), смстраенного нз начального сосгоянна оь гра4га регионов й(Аг), н, слеяовательно, Формула Ф=АС,п вмнолняенз в состоа- Сисяммы ' ввв гз ч чэ чу х Ряс. 1ь26.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
