Лекция 7. Верификация LTL. Автоматы Бюхи

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2016Лекция 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 ) имеет следующий вид:ltlf ::=a | ltlf ∨ ltlf | ltlf & ltlf | ¬ltlf | ltlf → ltlf |Xltlf | Fltlf | Gltlf | ltlf Ultlf | ltlf Rltlf(a ∈ AP)В лекции 4 давалось немного другое определение LTL-формулОтличие — отсутствует символ A, с которого в лекции 4начиналась каждая LTL-формулаЕсли ограничиться рассмотрением только логики линейноговремени, то этот символ избыточен и опускаетсяЗадача 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 для LTLФормулировка задачи model checking для LTL: для заданныхмодели Крипке M и LTL-формулы ϕ проверить соотношениеM |= ϕА как это расшифровывается?Проверить, что любая (бесконечная) трасса системы Mудовлетворяет свойству ϕЕсли имеется LTL-формула ϕ, то для любой трассы любоймодели Крипке можно проверить, удовлетворяет ли трассасвойству ϕИными словами, каждой LTL-формулой ϕ опредеяетсямножество трасс Tr (ϕ), таких что какая бы ни была модель M,верноM |= ϕ ⇔ Tr (M) ⊆ Tr (ϕ)Сравнение выразительных возможностейLTL и CTLА имеет ли смысл рассматривать логику линейного времени,если имеются “хорошие” алгоритмы проверки CTL-формул?Утверждение.

Существует LTL-формула, которой неэквивалентна ни одна CTL-формула(лекция 4)А может быть, мы зря отдельно рассматривали логикуветвящегося времени?Утверждение. Существует CTL-формула, которой неэквивалентна ни одна LTL-формула(лекция 4)(формулы ϕ, ψ логики CTL* эквивалентны, если для любоймодели Крипке M верно либо M |= ϕ и M |= ψ, либо M 6|= ϕ иM 6|= ψ)Табличный алгоритм model checking для LTLМожно ли описать алгоритм разметки состоянийподформулами, похожий на табличный алгоритм для CTL?При попытке это сделать возникает такая проблема:Iтабличный алгоритм размечает состояния формулами,выполняющимися в этих состоянияхIAFϕ: при построении всех трасс будет достигнутосостояние, в котором верна формула ϕIFϕ: в любой трассе наступит момент времени, когдабудет выполнена формула ϕIмомент времени, подразумеваемый формулой Fϕ, несвязан напрямую ни с каким состояниемНесоответствие моментов времени и состояний усложняетпринципы работы табличного алгоритма для LTLОднако эти трудности могут быть преодоленыНебольшая пауза1.

Все ли помнят, что табличный алгоритм model checkingдля LTL уже рассказывался?2. Все ли помнят, как выглядело описание алгоритма?3. Все ли представляют, как этот алгоритм работает хоть длякаких-нибудь LTL-формулы и модели Крипке?4. Все ли помнят, почему этот алгоритм работает?Всё это рассказывалось давно, и тогда не было такогопонимания задачи model checking, как есть сейчасПоэтому можно повторить, как выглядит табличный алгоритмпроверки LTL-формулТабличный алгоритм model checking для LTLПример:ϕ: pUqM:pqpppВерно ли, что M |= ϕ?Табличный алгоритм model checking для LTLПопытаемся доказать, что M 6|= ϕБудем обходить состояния модели и компактно описыватьвсевозможные способы работы системы, размечая состояниямножествами формул, истинных в данный момент работыОтталкиваясь от предположения о том, какие формулыистинны и ложны для текущего состояния в текущий моментвремени (сегодня), будем строить предположения оследующем моменте времени (завтра), переходя кследующему состояниюНапример, находясь в состоянииp, мы точно знаем: p, qКроме того, можно предположить как pUq, так и pUqТабличный алгоритм model checking для LTLЧтобы согласовать предположения об истинности формулсегодня и завтра, будем также делать предположения вида Xϕдля некоторых формул ϕЗачем так усложнять себе жизнь?Например, справедлива такая эквивалентность:pUq = q ∨ p & X(pUq)Если предположить сегодня X(pUq), то⇔Iсегодня pUqсегодня p или qIзавтра мы обязаны предположить pUqЕсли предположить сегодня X(pUq), то⇔Iсегодня pUqсегодня qIзавтра мы обязаны предположить pUqТабличный алгоритм model checking для LTLПример:ppqX(pUq)pUqpUqpUqX(pUq)...Успех!: доказано, что для любой трассы, начинающаейся с этихтрёх состояний, верно pUqТабличный алгоритм model checking для LTLПример:pppX(pUq)pUqpUqX(pUq)pUq......Успех!: доказано, что для любой трассы, в которой всегда верноp и неверно q, неверно и pUqТабличный алгоритм model checking для LTLПример:pppX(pUq)pUqpUqX(pUq)pUq......Неуспех?IСогласно предположениям, верно pUqIДля этой трассы свойство pUq не выполненоКак можно описать особенность строящихся предположений, изза которой они не совпали с реальными свойствами трассы?Почти всегда предполагается q и X(pUq)Табличный алгоритм model checking для LTLЧтобы исключить неуспешное построение предположений,достаточно следить за тем, что именно мы предполагаем дляпосылок, следствий и обещаний на завтра для формул видаϕUψДля формулы ϕUψ сегодня звенит звонок, если для текущегопредположения верно хотя бы одно из двух: ψ или X(ϕUψ)В допустимой последовательности предположений для каждойподформулы вида ϕUψ или ϕRψ проверяемой формулы звонокдолжен звенеть бесконечно частоТабличный алгоритм model checking для LTLВернёмся к примеру:ϕ: pUqM:pqpppПопробуем разметить состояния модели предположениямивсевозможными способамиТабличный алгоритм model checking для LTLH1H1H2H3H4pH1H3pqH2H4H2H2ppH1H1H2= {p, q, X(pUq), pUq}= {p, q, X(pUq), pUq}= {p, q, X(pUq), pUq}= {p, q, X(pUq), pUq}Табличный алгоритм model checking для LTLH1H1H3H2H4H2H2H1H1H2— предположение соответствует начальному состоянию и содержит pUq— звенит звонок для pUqТабличный алгоритм model checking для LTLH1изH1H3H2H4H2H2H1H1H2M |6 = ϕ⇔исходит маршрут, в котором звонок звенит бесконечночастоТабличный алгоритм model checking для LTLH1изH1H3H2H4H2H2H1H1H2M |6 = ϕ⇔достижима компонента сильной связности, содержащаяхотя бы одну вершину, в которой звенит звонокТабличный алгоритм model checking для LTLH1Итог: M 6|= pUqH1H3H2H4H2H2H1H1H2Табличный алгоритм model checking для LTLБолее полное описание табличного алгоритма выглядит так:Iисключим из формулы ϕ операторы →, ∨, F, G, оставивтолько &, ¬, X, U, и уберём все двойные отрицанияIпостроим множество всех формул, которые могутпоявиться при разметке состояний модели КрипкепредположениямиIдля каждого состояния s определим множество “хороших”для этого состояния предположений Hs , и заменимсостояние s на совокупность состояний (s, H), H ∈ HsIпроведём всевозможными способами дуги(s1 , H1 ) → (s2 , H2 ) так, чтобы выполнялось s1 → s2 и приэтом предположения на сегодня (H1 ) и завтра (H2 ) непротиворечили друг другуТабличный алгоритм model checking для LTLБолее полное описание табличного алгоритма выглядит так:IIв расклеенной таким образом модели найдём компонентысильной связности, такие что для каждой формулы видаψUχ, которая может появиться в предположениях, хотя быв одном состоянии звенит звонокпроверим, найдётся ли состояние (s, H), такое чтоIIIs — начальное состояние исходной модели,проверяемая формула предполагается ложной в Hиз состояния (s, H) достижима хотя бы одна из найденныхкомпонент сильной связностиТабличный алгоритм model checking для LTLПреобразование формулыЧтобы привести формулу к нужному виду, достаточноиспользовать такие эквивалентные преобразования:IGϕ = ¬F¬ϕIFϕ = trueUϕIϕRψ = ¬(¬ϕU¬ψ)Iϕ → ψ = ¬ϕ ∨ ψIϕ ∨ ψ = ¬(¬ϕ & ¬ψ)I¬¬ϕ = ϕТабличный алгоритм model checking для LTLЗамыкание Фишера-Ладнера [ϕ]FL формулы ϕ — этомножество всех формул, которые используются при разметкесостояний модели Крипке предположениями для проверкиформулы ϕ, и его можно описать так:Iкаждая подформула формулы ϕ, не имеющая отрицаниевнешней связкой, входит в [ϕ]FLIесли (ψUχ) ∈ [ϕ]FL , то X(ψUχ) ∈ [ϕ]FLПредположение — это множество [ϕ]FL , в котором каждаяподформула покрашена в зелёный или красный цвет (считаетсяистинной или ложной соответственно)Для краткости будем использовать запись ¬ψ как синоним ψ, азапись ¬ψ — как синоним ψТабличный алгоритм model checking для LTLХорошее предположение H для заданного состояния sмодели Крипке (S, S0 , R, L) удовлетворяет двум условиям:1.