2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 17
Текст из файла (страница 17)
формулы путей ф;.-Ф] р] р р]Хр]и()р Некоторые формулы относатсв к обоим юнюсам. Например, формула А(а() Ь) является кшс формулой ЕТ1., твк и формулой СП.. Формула АС(р=> Уа) яшшетсв формулой 1.Т1„она не является формулой СТ1.. Формула АО(у~ЕРр) -является формулой СТ1., оиа не является формулой (.Т1.. Вес зтн формулы лыщются формулами логики СТ1,». Формулы логики СП.» интерпретирукзюл на вычислениях структуры Кринке, которые можно прелсшвнть бесконечным деревом (рис. 2.12, в).
Логика С'П.» более мощная, чем и логика ЬП„и логика СТ1 Формулы СТ1.' могут различать не только вычисления (линейные пути поведений систем), но н разветвления, деревья поведений. Летят за диямя дии, и каждый час уносит Часюптку бытиц а мы с тобой вдвоем Лреднаеагаем жить, и глядь — какраз — умрем как и многие другие выскшывания естественного тыка, могут быль формализованы в рамках темпоральиой логики по-разному, хотя, масомненно, здсоь требуетсв использование именно логики вепищегоы времешь Одна из возможных формализаций такая; р~ = А(С»1(уе «ЮЕХИеагй) Эта формула логики СП.» (133] утверждает, что вдоль всех вычислений (А) с вечной жизнью (С!г)е ) всегда (С ) возможно (Е ) встретить смерть в слелующнй момент (Х г(еагй ).
Строфа Пушкина как рвз и говорит о возмоююсги в любой момент переключения нашего бытия на другую ветвь, на которой иао (к сшкалеиию) ожидает смерть. Структура Кринке, которая соответ.- ствует строкам Пушкина, представлена на рнс.224,а: в кшкдый момент (в каждом состоянян) перед нами альтернатива (которую обычно выбираем Хзмеа 2 Тее не мы!): нлн жпгь дальше, илн умереть. Особенно четко это показывает раз- вертка структуры Кринке, покязаннаа ив рис. 2.14, б. Формула рь, на этой струатуре Кринке выполняется. а 6 Рно 3.1* Структура Крюнн и ее развертка (варево еымюленнй) Пр Ко~ Пр ()у Рис.
3.1К Структура Крнгае (я) н ее дерево емеяеннй (б) Отметим, что на структуре Кринке (рис. 2.15) эта формула не выполняетсю ее разверни имеет вычисления бесконечной жизни, на которых нет ветвления на состояния, помеченные Ыеагй, Структуры Кринке, показанные на рис. 2.14 и 2.1 5, имеют одно и то же м полистно вычислений (рнс. 2.1 6), которое может быль выражено ю.регулярным вырюкеннем ~1(Те" и 1!ге+беляна~: одна бесконечная цепочка )Ре и множество цепочек с любым (ненулевым) конечным числом фе, за которыми слелует бесконечное число Иеагй. Следствием того, чго обе структуры Кринке имеют одно и то же множество линейных вычислений, являегсв то, что никакая формула ЬТЬ не может их различить. Этот пример, в частности, показывает, что логика СТ1.е более мошнмг, чем логика 1.Т1,: формулы СТЬе рвзличжот этн две струкгурм Кринке.
'лаев 2 Рнс. 2.16. Множество еычнсленнн стРуктуР Кряпке Рна 2. 14 н 2.15 вечным тся: ее пс. 2.14 : моямт ~ беско- :и того, вычнс'ь. Этот ~ логнка Прныпр 2.7 Комбинации кванторов лугой А н Е с темпоральнымн операторамн р н С вмтст достаточно очевндный смысл; П АСф — утверждение ф — инвариант (ф выполняется всегда, в любом состояннн); П ЕСф — погснцнально всегда ф (возможно, что ф будет выполнвться всв ерема); 0 АРф — когда-ннбудыр обвзательно выповннтся; 0 ЕР ф —. когда.нибудь, возмопщог ф выполннюя. Прнывр 22) Пусть р означает Я люблю Мтау", 4' означтт "ЯлюблюДтау", Тогдж П формула АС р является формулой СП„она формапнзует следующее высказывание: "Я люблю Мтиу, и, что бы ни сзучююсь, я буду любюнь ее есеа)а"; П формула АРС(рл ф) является формулой 1Т1„онв формялнзует следующее высказывание: "Что бы ни сауптось, в будущем л полюблю Машу навсегда, а Дашу ие буду любить.~', П формула Е(РААСУ )) — формула СТ(,„она формалнзует высказывание: "Я не нсюночаю такого раиюннв событнб (Е ), что я буду любюнь Мавау до тех пор (() ), пока, накопал я не начюблю Дтиу навечно ( АС )".
2.10. Сравнение логик ЕТ~ и СТ~ Для обеих логик, ВТС и СТ)„разработаны эффективные алгоритмы проверки вмпслннмостн их формул на структурах Кринке. Эти алгоритмы реаяизованы в нескольких системах верификации, как свободно распространяемых, так и используемых внутри компаний — производителей ПО и аппаратуры, и они использукпся в рамках корпоративных технологических циклов разработки систем. В следующих двух главах мы рассмотрим технмку верификации для кюкдой из этихдвух логик. Существует множество черт, которые отличают зти логики друг от прута, но главные различие необходимо подчеркнуть особо: С( Формулы этих двух логик характеризуют свойства разных типов: ° формулы 1ТС являются формулами пути; в логике Пг.
вообще нет кеаввюрое пути. При проверке выполнения свойств структуры Кринке единственный квантор луги А перед формулой ЕТЬ говорит, что этв формула доюкна выполняться на всех еохнолсиых пугхх этой структуры Крипке. Логика П г. более проста и интуитивна, более понятна, чем С"П.; ° формулы СТС являются формулами состояний; в логике СТС любой темпоральный оператор предварен квантором луги, который определяет, на всех (квантор А) нлн только на некоторых (кваигор Е) путях из текущего состояния сгрукгуры Кринке угвер|кдается истинность соответствующей темпоральной формулы пути. ьг Формулы обеих логик интерпретируются (т. е.
принимают истинное или ложное значение) на струкгурах Крипке, но: ° формулы логики ЬТ(, интерпретируются на всех вычислениях структуры Кринке, начинающихся в начальном состоянии. Они принимают истинное или ложное значение на каждом вычислении структуры Кринке. Формула (з ЕТ(. выполняется на структуре Кринке М, если (э выполнается на всех траекториях вычислений М (в вачальнан сосвюллии каждого бесконечного вычисления этой структуры). Вычисления эти бесконечны, и их бесконечное число. Этим определяются ббльшие трудности проверки выполнения формуяы П"ь. на структуре Кринке, чем проверка формул СТ( с ° формулы логики СТВ интерпретируются на деревьях вычислений структуры Кринке. Дерево вычислений — это развертка структуры Кринке с корнем в данном состоянии.
Любая формула СТЬ принимает истинное илн ложное значение в кюкдом состоянии структуры Кринке, Главе 2 «верки сваны , так и и они «ботки «и для та, но «е нет рипке ю этв «ук«у«, чем юбой деляях из аоот- или )'хт)'- «т нснпке. «псл- млии «эти ыпие «пке, ений «уры наст «пке, а таких состояний конечное числос Этим определястсв удимгюльювз эффективность алгоритма то«)е! сйеаЬЪб лля формул СТЬ. Формула «р СП. выполняется на структуре Кринке М, если «р выполняется на на-. чальном сосмаании структуры Кринке, в корне дерева вычислений А« . О Техника верификации для ЬТЬ ««СТЬ совершенно различив как по при«аеняемым аягоритмам, так и по их сложности: ° существуют инструменты верификации, которые реализуют алгоритмы Моде! сйес)««пб дяя ЬТЬ, например, Вр«п.
Слолоюсть алгоритмов верификации лннейна относительно числа состояний струюуры Кринке н зкспоненциальна относительно сложности «чисва подформул) формулы ЬТЬ, но поскольку проверяемые формулы ЬТЬ обычно малы, возмолою использование этих алгоритмов для верифиющии достаточно сложных систем; ° существуют другие инструменты, реализующие автор«пмы верифика-.. ции лля формул СТЬ„например, ЗМ«Г.
Сложность алгорнзмов верификации для СП. пропорциональна числу состояний структуры Кринке и сложности «чисчу подформул) формулы СТ).. 0 Многие свойства технических систем могут быть выражены квк формулами логики СП., так и формулами логики ЬТЬ. Например." ° "каасдое сооб«ленив ксгдач«нбудь е б)«)уи)ем будем ладрмерэп)ело".: СП.: АС(ген«э*э«Аргер) ЬТЬ; О(зел«)ю)«геп ) Однако яееерло угщрждение, чго если в формуле ЬТЬ юскдмй темпораэьный оператор будет предварен квантором пути А, то построен«ма так фбрмула СП. будет эквивалентна исходной формуле (см.
задачу 2.7). 0 Выразительнал моппюсть этик двух логик несравнима, т. е. некоторые свойспщ могут быль вырюкены в СП„но не могут быть выражены в ЬТ$ и наоборот ° например, формула АСК)г«р логики СТЬ„вырвжаихщщ "доел«мщ«ь мосюь сеойсмеа «э", не вырюима в ЬТЬ; ° например,. формула в С ч«логики ЬТ)., вырюкающая "см««биэинцню сеобсвма Э«каг«)а-инбу«)ь а буржуи«жн", не выразима в СП . 2.11. Темпоральные логики прошлого В философии, лингвистике и теории искусственного интеллекта анализ утверждений, зависящих от времени, обычно проводится как для будущего времени, так н дяя прошлого. В технике рассмотрение формул темпоральных лш'ик почти всегда связано с булущнм временем. Это обусловлено твм, что основное применение темпораяьиых логик в технике — анализ будущего поведения вновь создаваемых технических систем.
Однако в некоторых случаях н лдя технических систем удобно выражать темпоральные свойства нх прошлого поведения. В частности, причинные зависимости иногда легче транслировать в формулы темпоральных логик с модазьностями прошлого. Естественно для этого ввести так называемые "темпоральные операторы прошлого", например, Р" и Х ~. Формула Р ~чг понимается так: "когда-го в прошлом утверждение м было истинным" и эквиваяентна формуле Тепзе (язйю Рм, а формула Х м понимается так: "непосредственно в предыдущем состоянии угверлгдение Ш было истинным". Зеркальнмм отображением оператора () валяется оператор Б (млсе).
Темпорвльшш формула фйш понимается так; "формула у выполнилась когда-то в прошлом, и с тех пор выполняется формула ф". Иаюльзуя темпоральные операторы прошлого, свойство; "Пока ключ зажигалка ле вставлен, машина не поедем" наиболее естественно формавиювать так: АО(згаггизг кеюч ипкгмаигм еслшглен) —.всегда верно ( АО ), что если мешина стартовшш (згагг), то предварительно ( Р ' ) ключ зажигания был вставлен. В гх б мы увидим, что операторы прошлого не увеличивают экспрессивности темпоральной логики, и формулы с модельными операторнни прошлого для струатур Кринке можно выразить через операторы будущего, аведа дополнительные атомарные преднкаты.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
