2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 19
Текст из файла (страница 19)
К заяаче 2.9 2.9. Логика СТС н ЬТ1. несравнимы по своей вырзонтельной мощности. Существуют свойства поведеннй, которые могут быть выражены в одной из логик и не могут быль выражены в другой. Для того чтобы в этом убедиться, выполните следукннее. а) Докюкнте теорему: Существуют свойства поведеннй, выражаемые в СП. н не вырюкаемые в 1ТЕ.
Для этого дяя двух рвзверток структур Крнпкс (рнс. 2.! 7К 'г) поюмапе, по никакая формула 2.ТЬ не может разлнчнщ этн дае структуры (Указанаж рассмотрите возможные вычнсления н Аузй ()мвв 2 й) постройте формулу Ст(., которая истинна на одной нз структур Крнпке и ложна на другой. о уилзвппе Зта формула дающм отразить, что в М~ только одно следующее состояние с двумя альтернативами, а в Мз — два следуизщих состояния, кюкдое без альтернатив). б) Попробуйте выразить в логике С"П. свойства поведения, представлен. ные (.П,-формулами АСРр и А(Х рчХХг) 2.16. Выразите формулу А(рПЕ) логики СП. с помощью других формул этой логики. 2.11.
Пуси р означает "Я любав Можу", а р — "Я люблю Дзиу". Каким высказыванием соотастощукп слелующне формулы СП.: а) АРЕСр б) ЕРАСр в) А(р()е) г) Е((ЕХр)0(АС р)) 2.12. ДОКажИтЕ, ЧтО фОрчува С(рой)ез(СРруСРр) ОбщвэиаЧНМВ (т.Е. истинна на всех ее интерпретадияк). 2.13. Формаянзуйге утверждения в логике ).Т(;. а) "Я выйду замуж не менее двух раз" б) "Я выйду замуж не более двух раз" в) "Я выйду замуж точно дщ раза" г) "Я выйду замуж не менее одного резв" д) "Я выйду замуж не более одного рща" е) "Я выйду замуж точно одни раз" ж) "Я никогда не выйду замуж" в предположении, что говорящаз сейчас не замучи н никогда замужем не была. Используйте атомарный предикат р, обозначающий собмтие "Я еыяезьуиззрок . 2.14. Постройте структуру Кринке, на которой выполняется формула ЕСЕРр н не выполняется формула ЕСЩ>.
и совина, рмул г вы- (т. е. » не вы- ~ула 2.1$. Выразите в ЬТ~. сеойспю: "Мвмду квщдой парой соагояний, удоащтворяющих свойству р, обязательно встреппса состояние, удовлетвортощее свойству а ". 2.16. Дяя темпорвльиых логик СП. н СП.» определены подкввссы: логюэ АСТ)., АСТ1.», ЕС)Т, и ЕСП.». Формула СТЕ является формулой логика АСП., если у нее используегся только универсальный квантор пути А (т. е.
все пары: <ктлалар пути, тглггюральлый опгралюр> яввяючся парами АХ, АР, АО, А() ) и все отрицания применяются талька к атомарным преднкатам. Логика АСТ1, называется "улав»реаль»ай лагаяай СТй". Формула СП. является формулой логики ЕСП., если у нее используется только кввнтор существования пути Е и все отрицания применяются толью к атомарным предикатам. Логика АСП.
называется "зкзкстгицкальвай логикой СТй". Аналогично опрещпяются универсальная и экзистенциальная логики СТЬ». Какой — уннеерсвлыюй илн зюистенцнальной — логике СП. (илн СТ$Р) принаалткат формулы: а) АХрюА(йЮ г) б) Аура»А (йОг) в) ЕХрю(аЕ г) г) ЕОрчЕР(йлЕ( р()г)) 2.17. Кроме темпоральных операторов Р н С, которые определяю»та через оператор 6, иногда улобно примеюпь оператор К, который назывветая "олераторан разбаокаровха" (ю!сам) с двумя аргументами.
Оператор ц,йфз имеет следующую сеыыпику: он утверждает, что свойство рз выполняется на всем пути вплоть до того состояния, в котором истинно ем хотя р~ манат и не выпслниться на пути никогда. Оператор К является двойсщенным операюру 1): 9Фрзн ( ФР рз). Определите формальную семантику оператора разблокировки К. 2.18.
Доктките нли опровергните: а) (рр)Ю(рй) и р(равд) б) О(р юХр) ж Ори»СХр в) О(рпьХр)иб рчйбр гРЕСЕЕ р и РХЕС р л) рс)~~(риац) у)е 34%. Псстройге несколько вычислений, на конГсык фо(нгулы С(Лерсел ~ СПерсил) ' букет истинной. гМ.П рй ору у) Ер ~,иа о Раы формулы: а) АЕЕХр б) ЕЕАХРЛАЕЕхе в) ЕР(р лАРу) г) ЕХЕСр л) АРСр е) АСРрлЕРСР ;расее а главд 3 ющие Алгоритм тоде! слесИля для СТ1 В этой главе рассматривается алгоритм проверки моделей лля одного из пгщклассов темпоральиых логик — логики СТ(. (Союриюбспа! Тще (.ойю). Формулы этой логики позволяют выразить досщзочио сложиые свойспщ поаедеиия реагирующих систем.
Алгоритм проверки выполиимости формулы СП. иа модели реегирующмх систем — структуре Крипке — удивигельио прост и эффективен. ЗЛ. Темпоральная логика ветвящегося времени СТЕ Рис. К1 уточняет рис. 1.1, представляя схему верификации иа основе меюда лязге( сйесаля. В качестве формальной модели системы для верификации используетса структура Крипке, а формвеьиая спецификация требоваиий ъь лается формулой темпоральиой логики В общей темпоральиой логике ветващегося времени СТ(.е возможиы любые комбинации кввиторов пути ( А и Е ) и темпоральиых операторов ( Х и () ).
Темпоральиые операторы Р и С (как и кваигор всеобщиости) являются выводимыми в этой логике. Логика еемеящегося времени СП (Союропцюпа1 Тгее (ой1с) явлаетсв ограничением СП.': в формулах СТК юскдый темпо. ральиый оператор дояжеи быль предаареи кваитором пути. Иными словами, в формулах СП. эти модельжкти могут появиться только парами: АР, ЕСэ, А() ит.д. Формулы логики СП.
иитерпретнруютеа иа миожестве струкгур Крипке.т. е. модели вычислений с конечным числом состояиий и возможиыми вльтериатиаами. Тем самым ьюиелирусюа аозможиость "разветвлеиия" времени: Глвю З в каждом своем состовнмн ьюдель Кринке предоставляет несколько вариантов дальнейшего резанию вычислений, и формула СП. позволяет специфицировать свойспю поведения на различных ветвях дерева вычислений. Именно поз гому логика СТЕ названа логикой ееямящегосл времеви. Грамматика формул СП.
включает все 8 возможных пар: грз р1-юр!рчр)Е%р!ЕРр~ЕСцг)Е(р()р))Акр(АВр~АСер~А(р))р) Прн написании формул, квк обычно, макно использовпь скобки длв выделе. ния порядка выполнения операторов. Рнс ЕЕ Схема лроцеесв верифювцни ив основе алгоритма проверки модели (аюгыг снссдвй) 3.2. Семантика СТ1 на деревьях вычислений Все формулы СП, — зто формулы состояний, т. е. любая формула СП. в каждом состоянии струкгуры Кринке имеет конкретное истннностиое значение: она либо истинна, либо ложна.
Любая формула СП. на данной струкгуре Кринке М либо выполняется (если она истинна в начальном состоянии М ), либо не выполнвется (если она лшкна в начальном состоянии М ). еев 3 )иан- ифи:ний. чне: 7ре М), Повторим неформальное опредааенап щпх формул.
На двиной структуре Кринке: (у АХр выполняется в состоянии з, если формуяа р вмпоянявюл во всех состояниях, непосредственно следующихза з; О ЕХв выполнщтся в состоянии з, если формула и выполняется хотя бы в одном состоянии, непосредственно следукипем эа з; (2 АРф (неизбежно р) выполняеюя в состоянии з, если на всех пупа, начинающихся из состояния з. формула р когла-нибудь выполннтся; (2 Еув (возможно р) выполнястса в состоянии з, если нз этого состояния существует путь, на котором формула р когда-нибудь вьпюлнитсз; О АС р (глобально р) выполняется в состоянии з, если на всех путях, начинающихся из сосгозиия г, во всех состояниях этих путей формула р выполняется; О ЕПр выполняется в состоянии з, если существует путь из з, во вюх состояниях которого формула <р выполнзеюя; О А(р,Прз) выполняется в состоянии з, если на всех пугкц начинмощихся в з, когда-нибудь в будущем выполнима формула рз, ало этого во всек состояниях этих путей выполняется формула р,; 0 е(гэ,паз) выполняется в состоянии з, если нз з существует пуп, на котором когда-нибудь в будущем вьнюлннтся вз, а до этого во всех состояниях этого пугп выполняется (з~ .
Визуально эту семантику удобно предспвнть деревом вычислений с корнем е текущем соспмнии. На рис. 2.2 нюбрамены такие деревья, в кормы каторых истинны указаннме формулы. Визуальное представление семантики позваист поищь рекурсивное вырввмнне для формул СТ(.: а Аур = р АХ АР р на всех пущх нз текущего состояния формуяа р когда-нибудь выполнится — это то же самое, что или ф выполнщтся 'в текущем соспнвни, ющ же формула Аур выполнлстсз во всех слелующих состояниях; 0 Еур=рчЕХЕРр на каком-нибудь пути из текущего соспмниа когда-нибудь выполннтся формула р — зто то мв самос, что илп и щпюлнястся в текущем состоя- гласа з л нии, илн сущяствует Явкой пув, что формуле игр аыполнится в слелующем его состоянии; Гу Агягр=грлАХАСО ВО Всех ссстОяннях нВ Всех путна ия твкунгегс ссстгыния Выполняется формула Π— это то яге самое, сто ~р выпояняегся в текущем состоянии, и ВО Всех слелуюигих ссстояннях Всех путей, нечинегсщихся В текуогем состоянии, выполняется формула Абяг; Гл ЕОр=плЕХЕСО существует путь ня текущего состоаюы, во всех состгыииях которого о выполняется — это то же самое, что ~р выполняется в текущем состоянии |яетса ени, и н'о о евнин рве.
дд, Š— з. Визуальное предсмвяеине семантики формул СП. и из этого состоящм сущесщувг такой путь, в еледувщем состоянии которого формула ЕС ф выполщвтся; 0 А(е~б~рз) =фа т(В~ ьАХ А(В~6<рз)) на всех путях иэ текущего состояния когзаьнибудь выпслнитса оз, а до этого во всех состояниях выполняется В, — это то ме самое, кто или фз выполняезся в текущем состоанни, нлн ме в текупмм состоянии вмполняетса е~, а во есек следукнпих соскмниях всех пуща, идущих из текущего соспмння, выполнлегсл формула А(и~без); Глава З О Е(ф,Пр,)=рз (р,оЕХЕ(аьср,)) нз текущего состояния существует путь, на котором когда-нибудь выпалнится <рз, а до этого во всех состояниях этого пути выпслнаегся р, — это то же самое, по или рз выполняется в текущем состоянии, нлн же в текущем состоянии выполнястщ ~р, н нз него существует пуп„в следующем соспжнии которого формула Е(р~Прз ) выполняется.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
