Лекция 7. Верификация LTL. Автоматы Бюхи (1185507), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

для любого атомарного высказывания a верно: a ∈ H ⇔a ∈ L(s) (согласованность с атомарными высказываниямиL(s), или согласованность с состоянием s)2. внутренняя согласованность: для любых формулψ1 & ψ2 , χ1 Uχ2 ∈ [ϕ]FL верно:IIψ1 & ψ2 ∈ H ⇔ ψ1 , ψ2 ∈ Hχ1 Uχ2 ∈ H ⇔ χ2 ∈ H или {χ1 , X(χ1 Uχ2 )} ⊆ HНе противоречащие друг другу предположения H1 , H2 насегодня и завтра внешне согласованы: для любой формулыXψ ∈ [ϕ]FL верно:Xψ ∈ H1 ⇔ ψ ∈ H2При разметке состояний модели Крипке предположениямиI выбираются всевозможные предположения, согласованныевнутренне и с размечаемым состояниемI дуги проводятся для всевозможных пар внешнесогласованных предположенийТабличный алгоритм model checking для LTLТабличный алгоритм model checking для LTL можно считатьполностью описаннымОбоснование корректности этого алгоритма непросто дляпонимания и приведено в лекциях по курсу“Математическая логика и логическоепрограммирование”Достоинства табличного алгоритма:...Недостатки табличного алгоритма:Iтруден для пониманияIтребуется явный обход графа, полученного из моделиКрипке разметкой состояний предположениями(а можно ли этого избежать?)Iсостояния могут размечаться большими множествамиформул (а насколько большими?)Алгоритмы model checkingЗадача model checking для CTL имеет альтернативутабличному алгоритму: символьный алгоритмЗадача model checking для LTL также имеет альтернативутабличному алгоритму: автоматный алгоритмЕсли программное средство производит верификацию дляCTL, то скорее всего в основе реализованного алгоритмаверификации лежит символьный алгоритмЕсли программное средство производит верификацию для LTL,то скорее всего в основе реализованного алгоритмаверификации лежит автоматный алгоритмАвтоматный алгоритм model checking для LTLОбщая схема работы автоматного алгоритма:Iимеются модель Крипке M и LTL-формула ϕIпостроить автомат AM , описывающий в точностимножество всех трасс модели MIпостроить автомат A¬ϕ , описывающий в точностимножество всех трасс, не входящих в свойство ϕIпостроить автомат AM ⊕ A¬ϕ , описывающий в точностимножество всех трасс модели M, не обладающихсвойством ϕпроверить, описывается ли автоматом AM ⊕ A¬ϕ пустоемножество трассIIIесли да, то M |= ϕесли нет, то M 6|= ϕИ что же это за автоматы?Автоматы БюхиАвтомат Бюхи над алфавитом Σ — это системаA = (S, S0 , δ, F ), гдеIS — конечное множество состоянийIS0 ⊆ S — множество начальных состоянийIδ ⊆ S × Σ × S — отношение переходовIF ⊆ S — множество заключительных состоянийσ1 ,...,σks −−−−−→s 0 — синоним записи δ(s, σ1 , s 0 ) & .

. . & δ(s, σk , s 0 )Автоматы БюхиПримерaba, ba, ba— начальное состояние— заключительное состояниеНичего не напоминает?Синтаксис автоматов Бюхи в точности совпадает с синтаксисомконечных недетерминированных автоматов-распознавателейАвтомат Бюхи, прочитывая конечные слова, изменяет своисостояния точно так же, как и автоматы распознавателиОтличие этих двух моделей — в семантике: распознаваемомязыке (множестве слов)Автоматы БюхиАвтоматы Бюхи строятся для того, чтобы проверять, содержитли модель Крипке трассы, не удовлетворяющие заданномусвойствуИ трассы, и свойства основаны на бесконечных словахЯзык, распознаваемый автоматом Бюхи, — это множествобесконечных слов в заданном алфавитеМножество всех бесконечных слов в алфавите Σ будемобозначать так: ΣωТрасса автомата Бюхи A = (S, S0 , δ, F ), порождаемаябесконечным словом σ1 σ2 σ3 .

. . — это любая бесконечнаяпоследовательность его состояний видаσ1σ2σ3s1 −→s2 −→...,s0 −→такая что s0 ∈ S0Tr (A, w ) — множество всех трасс автомата Бюхи A,порождаемых бесконечным словом wАвтоматы Бюхиinf(t) — множество состояний, встречающихся бесконечночасто в трассе t автомата БюхиЯзык L(A), распознаваемый автоматом Бюхи A = (S, S0 , δ, F ),определяется так:L(A) = {w | ∃t ∈ Tr (A, w ) : inf (t) ∩ F 6= ∅}Проще говоря, бесконечное слово w распознаётся автоматомБюхи, если среди всех трасс автомата, получаемых припрочитывании этого слова, есть такая, в которой бесконечночасто повторяется хотя бы одно заключительное состояниеАвтоматы БюхиПримерaba, ba, baКакой язык распознаётся этим автоматом Бюхи?Этот язык состоит в точности из всех бесконечных словследующего вида:I(ab)ω — слово, получающееся бесконечным повторениемслова abI(ab)+ (a|b)ω — слово, состоящее из хотя бы одногоповторения слова ab, за которым следует любоебесконечное сочетание букв a, bАвтоматы БюхиА как построить автомат Бюхи, распознающий в точностимножество всех трасс заданной модели Крипке?Очень просто:Iалфавит, над которым строится автомат: 2APIобъявим состояния модели состояниями автомата БюхиIначальные состояния модели объявим начальнымисостояниями автоматаIсоединим состояния автомата дугами так же, как онибыли соединены в моделиIмножество высказываний, помечавшее состояние модели,переместим на каждую исходящую из состояния дугу вавтоматеIобъявим все состояния автомата заключительнымиАвтоматы БюхиПримерpqpppАвтомат, распознающий в точности множество всех трасс этоймодели Крипке, может выглядеть так:{p}{p}{q}{p}{p}{p}{q}Автоматы БюхиА как построить автомат Бюхи, распознающий в точностимножество Tr (ϕ) для LTL-формулы ϕ?Начнём с примеровGFaS :a∈SS :a∈SS :a∈/SS :a∈/SАвтоматы БюхиА как построить автомат Бюхи, распознающий в точностимножество Tr (ϕ) для LTL-формулы ϕ?Начнём с примеровFGaS : anyS :a∈SS :a∈SАвтоматы БюхиА как построить автомат Бюхи, распознающий в точностимножество Tr (ϕ) для LTL-формулы ϕ?Начнём с примеровG(a → Fb)S : a ∈ S, b ∈/SS :b∈SS :a∈/SS :b∈/SS :b∈SА как построить такой автомат Бюхи для LTL-формулы произвольного вида?Построение автомата Бюхи по LTL-формулеОбщая схема построения автомата Бюхи поLTL-формуле:LTL-формула ϕОбобщённый автомат Бюхи GAϕАвтомат Бюхи AϕОбобщённые автоматы БюхиОбобщённый автомат Бюхи над алфавитом Σ — это системаGA = (S, S0 , δ, F), гдеIS — конечное множество состоянийIS0 ⊆ S — множество начальных состоянийIδ ⊆ S × Σ × S — отношение переходовIF ⊆ 2S — семейство множеств заключительных состоянийОтличие от необобщённого автомата Бюхи только в том, какиеслова распознаются таким автоматомБесконечное слово w распознаётся обобщённым автоматомБюхи GA, если среди трасс, порождаемых словом w ,существует трасса t, такая что inf (t) ∩ F 6= ∅ для любогомножества F из семейства FОбобщённые автоматы БюхиУтверждениеДля любого обобщённого автомата Бюхи существуетнеобобщённый автомат Бюхи, распознающий тот жеязыкДоказательство.Рассмотрим произвольный обобщённый автомат БюхиGA = (S, S0 , δ, {F0 , .

. . , Fk−1 })Требуемый автомат Бюхи A = (S 0 , S00 , δ, F ) имеет следующееустройство:IS 0 = S × {0, . . . , k − 1}IS00 = S0 × {0}IF = {Fi × {i} | 0 ≤ i < k}Iδ 0 ((s, i), σ, (s 0 , i)) ⇔ δ(s, σ, s 0 ) и s ∈/ FiIδ 0 ((s, i), σ, (s 0 , i + 1(mod k))) ⇔ δ(s, σ, s 0 ) и s ∈ FiHПостроение автомата Бюхи по LTL-формулеИ как же построить обобщённый автомат Бюхи, распознающийсвойство ϕ?Например, такой обобщённый автомат Бюхи A = (S, S0 , δ, F)распознаёт свойство ϕ:I S — это всевозможные внутренне согласованныепредположения, построенные на основе замыканияФишера-Ладнера формулы ϕI S0 — это всевозможные предположения H, такие чтоϕ∈HI Каждой формуле ψUχ ∈ [ϕ]FL соответствует множествозаключительных состояний FψUχ , состоящее в точности изтех предположений H, для которых звенит звонок дляформулы ψUχ:IIIψ ∈ H илиX(ϕUψ) ∈ Hδ(H1 , L, H2 ) ⇔IIH1 и H2 — внешне согласованные предположенияпредположение H1 согласовано с атомарнымивысказываниями LАвтоматный алгоритм model checking для LTLПромежуточный итогДля заданных модели Крипке M и LTL-формулы ϕ требуетсяпроверить соотношениеM |= ϕЧто для этого уже сделано:Iдля модели M построен автомат Бюхи AM , такой чтоL(A) = Tr (M)Iдля формулы ¬ϕ построен автомат Бюхи A¬ϕ , такой чтоL(A¬ϕ ) = Tr (¬ϕ)Что осталось сделать:Iпостроить автомат AM ⊕ A¬ϕ , распознающий языкL(AM ) ∩ L(A¬ϕ )Iпроверить, имея описание автомата, пуст ли этот языкПересечение автоматов БюхиУтверждениеДля любой пары автоматов Бюхи A1 , A2 существуетавтомат Бюхи A, распознающий язык L(A1 ) ∩ L(A2 )Доказательство.Рассмотрим произвольные автоматы Бюхи A1 = (S1 , S01 , δ1 , F1 ),A2 = (S2 , S02 , δ2 , F2 )Достаточно построить обобщённый автомат Бюхи,распознающий язык L(A1 ) ∩ L(A2 )Требуемый обобщённый автомат Бюхи GA имеет следующееустройство:GA = (S1 × S2 , S01 × S02 , δ, {F1 × S2 , S1 × F2 }), гдеδ((s1 , s2 ), σ, (s10 , s20 )) ⇔ δ1 (s1 , s10 ) и δ2 (s2 , s20 )HПроверка пустоты автомата БюхиУтверждениеЯзык L(A), распознаваемый автоматом Бюхи A, пусттогда и только тогда, когда существует заключительноесостояние автомата A, принадлежащее какому-либоциклу, достижимому из какого-либо начальногосостояния этого автоматаДоказательство.Очевидно?Примерaba, ba, baЯзык, распознаваемый этим автоматом, непустПроверка пустоты автомата БюхиУтверждениеЯзык L(A), распознаваемый автоматом Бюхи A, пусттогда и только тогда, когда существует заключительноесостояние автомата A, принадлежащее какому-либоциклу, достижимому из какого-либо начальногосостояния этого автоматаДоказательство.Очевидно?Примерaba, baЯзык, распознаваемый этим автоматом, пустСведение задачи model checking для LTL кпроблеме пустоты для автоматов БюхиИтогПусть M — произвольная модель Крипкеи ϕ — произвольная LTL-формулаТогдаM |= ϕ⇔L(AM ⊕ A¬ϕ ) = ∅Конец лекции 7.

Характеристики

Список файлов лекций