LectLog22 (1158012)
Текст из файла
Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 22.Задача верификации моделейпрограмм.Подформулы Фишера-Ладнера.Табличный метод верификациимоделей программ.Алгоритм верификации моделейпрограмм.ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММЗадача model checking для PLTLДля заданной формулы PLTL ϕ и конечной LTS M проверить M |= ϕ.Почему задача model checking непроста? Потому чтоIвыполнимость формул PLTL проверяется на бесконечныхинтерпретациях,IВ LTS M имеется бесконечно много интерпретаций (трасс).Почему задача model checking имеет эффективное решение?Потому чтоIвсе это бесконечное множество бесконечных интерпретаций«упаковано» в конечную структуру — LTS M.ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММЗамысел табличного метода1. Вместо проверки выполнимости ϕ во всех интерпретацияхлучше заняться поиском контрмодели — интерпретации I ,в которой не выполняется ϕ.2.
Выполнимость всякой формулы ψ полностью определяетсявыполнимостью ее подформул. Поэтому (не)выполнимостьформул можно проверять индуктивно.3. (Не)выполнимость формулы на одной из трасс LTS M,начинающейся в состоянии s, — это свойство состояния s.Значит, проверяя (не)выполнимость всех подформулформулы ϕ для всех состояний LTS M, можно вычислитьмножество S ϕ всех тех состояний, в которых невыполняется формула ϕ.
Если S0 ∩ S ϕ 6= ∅, то M 6|= ϕ.ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММВспомогательные определения и обозначенияДля заданной LTS M = hAP, S, S0 , −→, ρi, трассыtr = si0 , si1 , . . . , sin , sin+1 , . . . в LTS M и формулы PLTL ϕ будемиспользовать записьItr |= ϕ для обозначения отношения выполнимостиI (tr ), 0 |= ϕ;Itr [j] для обозначения j-го состояния sij в трассе tr ;Itr |j для обозначения трассы tr 0 = sij , sij+1 , . .
. , являющейсясуффиксом трассы tr , начинающейся состоянием sij .ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММУтверждение 1.Для любой LTS M и формула PLTL ϕ верноM 6|= ϕ⇐⇒существует такая начальная трасса tr , tr ∈ Tr0 (M),для которой tr 6|= ϕ.Доказательство.Самостоятельно.Таким образом, вместо задачи M |= ϕ мы будем рассматриватьдругую задачу:найти в LTS M начальную трассу tr , для которой tr 6|= ϕ.Если такой трассы найти не удастся, то верно M |= ϕ.ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММПриведение формулы к позитивной формеПрименяя равносильные преобразования, упростим формулу ϕ.Этап 1.
Удаление импликации → и темпоральных операторовG, F на основании законов взаимной зависимости|= ψ → ψ ≡ ¬ψ ∨ χ;|= Fψ ≡ true Uψ;|= Gψ ≡ false Rψ.Этап 2. Продвижение ¬ вглубь формулы на основании законовдвойственности|= ¬(ψ&χ) ≡ ¬ψ ∨ ¬χ;|= ¬(ψ ∨ χ) ≡ ¬ψ&¬χ;|= ¬¬ψ ≡ ψ;|= ¬Xψ ≡ X¬ψ;|= ¬(ψUχ) ≡ ¬ψR¬χ;|= ¬(ψRχ) ≡ ¬ψU¬χ.ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММУтверждение 2.В результате применения равносильных преобразований этапов1 и 2 любая формула PLTL ϕ приводится к равносильнойформуле ϕ0 , представленной в позитивной форме, в которойIиспользуются только логические связки ∨, &, ¬ итемпоральные операторы X, F, G,Iсвязка ¬ применяется только к атомарным высказываниямp, p ∈ AP.Доказательство.Самостоятельно.ЗАДАЧА ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММПриведение формулы к позитивной формеПример.ϕ = G(free & Xbusy → XF(pr1 ∨ pr2 )).Этап 1.ϕ0 = false R (¬(free & Xbusy ) ∨ X(true U(pr1 ∨ pr2 ))).Этап 2.ϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ПОДФОРМУЛЫ ФИШЕРА–ЛАДНЕРАПусть ϕ1 — формула PLTL в позитивной форме.
Тогдамножеством подформул Фишера–Ладнера называетсянаименьшее множество формул PLTL FLSubϕ1 , содержащееформулу ϕ1 и удовлетворяющее следующим условиям:Iесли p ∈ FLSubϕ1 и p ∈ AP, то ¬p ∈ FLSubϕ1 ,Iесли ψ&χ ∈ FLSubϕ1 , то {ψ, χ} ⊆ FLSubϕ1 ,Iесли ψ ∨ χ ∈ FLSubϕ1 , то {ψ, χ} ⊆ FLSubϕ1 ,Iесли ¬ψ ∈ FLSubϕ1 , то ψ ∈ FLSubϕ1 ,Iесли Xψ ∈ FLSubϕ1 , то ψ ∈ FLSubϕ1 ,Iесли ψUχ ∈ FLSubϕ1 , то {ψ, χ, X(ψUχ)} ⊆ FLSubϕ1 ,Iесли ψRχ ∈ FLSubϕ1 , то {ψ, χ, X(ψRχ)} ⊆ FLSubϕ1 .Утверждение 3.Если ϕ1 содержит n логических связок и темпоральныхоператоров, то |FLSubϕ1 | ≤ 3n.ПОДФОРМУЛЫ ФИШЕРА–ЛАДНЕРАПример.Пустьϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ТогдаFLSubϕ1= {ϕ1 ,false, Xϕ1 , ¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 )),¬free, X¬busy , X(true U(pr1 ∨ pr2 )),free, ¬busy , true U(pr1 ∨ pr2 ),busy , true, pr1 ∨ pr2 ,pr1 , pr2 , ¬pr1 , ¬pr2 }.ПОДФОРМУЛЫ ФИШЕРА–ЛАДНЕРАNext-подформулыПусть ϕ1 — формула PLTL в позитивной форме и FLSubϕ1 —множеством подформул Фишера–Ладнера формулы ϕ1 .Тогда запись XSubϕ1 будет обозначать множество всех техподформул Фишера–Ладнера, которые начинаются операторомX (neXttime), т.
е.XSubϕ1 = {ψ : ψ = Xχ, ψ ∈ FLSubϕ1 }.Пример.Пустьϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ТогдаXSubϕ1= {Xϕ1 , X¬busy ,X(true U(pr1 ∨ pr2 ))}.ПОДФОРМУЛЫ ФИШЕРА–ЛАДНЕРА(Until-Release)-подформулыПусть ϕ1 — формула PLTL в позитивной форме и FLSubϕ1 —множеством подформул Фишера–Ладнера формулы ϕ1 .Тогда запись URSubϕ1 будет обозначать множество всех техподформул Фишера–Ладнера, которые начинаются операторомU (Until) или R (Release), т. е.USubϕ1= {ψ : ψ = χ1 Uχ2 , ψ ∈ FLSubϕ1 }∪{ψ : ψ = χ1 Rχ2 , ψ ∈ FLSubϕ1 }.Пример.Пустьϕ1 = false R (¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 ))).ТогдаUSubϕ1= {ϕ1 , true U(pr1 ∨ pr2 )}.ПОДФОРМУЛЫ ФИШЕРА–ЛАДНЕРАСогласованные множества подформулПусть ϕ1 — формула PLTL в позитивной форме, и FLSubϕ1 —множество подформул Фишера–Ладнера для ϕ1 .Тогда согласованным множеством подформул формулы ϕ1называется всякое подмножество B, B ⊆ FLSubϕ1 ,удовлетворяющее следующим условиям:1.
true ∈ B, false ∈/ B,2. для любого атомарного высказыванияp, p ∈ AP ∩ FLSubϕ1 , выполняется в точности одно издвух включений: либо p ∈ B, либо ¬p ∈ B;3. ψ ∨ χ ∈ B ⇐⇒ ψ ∈ B или χ ∈ B,4. ψ&χ ∈ B ⇐⇒ ψ ∈ B и χ ∈ B,5. ψUχ ∈ B ⇐⇒ χ ∈ B или {ψ, X(ψUχ)} ⊆ B,6. ψRχ ∈ B ⇐⇒ χ ∈ B и при этом χ ∈ B или X(ψRχ) ∈ B.ПОДФОРМУЛЫ ФИШЕРА–ЛАДНЕРАСогласованные множества подформулСогласованные множества подформул — это максимальныемножества формул, которые не содержат «явных»противоречий, т. е. таких противоречий, которые можнообнаружить в текущий момент времени.Например, множество, состоящее из двух формулXpX¬p— завтра я пойду на лекцию,— завтра я не пойду на лекцию,может быть согласованным (хотя и противоречивым),поскольку сегодня возможное противоречие, содержащееся вэтих высказываниях, не проявляется.Согласованное множество подформул является аналогомсемантической таблицы — оно выражает наше пожеланиесделать все утверждения, содержащиеся в этом множестве,истинными, а все утверждения, не содержащиеся в нем, —ложными.ПОДФОРМУЛЫ ФИШЕРА–ЛАДНЕРАСогласованные множества подформулПример.ПустьFLSubϕ1= {free, busy , pr1 , pr2 , ¬free, ¬busy , ¬pr1 , ¬pr2 ,pr1 ∨ pr2 ,true U(pr1 ∨ pr2 ),X¬busy , X(true U(pr1 ∨ pr2 )),¬free ∨ X¬busy ∨ X(true U(pr1 ∨ pr2 )),ϕ1 , Xϕ1 }.Тогда одним из согласованных множеств подформул формулыϕ1 является множествоB = {true, pr1 , ¬pr2 , ¬free, busy , X¬busy ,true U(pr1 ∨ pr2 ), X(true U(pr1 ∨ pr2 )), ϕ1 }.ПОДФОРМУЛЫ ФИШЕРА–ЛАДНЕРАУтверждение 4.Пусть I — произвольная темпоральная интерпретация, и ϕ1 —произвольная формула в позитивной форме.Тогда для любого момента времени n множество формулBn = {ψ : ψ ∈ FLSubϕ1 и I , n |= ψ}является согласованным.Доказательство.Самостоятельно.
Непосредственно из определениясогласованного множества.А верно ли обратное утверждение: каждое согласованноемножество формул выполнимо в некоторой интерпретации вначальный момент времени?ПОДФОРМУЛЫ ФИШЕРА–ЛАДНЕРАУтверждение 5.Пусть ϕ1 — формула PLTL в позитивной форме. Тогда1. для любой пары B 0 ⊆ AP ∩ FLSubϕ1 , B 00 ⊆ XSubϕ1 ,существует такое согласованное множество подформул B,для которого верно B ∩ AP = B 0 , B ∩ XSubϕ1 = B 00 ;2.
для любой пары B1 и B2 согласованных множествподформул Фишера-Ладнера ϕ1 верны соотношенияB1 = B2 ⇐⇒ B1 ∩ AP = B2 ∩ AP иB1 ∩ XSubϕ1 = B1 ∩ XSubϕ1 .Доказательство.Самостоятельно.Утверждение 6.Если ϕ1 содержит n логических связок и темпоральныхоператоров, то число различных согласованных множествподформул Фишера-Ладнера не превосходит величины 23n .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИМОДЕЛЕЙ ПРОГРАММПусть задана формулы PLTL ϕ и конечная LTSM = hAP, S, S0 , −→, ρi.Нужно проверить выполнимость M |= ϕ.Для этого1.
формула ϕ приводится к позитивной форме ϕ1 ,2. для формулы ϕ1 строятсяIIIIмножество подформул Фишера–Ладнера FLSubϕ1 ,множество Next-подформул XSubϕ1 ,множество U-подформул FLSubϕ1 ,совокупность Conϕ1 всех возможных согласованныхмножеств подформул Фишера–Ладнера.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИМОДЕЛЕЙ ПРОГРАММСистемой Хинтикки для формулы PLTL ϕ1 и LTS Mназывается раскрашенный ориентированный графGϕ1 ,M = (V , E ) с множеством вершин V и множеством дуг E ,которые устроены так:V = {(s, B) : s ∈ S, B ∈ Conϕ1 , ρ(s) = B ∩ AP},т.
е. вершинами графа являются всевозможные пары(состояние s, согласованное множество B),для которых разметка ρ(s) состояния s подтверждаетистинность всех атомарных высказываний множества B;E= {h(s 0 , B 0 ), (s 00 , B 00 )i : s 0 −→ s 00и для любой Next-подформулы Xψ, Xψ ∈ XSubϕ1 ,верно Xψ ∈ B 0 ⇐⇒ ψ ∈ B 00 },т. е. дугами графа являются все такие переходы LTS M,которые позволяют подтвердить все обещания Xψ выполнитьψ в следующий момент времени.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИТеперь проведем раскраску вершин графа Γϕ1 ,M = (V , E ).Рассмотрим множество (Until-Release)-подформулURSubϕ1 = {χ01 Uχ001 , . . .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
