LectLog22 (Старые лекции, в целом тоже самое)

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 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 , . . .