Лекция 7 Задача model checking для ltl алгоритмы верификации ltl-формул: табличный алгоритм, автоматный алгоритм



Скачать 324.65 Kb.
Pdf просмотр
Дата05.04.2017
Размер324.65 Kb.
Просмотров131
Скачиваний0
ТипЛекция

Математические методы верификации схем и программ
Лекторы:
Захаров Владимир Анатольевич
Подымов Владислав Васильевич e-mail рассказчика:
valdus@yandex.ru
Осень 2016

Лекция 7
Задача model checking для LTL
Алгоритмы верификации LTL-формул:
табличный алгоритм,
автоматный алгоритм
Автоматы Бюхи,
их свойства и обобщения

Задача model checking для LTL
Напоминание
AP
— множество атомарных высказываний
Модель Крипке над множеством AP — это система
M = (S , S
0
, R, L), где
S — конечное множество состояний
S
0
⊆ S — множество начальных состояний
R ⊆ S × S —
тотальное отношение переходов
L : S → 2
AP

функция разметки
Отношение переходов тотально
, если для любого состояния s ∈ S существует состояние s
∈ S, такое что R(s, s )
s → s
— синоним R(s, s )

Задача model checking для LTL
Пример
: кофейный автомат idle coin
1
coin
2
error coffee tea
1
tea
2
L(idle) = {idle}
L(coin
1
) = {OneCoin, ReadyForTea}
L(error ) = {OneCoin, ShowErrorMessage}
L(tea
1
) = {GiveTea}
L(coin
2
) = {TwoCoins, ReadyForTea, ReadyForCoffee}
L(coffee) = {GiveCoffee}
L(tea
2
) = {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-спецификаций:
FGiveCoffee
G(TwoCoins → ¬XShowErrorMessage)
G¬(OneCoin & XGiveCoffee)
GF(GiveTea ∨ GiveCoffee)
G¬ShowErrorMessage → GF(GiveTea ∨ GiveCoffee)
G(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 |= ϕ и
M |= ψ)

Табличный алгоритм model checking для LTL
Можно ли описать алгоритм разметки состояний подформулами, похожий на табличный алгоритм для CTL?
При попытке это сделать возникает такая проблема:
табличный алгоритм размечает состояния формулами,
выполняющимися в этих состояниях
AFϕ: при построении всех трасс будет достигнуто состояние
, в котором верна формула ϕ
Fϕ: в любой трассе наступит момент времени, когда будет выполнена формула ϕ
момент времени, подразумеваемый формулой Fϕ, не связан напрямую ни с каким состоянием
Несоответствие моментов времени и состояний усложняет принципы работы табличного алгоритма для LTL
Однако эти трудности могут быть преодолены

Небольшая пауза
1.
Все ли помнят, что табличный алгоритм model checking для LTL уже рассказывался?
2.
Все ли помнят, как выглядело описание алгоритма?
3.
Все ли представляют, как этот алгоритм работает хоть для каких-нибудь LTL-формулы и модели Крипке?
4.
Все ли помнят, почему этот алгоритм работает?
Всё это рассказывалось давно, и тогда не было такого понимания задачи model checking, как есть сейчас
Поэтому можно повторить, как выглядит табличный алгоритм проверки LTL-формул

Табличный алгоритм model checking для LTL
Пример:
ϕ: pUq
M:
p p
q p
p
Верно ли, что M |= ϕ?

Табличный алгоритм model checking для LTL
Попытаемся доказать, что M |= ϕ
Будем обходить состояния модели и компактно описывать всевозможные способы работы системы, размечая состояния множествами формул, истинных в данный момент работы
Отталкиваясь от предположения о том, какие формулы истинны и
ложны для текущего состояния в текущий момент времени (сегодня), будем строить предположения о следующем моменте времени (завтра), переходя к следующему состоянию
Например,
находясь в состоянии p
, мы точно знаем:
p
,
q
Кроме того, можно предположить как pUq
, так и pUq

Табличный алгоритм model checking для LTL
Чтобы согласовать предположения об истинности формул сегодня и завтра, будем также делать предположения вида Xϕ
для некоторых формул ϕ
Зачем так усложнять себе жизнь?
Например, справедлива такая эквивалентность:
pUq = q ∨ p & X(pUq)
Если предположить сегодня
X(pUq)
, то сегодня pUq

сегодня p
или q
завтра мы обязаны предположить pUq
Если предположить сегодня
X(pUq)
, то сегодня pUq

сегодня q
завтра мы обязаны предположить pUq

Табличный алгоритм model checking для LTL
Пример:
p p
q
X(pUq)
pUq pUq
X(pUq)
pUq
Успех!
: доказано, что для любой трассы, начинающаейся с этих трёх состояний, верно pUq

Табличный алгоритм model checking для LTL
Пример:
p p
p
X(pUq)
pUq pUq
X(pUq)
pUq
Успех!
: доказано, что для любой трассы, в которой всегда верно p и неверно q, неверно и pUq

Табличный алгоритм model checking для LTL
Пример:
p p
p
X(pUq)
pUq pUq
X(pUq)
pUq
Неуспех?
Согласно предположениям, верно pUq
Для этой трассы свойство pUq не выполнено
Как можно описать особенность строящихся предположений, из- за которой они не совпали с реальными свойствами трассы?
Почти всегда предполагается q
и
X(pUq)

Табличный алгоритм model checking для LTL
Чтобы исключить неуспешное построение предположений,
достаточно следить за тем, что именно мы предполагаем для посылок, следствий и обещаний на завтра для формул вида
ϕUψ
Для формулы ϕUψ сегодня звенит звонок
, если для текущего предположения верно хотя бы одно из двух:
ψ
или
X(ϕUψ)
В
допустимой последовательности предположений для каждой подформулы вида ϕUψ или ϕRψ проверяемой формулы звонок должен звенеть бесконечно часто

Табличный алгоритм model checking для LTL
Вернёмся к примеру:
ϕ: pUq
M:
p p
q p
p
Попробуем разметить состояния модели предположениями всевозможными способами

Табличный алгоритм model checking для LTL
p p
q p
p
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
H
1
= {
p
,
q
,
X(pUq), pUq
}
H
2
= {
p
,
q
,
X(pUq)
,
pUq
}
H
3
= {
p
,
q
,
X(pUq)
,
pUq
}
H
4
= {
p
,
q
,
X(pUq)
,
pUq
}

Табличный алгоритм model checking для LTL
p p
q p
p
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
— предположение соответствует начальному состоянию и со- держит pUq
— звенит звонок для pUq

Табличный алгоритм model checking для LTL
p p
q p
p
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
M |= ϕ

из исходит маршрут, в котором звонок звенит бесконечно часто

Табличный алгоритм model checking для LTL
p p
q p
p
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
M |= ϕ

из достижима компонента сильной связности, содержащая хотя бы одну вершину, в которой звенит звонок

Табличный алгоритм model checking для LTL
p p
q p
p
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
H
1
H
2
H
1
H
2
H
3
H
4
H
2
H
1
H
2
H
1
Итог: M |= pUq

Табличный алгоритм model checking для LTL
Более полное описание табличного алгоритма выглядит так:
исключим из формулы ϕ операторы →, ∨, F, G, оставив только &, ¬, X, U, и уберём все двойные отрицания построим множество всех формул, которые могут появиться при разметке состояний модели Крипке предположениями для каждого состояния s определим множество “хороших”
для этого состояния предположений H
s
, и заменим состояние s на совокупность состояний (s, H), H ∈ H
s проведём всевозможными способами дуги
(s
1
, H
1
) → (s
2
, H
2
) так, чтобы выполнялось s
1
→ s
2
и при этом предположения на сегодня (H
1
) и завтра (H
2
) не противоречили друг другу

Табличный алгоритм model checking для LTL
Более полное описание табличного алгоритма выглядит так:
в расклеенной таким образом модели найдём компоненты сильной связности, такие что для каждой формулы вида
ψUχ, которая может появиться в предположениях, хотя бы в одном состоянии звенит звонок проверим, найдётся ли состояние (s, H), такое что s — начальное состояние исходной модели,
проверяемая формула предполагается ложной в H
из состояния (s, H) достижима хотя бы одна из найденных компонент сильной связности

Табличный алгоритм model checking для LTL
Преобразование формулы
Чтобы привести формулу к нужному виду, достаточно использовать такие эквивалентные преобразования:
Gϕ = ¬F¬ϕ
Fϕ = trueUϕ
ϕRψ = ¬(¬ϕU¬ψ)
ϕ → ψ = ¬ϕ ∨ ψ
ϕ ∨ ψ = ¬(¬ϕ & ¬ψ)
¬¬ϕ = ϕ

Табличный алгоритм model checking для LTL
Замыкание Фишера-Ладнера
[ϕ]
FL
формулы ϕ — это множество всех формул, которые используются при разметке состояний модели Крипке предположениями для проверки формулы ϕ, и его можно описать так:
каждая подформула формулы ϕ, не имеющая отрицание внешней связкой, входит в [ϕ]
FL
если (ψUχ) ∈ [ϕ]
FL
, то X(ψUχ) ∈ [ϕ]
FL
Предположение
— это подмножество [ϕ]
FL
, в котором каждая формула покрашена в зелёный или красный цвет (считается истинной или ложной соответственно)
Для краткости будем использовать запись
¬ψ
как синоним
ψ
, а запись
¬ψ
— как синоним
ψ

Табличный алгоритм model checking для LTL
Хорошее предположение
H для заданного состояния s модели Крипке (S, S
0
, R, L) удовлетворяет двум условиям:
1.
для любого атомарного высказывания a верно:
a
∈ H ⇔
a ∈ L(s) (
согласованность с атомарными высказываниями
L(s)
, или согласованность с состоянием s
)
2.
внутренняя согласованность
: для любых формул
ψ, ψ
1
& ψ
2
, χ
1

2
∈ [ϕ]
FL
верно:
ψ
∈ H ⇔
ψ
/
∈ H
ψ
1
& ψ
2
∈ H ⇔
ψ
1
,
ψ
2
∈ H
χ
1

2
∈ H ⇔
χ
2
∈ H или {
χ
1
,
X(χ
1

2
)
} ⊆ H

Табличный алгоритм model checking для LTL
Не противоречащие друг другу предположения H
1
, H
2
на сегодня и завтра внешне согласованы
: для любой формулы
Xψ ∈ [ϕ]
FL
верно:

∈ H
1

ψ
∈ H
2
При разметке состояний модели Крипке предположениями выбираются всевозможные предположения, согласованные внутренне и с размечаемым состоянием дуги проводятся для всевозможных пар внешне согласованных предположений
Табличный алгоритм model checking для LTL полностью описан

Табличный алгоритм model checking для LTL
Обоснование корректности этого алгоритма непросто для понимания и приведено в лекциях по курсу
“Математическая логика и логическое программирование”
Достоинства табличного алгоритма:
Недостатки табличного алгоритма:
труден для понимания требуется явный обход графа, полученного из модели
Крипке разметкой состояний предположениями
(
а можно ли этого избежать?
)
состояния могут размечаться большими множествами формул (
а насколько большими?
)

Алгоритмы model checking
Задача model checking для CTL имеет альтернативу табличному алгоритму:
символьный алгоритм
Задача model checking для LTL также имеет альтернативу табличному алгоритму:
автоматный алгоритм
Если программное средство производит верификацию для
CTL, то скорее всего в основе реализованного алгоритма верификации лежит символьный алгоритм
Если программное средство производит верификацию для LTL,
то скорее всего в основе реализованного алгоритма верификации лежит автоматный алгоритм

Автоматный алгоритм model checking для LTL
Общая схема работы автоматного алгоритма:
имеются модель Крипке M и LTL-формула ϕ
построить автомат A
M
, описывающий в точности множество всех трасс модели M
построить автомат A
¬ϕ
, описывающий в точности множество всех трасс, не обладающих свойством ϕ
построить автомат A
M
⊕ A
¬ϕ
, описывающий в точности множество всех трасс модели M, не обладающих свойством ϕ
проверить, описывается ли автоматом A
M
⊕ A
¬ϕ
пустое множество трасс если да, то M |= ϕ
если нет, то M |= ϕ
И что же это за автоматы?

Автоматы Бюхи
Автомат Бюхи над алфавитом Σ — это система
A = (S , S
0
, δ, F ), где
S — конечное множество состояний
S
0
⊆ S — множество начальных состояний
δ ⊆ S × Σ × S —
отношение переходов
F ⊆ S — множество заключительных состояний s
σ
1
,...,σ
k
−−−−−→ s
— обозначение множества переходов
δ(s, σ
1
, s ), . . . , δ(s, σ
k
, s )

Автоматы Бюхи
Пример a
b a
a, b a, b
— начальное состояние
— заключительное состояние
Ничего не напоминает?
Синтаксис автоматов Бюхи в точности совпадает с синтаксисом конечных недетерминированных автоматов-распознавателей
Автомат Бюхи, прочитывая конечные слова, изменяет свои состояния точно так же, как и автоматы распознаватели
Отличие этих двух моделей — в семантике: распознаваемом языке
(множестве слов)

Автоматы Бюхи
Автоматы Бюхи строятся для того, чтобы проверять, содержит ли модель Крипке трассы, не удовлетворяющие заданному свойству
И трассы, и свойства основаны на бесконечных словах
Язык, распознаваемый автоматом Бюхи, — это множество бесконечных слов в заданном алфавите
Множество всех бесконечных слов в алфавите Σ будем обозначать так:
Σ
ω
Трасса автомата Бюхи A = (S, S
0
, δ, F ), порождаемая бесконечным словом σ
1
σ
2
σ
3
. . . — это любая бесконечная последовательность его состояний вида s
0
σ
1
−→ s
1
σ
2
−→ s
2
σ
3
−→ . . . ,
такая что s
0
∈ S
0
Tr (A, w )
— множество всех трасс автомата Бюхи A,
порождаемых бесконечным словом w

Автоматы Бюхи inf(t)
— множество состояний, встречающихся бесконечно часто в трассе t автомата Бюхи
Язык L(A), распознаваемый автоматом Бюхи
A = (S , S
0
, δ, F ),
определяется так:
L(A) = {w | ∃t ∈ Tr (A, w ) : inf (t) ∩ F = ∅}
Проще говоря, бесконечное слово w распознаётся автоматом
Бюхи, если среди всех трасс автомата, получаемых при прочитывании этого слова, есть такая, в которой бесконечно часто повторяется хотя бы одно заключительное состояние

Автоматы Бюхи
Пример a
b a
a, b a, b
Какой язык распознаётся этим автоматом Бюхи?
Этот язык состоит в точности из всех бесконечных слов следующего вида:
(ab)
ω
— слово, получающееся бесконечным повторением слова ab
(ab)
+
(a|b)
ω
— слово, состоящее из хотя бы одного повторения слова ab, за которым следует любое бесконечное сочетание букв a, b

Автоматы Бюхи
А как построить автомат Бюхи, распознающий в точности множество всех трасс заданной модели Крипке?
Очень просто:
алфавит, над которым строится автомат: 2
AP
объявим состояния модели состояниями автомата Бюхи начальные состояния модели объявим начальными состояниями автомата соединим состояния автомата дугами так же, как они были соединены в модели множество высказываний, помечавшее состояние модели,
переместим на каждую исходящую из состояния дугу в автомате объявим все состояния автомата заключительными

Автоматы Бюхи
Пример p
p q
p p
Автомат, распознающий в точности множество всех трасс этой модели Крипке, может выглядеть так:
{p}
{p}
{q}
{p}
{p}
{p}
{q}

Автоматы Бюхи
А как построить автомат Бюхи, распознающий в точности множество Tr (ϕ) для LTL-формулы ϕ?
Начнём с примеров
GFa
S : a /
∈ S
S : a ∈ S
S : a /
∈ S
S : a ∈ S

Автоматы Бюхи
А как построить автомат Бюхи, распознающий в точности множество Tr (ϕ) для LTL-формулы ϕ?
Начнём с примеров
FGa
S : any
S : a ∈ S
S : a ∈ S

Автоматы Бюхи
А как построить автомат Бюхи, распознающий в точности множество Tr (ϕ) для LTL-формулы ϕ?
Начнём с примеров
G(a → Fb)
S : b ∈ S
S : a /
∈ S
S : a ∈ S , b /
∈ S
S : b ∈ S
S : b /
∈ S
А как построить такой автомат Бюхи для LTL-формулы произ- вольного вида?

Построение автомата Бюхи по LTL-формуле
Общая схема построения автомата Бюхи по
LTL-формуле:
LTL-формула ϕ
Обобщённый автомат Бюхи GA
ϕ
Автомат Бюхи A
ϕ

Обобщённые автоматы Бюхи
Обобщённый автомат Бюхи над алфавитом Σ — это система
GA = (S , S
0
, δ, F ), где
S — конечное множество состояний
S
0
⊆ S — множество начальных состояний
δ ⊆ S × Σ × S —
отношение переходов
F ⊆ 2
S
— семейство множеств заключительных состояний
Отличие от необобщённого автомата Бюхи только в том, как трактуются заключительные состояния
Бесконечное слово w распознаётся обобщённым автоматом
Бюхи GA, если среди трасс, порождаемых словом w ,
существует трасса t, такая что inf (t) ∩ F = ∅ для любого множества F из семейства F

Обобщённые автоматы Бюхи
Утверждение
Для любого обобщённого автомата Бюхи существует необобщённый автомат Бюхи, распознающий тот же язык
Доказательство.
Рассмотрим произвольный обобщённый автомат Бюхи
GA = (S , S
0
, δ, {F
0
, . . . , F
k−1
})
Требуемый автомат Бюхи A = (S , S
0
, δ, F ) имеет следующее устройство:
S = S × {0, . . . , k − 1}
S
0
= S
0
× {0}
F = {F
i
× {i } | 0 ≤ i < k}
δ ((s, i ), σ, (s , i )) ⇔ δ(s, σ, s ) и s /
∈ F
i
δ ((s, i ), σ, (s , i + 1(mod k))) ⇔ δ(s, σ, s ) и s ∈ F
i

Построение автомата Бюхи по LTL-формуле
И как же построить обобщённый автомат Бюхи, распознающий свойство ϕ?
Например, такой обобщённый автомат Бюхи A = (S, S
0
, δ, F )
распознаёт свойство ϕ:
S — это всевозможные внутренне согласованные предположения
, построенные на основе замыкания
Фишера-Ладнера формулы ϕ
S
0
— это всевозможные предположения H, такие что
ϕ
∈ H
Каждой формуле ψUχ ∈ [ϕ]
FL
соответствует множество заключительных состояний F
ψUχ
, состоящее в точности из тех предположений H, для которых звенит звонок для формулы ψUχ:
ψ
∈ H или
X(ϕUψ)
∈ H
δ(H
1
, L, H
2
) ⇔
H
1
и H
2

внешне согласованные предположения предположение H
1
согласовано с атомарными высказываниями
L

Автоматный алгоритм model checking для LTL
Промежуточный итог
Для заданных модели Крипке M и LTL-формулы ϕ требуется проверить соотношение
M |= ϕ
Что для этого уже сделано:
для модели M построен автомат Бюхи A
M
, такой что
L(A) = Tr (M)
для формулы ¬ϕ построен автомат Бюхи A
¬ϕ
, такой что
L(A
¬ϕ
) = Tr (¬ϕ)
Что осталось сделать:
построить автомат A
M
⊕ A
¬ϕ
, распознающий язык
L(A
M
) ∩ L(A
¬ϕ
)
проверить, имея описание автомата, пуст ли этот язык

Пересечение автоматов Бюхи
Утверждение
Для любой пары автоматов Бюхи A
1
, A
2
существует автомат Бюхи A, распознающий язык L(A
1
) ∩ L(A
2
)
Доказательство.
Рассмотрим произвольные автоматы Бюхи A
1
= (S
1
, S
1 0
, δ
1
, F
1
),
A
2
= (S
2
, S
2 0
, δ
2
, F
2
)
Достаточно построить обобщённый автомат Бюхи,
распознающий язык L(A
1
) ∩ L(A
2
)
Требуемый обобщённый автомат Бюхи GA имеет следующее устройство:
GA = (S
1
× S
2
, S
1 0
× S
2 0
, δ, {F
1
× S
2
, S
1
× F
2
}), где
δ((s
1
, s
2
), σ, (s
1
, s
2
)) ⇔ δ
1
(s
1
, s
1
) и δ
2
(s
2
, s
2
)

Проверка пустоты автомата Бюхи
Утверждение
Язык L(A), распознаваемый автоматом Бюхи A, пуст тогда и только тогда, никакое заключительное состояние, принадлежащее циклу, не достижимо ни из какого начального состояния
Доказательство.
Очевидно?
Пример a
b a
a, b a, b
Язык, распознаваемый этим автоматом, непуст

Проверка пустоты автомата Бюхи
Утверждение
Язык L(A), распознаваемый автоматом Бюхи A, пуст тогда и только тогда, никакое заключительное состояние, принадлежащее циклу, не достижимо ни из какого начального состояния
Доказательство.
Очевидно?
Пример a
b a
a, b
Язык, распознаваемый этим автоматом, пуст

Сведение задачи model checking для LTL к проблеме пустоты для автоматов Бюхи
Итог
Пусть M — произвольная модель Крипке и ϕ — произвольная LTL-формула
Тогда
M |= ϕ

L(A
M
⊕ A
¬ϕ
) = ∅

Конец лекции 7


Поделитесь с Вашими друзьями:


База данных защищена авторским правом ©nethash.ru 2017
обратиться к администрации

войти | регистрация
    Главная страница


загрузить материал