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

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2017Лекция 7Задача model checking для LTLАлгоритмы верификации LTL-формул:табличный алгоритм,автоматный алгоритмАвтоматы Бюхи,их свойства и обобщенияЗадача model checking для LTLНапоминаниеAP — множество атомарных высказыванийМодель Крипке (над множеством AP) — это системаM = (S, S0 , R, L), гдеIS — конечное множество состоянийIS0 ⊆ S — множество начальных состоянийIR ⊆ S × S — тотальное отношение переходовIL : S → 2AP — функция разметкиОтношение переходов тотально, если для любого состоянияs ∈ S существует состояние s 0 ∈ S, такое что R(s, s 0 )s → s 0 — синоним R(s, s 0 )Задача model checking для LTLПример: кофейный автоматidletea1coin1errortea2coin2coffeeL(idle) = {idle}L(coin1 ) = {OneCoin, ReadyForTea}L(error ) = {OneCoin, ShowErrorMessage}L(tea1 ) = {GiveTea}L(coin2 ) = {TwoCoins, ReadyForTea, ReadyForCoffee}L(coffee) = {GiveCoffee}L(tea2 ) = {GiveTea, OneCoin}Задача model checking для LTLНапоминаниеБНФ, определяющая синтаксисс LTL-формул ltlf (над AP):ltlf ::=a | ltlf ∨ ltlf | ltlf & ltlf | ¬ltlf | ltlf → ltlf |Xltlf | Fltlf | Gltlf | ltlf Ultlf(a ∈ AP)В лекции 4 давалось немного другое определение LTL-формулОтличия:I отсутствует символ A, с которого в лекции 4 начиналаськаждая LTL-формулаIIэтот символ избыточен и потому опускаетсяотсутствует оператор RIлекция 4: ϕRψ ≡ ¬(¬ϕU¬ψ)Задача model checking для LTLПримеры LTL-требований:IFGiveCoffeeIG(TwoCoins → ¬XShowErrorMessage)IG¬(OneCoin & XGiveCoffee)IGF(GiveTea ∨ GiveCoffee)IG¬ShowErrorMessage → GF(GiveTea ∨ GiveCoffee)IG(OneCoin ∨ TwoCoins ∨ GiveTea ∨ GiveCoffeeUidle)А какие из этих требований выполнены для предложенногокофейного автомата?Задача model checking для LTLLTL-формулой ϕ определяется свойство трасс Tr (ϕ):(tr = A0 , A1 , A2 , .

. . )Itr ∈ Tr (p), p ∈ APITr (ψ ∨ χ) = Tr (ψ) ∪ Tr (χ), Tr (ψ & χ) = Tr (ψ) ∩ Tr (χ),Tr (¬ψ) = (2AP )ω \ Tr (ψ), Tr (ψ → χ) = Tr (¬ψ ∨ χ)Itr ∈ Tr (Xψ)⇔tr 1 ∈ Tr (ψ)Itr ∈ Tr (Fψ)tr k ∈ Tr (ψ)⇔существует k, k ∈ N0 , такое чтоItr ∈ Tr (Gψ) ⇔ для любого k, k ∈ N0 , верноtr k ∈ Tr (ψ)tr ∈ Tr (ψUχ) ⇔ существует k, k ∈ N0 , такое чтоIII⇔p ∈ A0tr k ∈ Tr (χ)для любого m, m ∈ N0 , m < k, верно tr m ∈ Tr (ψ)?Задача model checking для LTL (M |= ϕ) может быть?переформулирована так: Tr (M) ⊆ Tr (ϕ)Табличный алгоритм model checking для LTLМожно ли проверить выполнимость LTL-формулы на моделиКрипке, размечая состояния модели подформулами аналогичнотому, как это делалось для CTL?CTL-формулы — это формулы состояния: значение такойформулы в каждом состоянии несложно выводится из значенияеё подформул в каждом состоянииLTL-формулы ϕ — это формулы пути: какие-то пути,исходящие из состояния, могут удовлетворять свойству Tr (ϕ),а какие-то — нетЧтобы проверить, выполнена ли LTL-формула в состоянии,может потребоваться перебрать всевозможные вариантытого, какие её подформулы верны, а какие — нет, для каждогосостоянияНебольшая пауза1.

Все ли помнят, что табличный алгоритм model checkingдля LTL уже рассказывался?2. Все ли помнят, как выглядело описание алгоритма?3. Все ли представляют, как этот алгоритм работает хоть длякаких-нибудь LTL-формулы и модели Крипке?4. Все ли помнят, почему этот алгоритм работает?Всё это рассказывалось давно, и тогда ещё не было такогоглубокого понимания задачи model checking, как есть сейчасПоэтому имеет смысл напомнить, как выглядит табличныйалгоритм проверки LTL-формулТабличный алгоритм model checking для LTLПример:ϕ: pUqM:pqpppВерно ли соотношение M |= ϕ?Табличный алгоритм model checking для LTLПопытаемся доказать, что M 6|= ϕДля этогоIупростим формулу ϕIразметим каждое состояние s модели всевозможными“хорошими” предположениями о том, какие подформулыформулы ϕ истинны и какие ложны хотя бы для одногопути, исходящего из sIпроведём “хорошим” образом дуги от предположений,сформулированных для текущего момента времени итекущего состояния, к предположениям,сформулированным для следующего момента времени иследующего состоянияIпопробуем найти бесконечную последовательностьпредположений, начинающуюся с ϕ и демонстрирующуюпуть в M, не удовлетворяющий свойству ϕУпрощение формулыLTL-формулы ϕ и ψ равносильны, если Tr (ϕ) = Tr (ψ)LTL-формулу будем называть упрощённой, если онаIIсодержит только связки &, ¬ и операторы X, Uне содержит двойных отрицаний (двух подряд идущихсвязок ¬)Утверждение.

Для любой LTL-формулы существуетравносильная упрощённая LTL-формулаДоказательство. Достаточно поочерёдно исключить изформулы всеIG:Gϕ ≡ ¬F¬ϕIF:Fϕ ≡ true U ϕI→:I∨:I¬¬:ϕ → ψ ≡ ¬ϕ ∨ ψϕ ∨ ψ ≡ ¬(¬ϕ & ¬ψ)¬¬ϕ ≡ ϕHДалее проверяемая формула полагается упрощённойПредположенияПри разметке состояний модели M для проверки формулы ϕиспользуются формулы из замыкания Фишера-Ладнера [ϕ]fl ,содержащегоIIвсе подформулы формулы ϕ, кроме подформул вида ¬ψX(ψUχ) для каждой подформулы ψUχ формулы ϕIпояснение того, зачем включать в [ϕ]fl такие X-формулы,будет дальшеПредположение (для формулы ϕ) — это подмножествомножества [ϕ]fl , в котором каждая формула помечена какистинная или ложнаяДля краткости будем использовать запись ¬ψ как синоним ψ, изапись ¬ψ как синоним ψХорошие и плохие предположенияПредположение H согласованно с множеством атомарныхвысказываний A, если для любого a, a ∈ AP, верноa∈H ⇔a∈AХорошее предположение H, помечающее состояние s моделиКрипке (S, S0 , R, L), удовлетворяет двум условиям:1.

согласованность с состоянием s, то есть согласованность сатомарными высказываниями L(s)2. внутренняя согласованность: для любых формулψ, ψ1 & ψ2 , χ1 Uχ2 ∈ [ϕ]FL верно:IIIψ∈H ⇔ψ∈/Hψ1 & ψ2 ∈ H ⇔ ψ1 , ψ2 ∈ Hχ1 Uχ2 ∈ H ⇔ χ2 ∈ H или {χ1 , X(χ1 Uχ2 )} ⊆ HТабличный алгоритм: разметим каждое состояние моделиКрипке всевозможными внутренне согласованнымипредположениями, согласованными с размечаемым состояниемХорошие и плохие предположенияIвнутренняя согласованность: для любых формулψ, ψ1 & ψ2 , χ1 Uχ2 ∈ [ϕ]FL верно:IIIψ∈H ⇔ψ∈/Hψ1 & ψ2 ∈ H ⇔ ψ1 , ψ2 ∈ Hχ1 Uχ2 ∈ H ⇔ χ2 ∈ H или {χ1 , X(χ1 Uχ2 )} ⊆ HПояснение: предположение H внутренне согласованно ⇔существует трасса, удовлетворяющая истинным и неудовлетворяющая ложным свойствам предположенияВ частности, справедлива следующая равносильность:ψUχ ≡ χ ∨ ψ & X(ψUχ)Это означает, чтоIесли χ, то ψUχIесли ψ и χ, то ψUχIесли ψ и χ, то ψUχ ⇔ X(ψUχ)Хорошие и плохие предположенияВернёмся к примеру:ϕ: pUqM:pqpppРазметим состояния модели M хорошими предположениямиХорошие и плохие предположенияϕ: pUqM:H1H1H2H3H4pH1H3pqH2H4H2H2ppH1H1H2= {p, q, X(pUq), pUq}= {p, q, X(pUq), pUq}= {p, q, X(pUq), pUq}= {p, q, X(pUq), pUq}Хорошие и плохие обещания на завтраУпорядоченная пара предположений (H1 , H2 ) внешнесогласованна, если для любой формулы вида Xψ из [ϕ]fl верно:Xψ ∈ H1⇔ψ ∈ H2Табличный алгоритм: соединим дугой все пары внешнесогласованных предположений H1 , H2 , помечающих состоянияs1 , s2 соответственно, такие что s1 → s2Пояснение: если трасса tr удовлетворяет истинным и неудовлетворяет ложным свойствам предположения H1 , а трассаtr 1 удовлетворяет истинным и не удовлетворяет ложнымсвойствам предположения H2 , то пара (H1 , H2 ) обязательноявляется внешне согласованнойХорошие и плохие обещания на завтраВернёмся к примеру:ϕ: pUqM:H1pH1H3pqH2H4H2H2ppH1H1H2H1 = {p, q, X(pUq), pUq} H3 = {p, q, X(pUq), pUq}H2 = {p, q, X(pUq), pUq} H4 = {p, q, X(pUq), pUq}Соединим дугами соседние внешне согласованныепредположенияХорошие и плохие обещания на завтраϕ: pUqM:H1pH1H3pqH2H4H2H2ppH1H1H2H1 = {p, q, X(pUq), pUq}H2 = {p, q, X(pUq), pUq}H3 = {p, q, X(pUq), pUq}H4 = {p, q, X(pUq), pUq}Система ХинтиккиH1 = {p, q, X(pUq), pUq} H3 = {p, q, X(pUq), pUq}H2 = {p, q, X(pUq), pUq} H4 = {p, q, X(pUq), pUq}В некоторых случаях бесконечная последовательность внешнесогласованных предположений демонстрирует наличие пути вмодели Крипке, удовлетворяющего истинным и неудовлетворяющего ложным формулам первого предположения:I H1 → H1 → H 3 → .

. . :трасса пути, размеченного таким образом, входит вTr (pUq)I H2 → . . . :трасса пути, размеченного таким образом, не входит вTr (pUq)К сожалению, это работает не всегда:I H1 → H1 → · · · → H1 → . . . : несмотря на то что pUq ∈ H1 ,трасса пути, размеченного таким образом, не входит вTr (pUq)“Плохая” особенность бесконечной последовательностипредположений H1 :Система ХинтиккиДля формулы ψUχ в предположении H звенит звонок, вернохотя бы одно из двух:Iχ∈HIX(ϕUψ) ∈ HСистема Хинтикки для модели Крипке M и формулы ϕ — этограф следующего вида:Iвершины — всевозможные пары (s, H), где s — состояниемодели и H — предположение, которым состояниепомечается согласно табличному алгоритмуI(s, H) → (s 0 , H 0 ) ⇔ s → s 0 и H → H 0Iвершина (s, H) объявляется начальной, если s —начальное состояние модели и ϕ ∈ HIкаждой подформуле Φ вида ψUχ формулы ϕприсваивается уникальный цвет cΦIвершина (s, H) помечается цветом cΦ , если в H звенитзвонок для формулы ΦСистема ХинтиккиВернёмся к примеру:ϕ: pUqM:H1pH1H3pqH2H4H2H2ppH1H1H2H1 = {p, q, X(pUq), pUq}H2 = {p, q, X(pUq), pUq}H3 = {p, q, X(pUq), pUq}H4 = {p, q, X(pUq), pUq}Система ХинтиккиСистема Хинтикки для M и ϕ:H1H1H3H2H4H2H2H1H1H2H1 = {p, q, X(pUq), pUq}H2 = {p, q, X(pUq), pUq}H3 = {p, q, X(pUq), pUq}H4 = {p, q, X(pUq), pUq}Система ХинтиккиБесконечный маршрут в системе Хинтикки являетсяопровергающим, если онIначинается в начальной вершинеIдля каждого цвета cΦ содержит бесконечно много вершин,окрашенных в этот цветТеорема.

M 6|= ϕ ⇔ в системе Хинтикки для M и ϕсуществует опровергающий маршрутТеорема. В системе Хинтикки существуетопровергающий маршрут ⇔ в этой системе из начальнойвершины достижима компонента сильной связности, ввершинах которой встречаются все цветаОбоснование этих утверждений смотрите в курсе“Математическая логика и логическое программирование” длякафедр 3-го потока факультетаСистема ХинтиккиОбратно к примеру:H1H1H3H2H4H2H2H1H1H2Две подходящие компоненты сильной связности обведеныпрямоугольникамиОдна из них достижима из начальной вершины, а значит,M 6|= pUqСистема ХинтиккиДостоинства табличного алгоритма:...Недостатки табличного алгоритма:Iтруден для пониманияIтребуется явный обход графа, полученного из моделиКрипке разметкой состояний предположениями(а можно ли этого избежать?)Iсостояния могут размечаться большими множествамиформул (а насколько большими?)Алгоритмы model checkingЗадача model checking для CTL имеет эффективнуюальтернативу табличному алгоритму: символьный алгоритмЗадача model checking для LTL также имеет эффективнуюальтернативу табличному алгоритму: автоматный алгоритмЕсли программное средство производит верификацию дляCTL, то скорее всего в основе реализованного алгоритмаверификации лежит символьный алгоритмЕсли программное средство производит верификацию для LTL,то скорее всего в основе реализованного алгоритмаверификации лежит автоматный алгоритмАвтоматный алгоритм model checking для LTLОбщая схема работы автоматного алгоритма:Iимеются модель Крипке M и LTL-формула ϕIпостроить автомат AM , распознающий множество Tr (M)Iпостроить автомат A¬ϕ , распознающий множество Tr (¬ϕ)Iпостроить автомат AM ⊕ A¬ϕ , распознающий множествоTr (M) ∩ Tr (¬ϕ)проверить, пусто ли множество, распознаваемоеавтоматом 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 ), .