Лекция 10. Временные автоматы. Регионная модель Крипке. Сведение МС к TCTL и CTL

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2016Лекция 10Задача model checkingдля временных автоматови сетей временных автоматовЭквивалентность оценок таймеровВременные регионыи регионы состоянийОценка числа временных регионовРегионная модель КрипкеСведение MC для TCTL к MC для CTLНапоминаниеВременной автомат — это система (L, `0 , Σ, C , I , T ), гдеIL — конечное множество состояний автоматаI`0 ∈ L — начальное состояниеIΣ — конечное множество событийIC — конечное множество таймеровII : L → inv (C ) — разметка состояниий инвариантамиT ⊆ L × (Σ ∪ {λ}) × guard(C ) × 2C × L — отношениепереходовIIIтретья компонента перехода — предусловиечетвёртая компонента перехода — множествосбрасываемых таймеровНапоминаниеIATC (C ) — множество всех элементарных ограничений надтаймерами множества C: true, false и всевозможныевыражения вида x ./ k и x − y ./ k, гдеIIIx, y — таймерыk — целая неотрицательная константа./∈ {<, ≤, >, ≥, =, 6=}Iinv (C ) — множество всех формул, составленных надатомами true, x < k, x ≤ k и связкой &IALC (A) — множество всех выражений вида A.`, где ` —состояние автомата AНапоминаниеКонфигурация временного автомата (L, `0 , Σ, C , I , T ) — этопара (`, d), где ` ∈ L и d : C → R≥0 (d — оценка таймеров)Начальная конфигурация автомата — это пара (`0 , 0, 0, .

. . , 0)Шаг вычисления временного автомата — это изменениеконфигурации (`, d) на конфигурацию (`0 , d 0 ) одним из двухспособов:I продвижение времени:(`, d)→(`0 , d 0 )IIII`0 = `существует константа k ∈ R>0 , такая что d 0 = d + kd 0 |= I (`)изменение состояния:IIII(`, σ, g , C, `0 ) ∈ Td |= gd 0 = reset(d, C)d 0 |= I (`0 )(`, d)→(`0 , d 0 )НапоминаниеСеть временных автоматов — это система(C , Chan, (A1 , .

. . , Ak )), гдеIC — конечное множество общих таймеровIChan — конечное множество общих каналоввзаимодействияIAi = (Li , l0i , {ch!, ch? | ch ∈ Chan} , C , I i , T i ) — временнойавтомат над общими таймерами и общими каналамивзаимодействия (1 ≤ i ≤ k)НапоминаниеКонфигурация сети (C , Chan, (A1 , . . . , Ak )),Ai = (Li , `i0 , Σ, C , I i , T i ) — это система (`1 , .

. . , `k , d), где `i ∈ Liи d : C → R≥0Начальная конфигурация сети имеет вид (`10 , . . . , `k0 , 0, 0, . . . , 0)Шаг вычисления сети — это изменение конфигурации(`1 , . . . , `k , d) на конфигурацию (`01 , . . . , `0k , d 0 ) одним из трёхспособов:1. продвижение времени:III`01 = `1 , . . . , `0k = `kсуществует положительная действительная константа D,такая что d 0 = d + Dd 0 |= I 1 (`1 ) & . . . & I k (`k )НапоминаниеКонфигурация сети (C , Chan, (A1 , . .

. , Ak )),Ai = (Li , `i0 , Σ, C , I i , T i ) — это система (`1 , . . . , `k , d), где `i ∈ Liи d : C → R≥0Начальная конфигурация сети имеет вид (`10 , . . . , `k0 , 0, 0, . . . , 0)Шаг вычисления сети — это изменение конфигурации(`1 , . . . , `k , d) на конфигурацию (`01 , . . . , `0k , d 0 ) одним из трёхспособов:2. асинхронное изменение состояния автомата Ai :IIIII`0p = `p для p 6= i(`i , λ, g , C, `0i ) ∈ T id |= gd = reset(d 0 , C)d 0 |= I i (`0i )НапоминаниеКонфигурация сети (C , Chan, (A1 , . . .

, Ak )),Ai = (Li , `i0 , Σ, C , I i , T i ) — это система (`1 , . . . , `k , d), где `i ∈ Liи d : C → R≥0Начальная конфигурация сети имеет вид (`10 , . . . , `k0 , 0, 0, . . . , 0)Шаг вычисления сети — это изменение конфигурации(`1 , . . . , `k , d) на конфигурацию (`01 , . . . , `0k , d 0 ) одним из трёхспособов:3. синхронное изменение состояний автоматов Ai , Aj :IIIIII`0p = `p для p 6= i, p 6= j(`i , c!, g 0 , C 0 , `0i ) ∈ T i(`j , c?, g 00 , C 00 , `0j ) ∈ T jd |= g 0 & g 00d 0 = reset(d, C 0 ∪ C 00 )d 0 |= I i (`0i ) & I j (`0j )НапоминаниеБесконечная модель Крипке M(A) [M(N)] временного автоматаA [сети временных автоматов N] определяется так:Iсостояние модели — это конфигурацияIначальное состояние — это начальная конфигурацияIпереходами связаны пары конфигураций, образующих шагвычисленияIсостояния модели размечены истинными в этих состоянияхатомарными высказываниями множеств ATC (C ), ALC (A),где C — таймеры автомата A [ATC (C ), ALC (Ai ), где C —общие таймеры сети N и Ai — автоматы сети]Полагаем, что “справедливостью” исключаются конвергентныевычисления: бесконечное продвижение времени без сменсостояний и с конечной верхней временной границейНапоминаниеСинтаксис формул логики TCTL (Timed CTL) совпадает ссинтаксисом формул логики CTL без оператора X надмножеством атомарных высказываний модели Крипке автоматаили сетиСемантика TCTL-формул отличается тем, что смыслтемпоральных операторов адаптирован к работе системы вреальном времени в условиях дискретной модели КрипкеM |=TCTL ϕ: TCTL-формула ϕ выполнена в модели Крипке MЗадача model checking для (сетей) временныхавтоматовЗадача model checking для временных автоматов (MCTA)Для временного автомата A и TCTL-формулы ϕ проверитьсправедливость соотношенияM(A) |=TCTL ϕЗадача model checking для сетей временных автоматов(MCNTA)Для сети временных автоматов N и TCTL-формулы ϕпроверить справедливость соотношенияM(N) |=TCTL ϕА можно ли более сложную задачу MCNTA свести к болеепростой задаче MCTA?Трансляция сети временных автоматов вовременной автоматРассмотрим сеть временных автоматовN = (C , Chan, (A1 , .

. . , Am )), гдеAi = (Li , `i0 , {ch!, ch? | ch ∈ Chan} , C , I i , T i )Построим по ней такой временной автоматA(N) = (L, `0 , ∅, C , I , T ):IL = L1 × · · · × LmI`0 = (`10 , . . . , `m0)II (`1 , . . . , `m ) = I 1 (`1 ) & . . . & I m (`m )((`1 , . . . , `m ), λ, g , C, (`01 , . . . , `0m )) ∈ T тогда и только тогда,когда верно одно из условий:IIIдля какого-либо автомата Ai верно (`i , λ, g , C, `0i ) ∈ T i , и`p = `0p при p 6= iдля каких-либо автоматов Ai , Aj , i 6= j, верно(`i , c!, g1 , C1 , `0i ) ∈ T i и (`j , c?, g2 , C2 , `0j ) ∈ Tj ; `p = `0p приp∈/ {i, j}; g = g1 & g2 ; C = C1 ∪ C2Трансляция сети временных автоматов вовременной автоматПереразметим модель Крипке M(A(N)) автомата A(N)следующим образом: метку A.(`1 , .

. . , `m ) заменим на меткиA.`1 , . . . , A.`meПусть в результате получена бесконечная модель M(A(N))eУтверждение. M(N) = M(A(N))Упражнение. Строго докажите это утверждениеСледствие. M(N) |= ϕ⇔eM(A(N))|= ϕТак задачу MCNTA можно свести к задаче MCTAТрудность задачи MCTAЗадача о сумме подмножеств (СП)Даны натуральное число N и множество натуральных чиселS = {m1 , . . .

, mk }Выяснить, существует ли подмножество множества S, такоечто сумма чисел этого подмножества есть NУтверждение. Задача о сумме подмножеств NP-полнаРассмотрим такой временной автомат A с таймерами x, y :x = mk , xx = m3 , xx = m1 , xx = m2 , x...x = 0x = 0x = 0`x = 0 x ≤ 0Утверждение. Задача СП имеет решение ⇔M(A) |= EF(A.` & y = N)И что же это говорит о трудности задачи MCTA?Сжатие модели КрипкеАлгоритмы проверки CTL-формул на моделях Крипке неприменимы напрямую к решению задачи MCTA:Iмодель M(A) временного автомата A в общем случаебесконечнаIсемантика TCTL отличается от семантики CTLПопытаемся добиться того, чтобы алгоритмы стали применимыДля этого “сожмём” бесконечную модель временного автоматав конечную модель Крипке так, чтобы исходная TCTL-формулаоказалась равновыполнима с синтаксически совпадающейконечной CTL-формулойДля этого попытаемся объединить множество значенийтаймеров в конечное число классовСжатие модели КрипкеПримерx ≤ 1x = 1`2x`1x < 1, x`3x ≤ 0Бесконечная модель Крипке для этого автомата:`3 ,0∞`1 ,0∞`1 ,k∞∞`2 ,0∞`2 ,m∞Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`1 , 0Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`1 , 0`1 , (0, ∞)`2 , 0Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`1 , 0`1 , (0, ∞)`2 , 0Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`3 , 0`1 , 0`1 , (0, ∞)`2 , 0`2 , (0, 1]Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`3 , 0`1 , 0`1 , (0, ∞)`2 , 0`2 , (0, 1]Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`3 , 0`1 , 0`1 , (0, ∞)`2 , 0`2 , (0, 1]Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`3 , 0`1 , 0`1 , (0, ∞)`2 , 0`2 , (0, 1)`2 , 1Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`3 , 0`1 , 0`1 , (0, ∞)`2 , 0`2 , (0, 1)`2 , 1Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`3 , 0`1 , 0`1 , (0, ∞)`2 , 0`2 , (0, 1)`2 , 1Сжатие модели Крипкеx ≤ 1x = 1`2`1xx < 1, x`3x ≤ 0А можно ли для этого автомата построить конечную модельКрипке, достаточную для решения задачи MCTA хотя бы дляконкретного автомата и конкретной формулы?(пока что будем называть такую модель сжатием)`3 , 0`1 , 0`1 , (0, ∞)`2 , 0`2 , (0, 1)`2 , 1Подходит ли такая модель для наших целей?Сжатие модели Крипке`3 , 0`1 , 0`1 , (0, ∞)`2 , 0`2 , (0, 1)`2 , 1AG(A.`2 → A(x ≤ 1UA.`1 )): выполнена в бесконечной иконечной моделяхAG(A.`2 & x = 1 → A(x ≥ 1UA.`2 )): выполнена в бесконечноймодели; а в конечной?А как в этой модели разметить состояния атомарнымивысказываниями?Сжатие модели КрипкеЕсли размечать сжатие атомарными высказываниями“по-честному”, то возникает неоднозначность в разметкеэлементарными ограничениями таймеровНапример, если x ∈ (0, ∞), то неясно, верно ли в состоянии сэтим интервалом ограничение x ≥ 1При этом в некоторых состояниях необходимо знать, верно лиx ≥ 1, если проверяется формулаAG(A.`2 & x = 1 → A(x ≥ 1UA.`2 ))А значение ограничения x ≥ 2 абсолютно неважноИ какие же элементарные ограничения нам важны припостроении сжатия?Те, которые содержатся в проверяемой формуле ϕМножество таких ограничений будем обозначать записьюATC (ϕ)Осталось понять, какой именно вид должны иметь состояниясжатияЭквивалентность оценок таймеров, регионыЕсли временной автомат содержит n таймеров, товсевозможные значения таймеров образуют пространство R nПопытаемся разбить это пространство на конечное числоклассов эквивалентности так, чтобы можно былоIоднозначно пометить каждое состояние сжатиявысказываниями из ALC (A) ∪ ATC (ϕ)Iгарантировать, что дуги, исходящие из каждого состояниясжатия, в точности соответствуют дугам, исходящим изкаждого состояния исходной бесконечной модели,описываемого выбранным состоянием сжатияКогда такое отношение будет построено, достаточно будетобъявить пару, состоящую из состояния автомата и классаэквивалентности таймеров, состоянием сжатия и естественнымобразом расставить переходы моделиЭквивалентность оценок таймеров, регионыДалее считаем заданными временной автоматA = (L, `0 , ∅, C , I , T ) и TCTL-формулу ϕ, выполнимостькоторой проверяется в модели M(A)Для простоты технических выкладок считаем, что ни в A, ни вϕ не встречается выражений вида x − y ./ kПредположим, что в A или ϕ встречается выражение x ./ k,./∈ {<, ≤, >, ≥, =, 6=}Чтобы знать, верно ли это выражение при оценке таймеров d,достаточно знатьIцелую часть значения d(x): bd(x)cIимеет ли значение d(x) ненулевую дробную частьfrac(d(x))Эквивалентность оценок таймеров, регионыМожно попытаться ввести эквивалентность оценок таймеровтак: оценки d, d 0 эквивалентны, если для любого таймераx ∈ C верноIbd(x)c = bd 0 (x)c иIfrac(d(x)) = 0⇔frac(d(x)) = 0Тогда для эквивалентных оценок d, d 0 будет верно:d(x) ./ k ⇔ d 0 (x) ./ kЭквивалентность оценок таймеров, регионыПримерПредположим, что автомат содержит два таймера: x и yКлассы введённой только что эквивалентности этих таймеровбудут выглядеть так:(один класс — связный сегмент одного цвета)d(y )21012d(x)Эквивалентность оценок таймеров, регионыРассмотрим такую пару переходов автомата:y ≥ 1x ≥ 2Предположим, что текущее состояние сжатия — центральное, ичто текущий класс эквивалентности сжатия —{(x, y ) | 1 < x < 2, 0 < y < 1}В зависимости от выбора представителя классаэквивалентности при продвижении времени могут бытьполучены два существенно различных состояния:Iв одном возможно выполнения перехода влево, ноневозможно выполнение перехода вправоIв другом возможно выполнение перехода вправо, ноневозможно выполнение перехода влевоВ исходной модели Крипке такая ситуация невозможна, азначит, введённое отношение эквивалентности не подходит длясжатияЭквивалентность оценок таймеров, регионыd(y )21012d(x)Добавим в список условий, при выполнении которых оценки таймеров d, d 0 признаются эквивалентными, такое:Iдля любой пары таймеров x, y верно:frac(d(x)) ≤ frac(d(y )) ⇔ frac(d 0 (x)) ≤ frac(d 0 (y ))Это условие исключает “плохую” ситуацию, описанную вышеЭквивалентность оценок таймеров, регионыd(y )21012d(x)Такое отношение эквивалентности всё равно не подходит дляописания сжатия, так как число классов эквивалентностибесконечноПопытаемся объединить некоторые классы эквивалентности так,чтобы сделать число классов конечнымЭквивалентность оценок таймеров, регионыПусть kx — максимальная константа, встречающаяся ввыражениях A и ϕ вида x ./ kТогда если d(x) > kx , то каким бы ни было значение d(x), всевысказывания x ./ k в A и ϕ будут иметь одно и то же значениеОбъединим классы эквивалентности так: если d и d 0отличаются только значением x и при этом d(x) > kx иd 0 (x) > kx , то объявим d и d 0 эквивалентнымиТеперь можно подвести итог рассуждений и сформулироватьпонятие эквивалентности оценок таймеровЭквивалентность оценок таймеров, регионыОценки таймеров d, d 0 эквивалентны, если выполненыследующие условия:IIдля любого таймера x верно: d(x) > kx ⇔ d 0 (x) > kxдля любых таймеров x, y , таких что d(x) ≤ kx и d(y ) ≤ ky ,верно:IIIbd(x)c = bd 0 (x)cfrac(d(x)) = frac(d 0 (x))frac(d(x)) ≤ frac(d(y ))⇔frac(d 0 (x)) ≤ frac(d 0 (y ))Регионами оценок будем называть классы эквивалентностиоценок таймеров[d] — это регион, которому принадлежит dРегионами конфигураций будем называть пары (`, r ), где ` ∈ Lи r — это регион оценокЕсли d(x) > kx , то регион [d] будем называть открытым для x,в противном случае — закрытым для xЭквивалентность оценок таймеров, регионыПримерПусть автомат A содержит два таймера: x и y — и пусть kx = 2и ky = 1Тогда регионы оценок будут выглядеть так:d(y )21012d(x)Оценка числа регионовУтверждениеЧисло N попарно различных регионов оценок длявременного автомата A = (L, `0 , C , I , T ) и формулы ϕ,таких что kx ≥ 1 для каждого таймера x ∈ C , оцениваетсяснизу и сверхуQтакими константами: Q|C |! ·kx ≤ N ≤ |C |! · 2|C |−1 ·(2kx + 2)x∈Cx∈CДоказательство.Откуда берётсяQIkx : отношение эквивалентности содержит столькоx∈Cединичных кубов размерности |C |, таких что регионывнутри этих кубов закрыты для всех таймеровI|C |!: столькими способами можно определить порядокдробных частей таймеров регионаОценка числа регионовУтверждениеЧисло N попарно различных регионов оценок длявременного автомата A = (L, `0 , C , I , T ) и формулы ϕ,таких что kx ≥ 1 для каждого таймера x ∈ C , оцениваетсяснизу и сверхуQтакими константами: Q|C |! ·kx ≤ N ≤ |C |! · 2|C |−1 ·(2kx + 2)x∈Cx∈CДоказательство.Откуда берётсяI2|C |−1 : столькими способами для каждого порядка можновыбрать, какие из соседних в порядке дробных частейравныI2kx + 2: столькими способами можно выбрать диапазондопустимых значений таймера в регионеHОперации над регионамиЧтобы коротко описать сжатие, определим, как изменяютсярегионы оценок при продвижении времени и сбросе таймеровРассмотрим регион r , подмножество таймеров C и константу kРегион reset(r , C) состоит из всех оценок reset(d, C), где d ∈ rОткрытый регион — это регион, открытый для всех таймеровПродвижение региона r (succ(r )) определяется так:Iесли r — открытый регион, то значение succ(r ) = rIиначе succ(r ) — регион, отличный от r и такой что длялюбой содержащейся в нём оценки d 0 верно: d 0 = d + k,где d ∈ r , и любая оценка вида d + k 0 , 0 ≤ k 0 ≤ k,содержится либо в r , либо в succ(r )Операции над регионамиУтверждениеЕсли элементарное ограничение a, содержащееся вавтомате A или формуле ϕ, верно для какой-либо оценкиd региона r , построенного для A и ϕ, то оно верно длявсех оценок этого регионаДоказательство.Очевидно?Отсылая к этому утверждению, будем говорить, что формула ϕнад элементарными ограничениями, содержащимися в A и ϕ, ибулевыми связками верна в регионе r (r |= ϕ), если она вернадля любой оценки этого региона, и неверна в регионе (r 6|= ϕ)иначеРегионная модель КрипкеРегионная модель Крипке Mr (A, ϕ) для автоматаA = (L, `0 , ∅, I , T ) и TCTL-формулы ϕ определяется так:Iсостояния модели — это всевозможные регионыконфигурацийIначальное состояние модели состоит из начальногосостояния автомата и региона [(0, .