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