7 Табличная верификация моделей для LTL. Автоматы Бюхи - их свойства и обобщения. Трансляция формул PLTL в автоматы Бюхи (1185959), страница 2

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

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

. . , δ(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 распознаётся автоматомБюхи, если среди всех трасс автомата, получаемых припрочитывании этого слова, есть такая, в которой бесконечночасто повторяется хотя бы одно заключительное состояниеАвтоматы БюхиПримерabccaЯзык, распознаваемый этим автоматом Бюхи, состоит вточности из всех бесконечных слов следующего вида:I(ab)ω — слово, получающееся бесконечным повторениемслова abI(ab)+ c ω — слово, начинающееся с конечного ненолевогочисла повторений ab, после которого бесконечноповторяется буква cАвтоматы Бюхи и модели КрипкеКак по модели Крипке M построить автомат Бюхи,распознающий язык Tr (M)?Очень просто:Iалфавит, над которым строится автомат: 2APIобъявим состояния модели состояниями автомата БюхиIначальные состояния модели объявим начальнымисостояниями автоматаIсоединим состояния автомата дугами так же, как онибыли соединены в моделиIмножество высказываний, помечавшее состояние модели,переместим на каждую исходящую из состояния дугу вавтоматеIобъявим все состояния автомата заключительнымиАвтоматы Бюхи и модели КрипкеПримерpqpppАвтомат, распознающий в точности множество всех трасс этоймодели Крипке, может выглядеть так:{p}{p}{q}{p}{p}{p}{q}Автоматы Бюхи и LTL-формулыКак по LTL-формуле ϕ построить автомат Бюхи,распознающий множество Tr (ϕ)?Начнём с примеровS :a∈SS :a∈SS :a∈/SS :a∈/SЭтот автомат распознаёт множество Tr (GFa)Автоматы Бюхи и LTL-формулыКак по LTL-формуле ϕ построить автомат Бюхи,распознающий множество Tr (ϕ)?Начнём с примеровS : anyS :a∈SS :a∈SЭтот автомат распознаёт множество Tr (FGa)Автоматы Бюхи и LTL-формулыКак по LTL-формуле ϕ построить автомат Бюхи,распознающий множество Tr (ϕ)?Начнём с примеровS : a ∈ S, b ∈/SS :b∈SS :a∈/SS :b∈/SS :b∈SЭтот автомат распознаёт множество Tr (G(a → Fb))А как построить такой автомат Бюхидля произвольной 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-формулыКак по LTL-формуле ϕ построить обобщённый автомат Бюхи,распознающий множество Tr (ϕ)?Например, такой обобщённый автомат Бюхи A = (S, S0 , δ, F)распознаёт язык Tr (ϕ):IS — это всевозможные внутренне согласованныепредположения, построенные на основе замыканияФишера-Ладнера формулы ϕIS0 — это всевозможные предположения H, такие чтоϕ∈HIКаждой формуле ψUχ ∈ [ϕ]FL соответствует множествозаключительных состояний FψUχ , состоящее в точности изтех предположений H, для которых звенит звонок дляформулы ψUχδ(H1 , L, H2 ) ⇔IIIH1 и 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проверить, пуст ли язык L(AM ⊕ A¬ϕ )Пересечение автоматов БюхиУтверждениеДля любой пары автоматов Бюхи 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Проверка пустоты автомата БюхиУтверждениеЯзык, распознаваемый автоматом Бюхи A, непуст в томи только том случае, если из какого-либо начальногосостояния достижимо заключительное состояние,принадлежащее какой-либо компоненте сильнойсвязностиДоказательство.Очевидно?Примерaba, ba, baЯзык, распознаваемый этим автоматом, непустПроверка пустоты автомата БюхиУтверждениеЯзык, распознаваемый автоматом Бюхи A, непуст в томи только том случае, если из какого-либо начальногосостояния достижимо заключительное состояние,принадлежащее какой-либо компоненте сильнойсвязностиДоказательство.Очевидно?Примерaba, baЯзык, распознаваемый этим автоматом, пустСведение задачи model checking для LTL кпроблеме пустоты для автоматов БюхиИтогПусть M — произвольная модель Крипкеи ϕ — произвольная LTL-формулаТогдаM |= ϕ⇔L(AM ⊕ A¬ϕ ) = ∅Конец лекции 7.

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

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