Ещё одни лекции В.А. Захарова, страница 37

формула ϕ приводится к позитивной форме ϕ1 ,2. для формулы ϕ1 строятсямножество подформул Фишера–Ладнера FLSubϕ1 ,множество Next-подформул XSubϕ1 ,множество U-подформул FLSubϕ1 ,совокупность Conϕ1 всех возможных согласованныхмножеств подформул Фишера–Ладнера.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИМОДЕЛЕЙ ПРОГРАММСистемой Хинтикки для формулы PLTL ϕ1 и LTS Mназывается раскрашенный ориентированный графGϕ1 ,M = (V , E ) с множеством вершин V и множеством дуг E ,которые устроены так:V = {(s, B) : s ∈ S, B ∈ Conϕ1 , ρ(s) = B ∩ AP},т.

е. вершинами графа являются всевозможные пары(состояние s, согласованное множество B),для которых разметка ρ(s) состояния s подтверждаетистинность всех атомарных высказываний множества B;E= {(s , B ), (s , B ) : s −→ s и для любой Next-подформулы Xψ, Xψ ∈ XSubϕ1 ,верно Xψ ∈ B ⇐⇒ ψ ∈ B },т. е. дугами графа являются все такие переходы LTS M,которые позволяют подтвердить все обещания Xψ выполнитьψ в следующий момент времени.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИТеперь проведем раскраску вершин графа Γϕ1 ,M = (V , E ).Рассмотрим множество (Until-Release)-подформулURSubϕ1 = {χ1 Uχ1 , . .

. , χk Uχk , χk+1 Rχk+1 , . . . , χk+m Rχk+m }.Каждой формуле ψi из множества URSubϕ1 сопоставиминдивидуальный цвет i.Раскрасим в цвет i все вершины (s, B), для которых выполненохотя бы одно из двух условийв случае, когда ψi = χi Uχi :1) χi ∈ B,2) X(χi Uχi ) ∈/ B.в случае, когда ψi = χi Rχi :1) χi ∈/ B,2) X(χi Rχi ) ∈ B.Бесконечный маршрут(si1 , Bi1 ), (si2 , Bi2 ), .

. . , (sin , Bin ), . . .в графе Γϕ1 ,M назовем радужным, если в нем бесконечно частовстречаются вершины каждого цвета 1, 2, . . . , k.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИОсновная теоремаДля любой формулы PLTL ϕ1 в позитивной форме и LTSM = AP, S, S0 , −→, ρM |= ϕ1в графе Γϕ1 ,M существует хотя бы один радужный маршрут,исходящий из вершины v0 = (s0 , B0 ), в которой s0 ∈ S0 иϕ1 ∈/ B0 .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДоказательство.(⇑) Предположим, что в графе Γϕ1 ,M есть радужный маршрут(s0 , B0 ), (s1 , B1 ), .

. . , (sn , Bn ), (sn+1 , Bn+1 ), . . ./ B0 .указанного вида, в котором ϕ1 ∈Тогда согласно определению системы Хинтикки Γϕ1 ,M в LTS Mесть начальная трассаtr |0 |= B0tr = ys0tr |1 |= B1tr |2 |= B2- y- ys1s2- r r rtr |n |= Bn- ysntr |n+1 |= Bn+1- y- r r rsn+1Покажем, что для любой формулы ψ, ψ ∈ FLSubϕ1 , и длялюбого n, n ≥ 0, верноtr |n |= ψ ⇐⇒ ψ ∈ Bn .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДоказательство.Если удастся показать, чтоtr |n |= ψ ⇐⇒ ψ ∈ Bn(∗)/ B0 , придем к заключению tr |= ϕ1 .то, учитывая ϕ1 ∈Для доказательства соотношения (∗) воспользуемся индукциейпо числу связок в формуле ψ.Базис индукции. p ∈ AP.p ∈ Bn ⇐⇒ p ∈ ξ(sn ) ⇐⇒ tr |n |= p ./ Bn ⇐⇒ p ∈/ ξ(sn ) ⇐⇒ tr |n |= p ⇐⇒ tr |n |= ¬p.¬p ∈ Bn ⇐⇒ p ∈ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДоказательство.Индуктивный переход.1.

Логические связки & и ∨.ψ1 &ψ2 ∈ Bn ⇐⇒ ψ1 ∈ Bn и ψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 и tr |n |= ψ1⇐⇒ tr |n |= ψ1 &ψ1 .2. Темпоральный оператор X.Xψ ∈ Bn ⇐⇒ ψ ∈ Bn+1 ⇐⇒ tr |n+1 |= ψ ∈ Bn+1 ⇐⇒ tr |n |= Xψ.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.3. Темпоральный оператор R.3.1. Покажем ψ1 Rψ2 ∈ Bn =⇒ tr |n |= ψ1 Rψ2 .Заметим, что согласно определению согласованного множестваψ1 Rψ2 ∈ B ⇐⇒ ψ2 ∈ B и при этом ψ1 ∈ B или X(ψ1 Rψ2 ) ∈ B.Пусть ψ1 Rψ2 ∈ Bn .

Тогда возможны 2 случая.Вариант 1. X(ψ1 Rψ2 ) ∈ Bn+i для любого i, i ≥ 0.Тогда по определению Γϕ1 ,M в каждом множестве Bn+i , i ≥ 0,содержится формула ψ1 Rψ2 и, следовательно, ψ2 ∈ Bn+i .Тогда по индуктивному предположению tr |n+i |= ψ2 для любогоi, i ≥ 0.

Следовательно, tr |n |= ψ1 Rψ2 .rrrtr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1- yn+2- ytr |n+i |= ψ2- yn+i-r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход./ Bn+k для некоторого k, k ≥ 0.Вариант 2. X(ψ1 Rψ2 ) ∈/ Bn+k0 ноТогда существует такое k0 , что X(ψ1 Rψ2 ) ∈X(ψ1 Rψ2 ) ∈ Bn+i для любого i, 0 ≤ i < k0 .Тогда по определению графа Γϕ1 ,M в каждом множестве Bn+i ,0 ≤ i ≤ k0 , содержится формула ψ1 Rψ2 .Тогда по определению согласованных множеств ψ2 ∈ Bn+i длялюбого i, 0 ≤ i ≤ k0 , и, кроме того, ψ1 ∈ Bn+k0 .Тогда по индуктивному предположению tr |n+i |= ψ2 для любого0 ≤ i ≤ k0 и tr |n+k0 |= ψ1 . Значит, tr |n |= ψ1 Rψ2 .rrrtr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k0 −1 |= ψ2- yn+2- ytr |n+k0 |= ψ1tr |n+k0 |= ψ2- y-n+kИтак, в обоих случаях ψ1 Rψ2 ∈ Bn =⇒ tr |n |= ψ1 Rψ2 .r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход./ Bn =⇒ tr |n |= ψ1 Rψ2 .3.2.

Покажем ψ1 Rψ2 ∈/ Bn . Т. к. ψ1 Rψ2 ∈ URSubϕ1 этой формулеПусть ψ1 Rψ2 ∈соответствует некоторый цвет j.Поскольку рассматриваемый маршрут(s0 , B0 ), (s1 , B1 ), . . . , (sn , Bn ), (sn+1 , Bn+1 ), . . .является радужным, то вершины, окрашенные в цвет j,встречаются в этом маршруте бесконечно часто.Значит, существует такое k, k ≥ 0, что вершина (sn+k , Bn+k ) —первая, окрашенная в цвет j вершина, следующая в этомрадужном маршруте вслед за вершиной (sn , Bn ).Имеются две причины, по которым вершина (sn+k , Bn+k )оказалась окрашенной в цвет j: ψ2 ∈/ Bn+k , X(ψ1 Rψ2 ) ∈ Bn+k ,Рассмотрим каждый из этих случаев по отдельности.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Вариант 1. ψ2 ∈/ Bn+k .Т.

к. все вершины (sn+i , Bn+i ), 0 ≤ i < k не окрашены в цвет j,для каждого из множеств Bn+i , 0 ≤ i < k, верны соотношенияψ2 ∈ Bn+iиX(ψ1 Rψ2 ) ∈/ Bn+i .Тогда по определению графа Γϕ1 ,M для каждого множества/ Bn+i . А отсюдаBn+i , 0 ≤ i < k, верно соотношение ψ1 Rψ2 ∈следует, что ψ1 ∈/ Bn+i для любого i, 0 ≤ i < k.Тогда по индуктивному предположениюtr |n+i |= ψ2 и tr |n+i |= ψ1 для любого i, 0 ≤ i < k,tr |n+k |= ψ2 .rrrtr |n |= ψ1 tr |n+1 |= ψ1tr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k−1 |= ψ1tr |n+k−1 |= ψ2- y- yn+2А это означает, что tr |n |= ψ1 Rψ2 .tr |n+k |= ψ2- yn+k-r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход.Вариант 2.

X(ψ1 Rψ2 ) ∈ Bn+k .Т. к. все вершины (sn+i , Bn+i ), 0 ≤ i < k не окрашены в цвет j,для каждого из множеств Bn+i , 0 ≤ i < k, верны соотношенияψ2 ∈ Bn+iиX(ψ1 Rψ2 ) ∈/ Bn+i .Тогда по определению графа Γϕ1 ,M для каждого множества/ Bn+i . А отсюдаBn+i , 0 ≤ i ≤ k, верно соотношение ψ1 Rψ2 ∈/ Bn+i для любого i, 0 ≤ i < k и ψ2 ∈/ Bn+k .следует, что ψ1 ∈Тогда по индуктивному предположениюtr |n+i |= ψ2 и tr |n+i |= ψ1 для любого i, 0 ≤ i < k,tr |n+k |= ψ2 .rrrtr |n |= ψ1 tr |n+1 |= ψ1tr |n |= ψ2 tr |n+1 |= ψ2- yn- yn+1tr |n+k−1 |= ψ1tr |n+k−1 |= ψ2- y- yn+2И во втором случае tr |n |= ψ1 Rψ2 .tr |n+k |= ψ2- yn+k-r r rТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИИндуктивный переход./ Bn , то tr |n |= ψ1 Rψ2 .Таким образом, если ψ1 Rψ2 ∈В итоге, для любой формулы вида ψ1 Rψ2 и для любойвершины (sn , Bn ) нашего радужного маршрута верносоотношениеψ1 Rψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 Rψ2 .4.

Темпоральный оператор U.Для доказательства соотношенияψ1 Rψ2 ∈ Bn ⇐⇒ tr |n |= ψ1 Rψ2применяются рассуждения, аналогичные тем, которые былииспользованы для исследования оператора R.Самостоятельно.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИЗавершив обоснование индуктивного перехода, мы тем самымзавершили доказательство первой части теоремы:M |= ϕ1⇑в графе Γϕ1 ,M существует хотя бы один радужный маршрут,исходящий из вершины v0 = (s0 , B0 ), в которой s0 ∈ S0 иϕ1 ∈/ B0 .Покажем, что в том случае, когда имеет место M |= ϕ1 , вграфе Γϕ1 ,M из некоторой вершины v0 = (s0 , B0 ), в которойs0 ∈ S0 и ϕ1 ∈/ B0 , исходит хотя бы один радужный маршрут.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИПусть M |= ϕ1 . Тогда в LTS M существует такая начальнаятрасса tr , для которой tr |= ϕ1 .

Рассмотрим эту трассу tr .Для каждого i, i ≥ 0, положимBi = {ψ : ψ ∈ FLSubϕ1 , tr |i |= ψ .}Согласно утверждению 4, все построенные множества Biявляются согласованными.Покажем, что последовательность пар(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . .

. , (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .образует искомый радужный маршрут в графе Γϕ1 .ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИДействительно,1. Для любого n, n ≥ 0, верно tr [n] −→ tr [n + 1], поскольку tr— маршрут в LTS M.2. Для любого n, n ≥ 0 и для любой формулы Xψ ∈ XSubϕ1 ,верноXψ ∈ Bn ⇐⇒ ψ ∈ Bn+1посколькуXψ ∈ Bn ⇐⇒ tr |n |= Xψ ⇐⇒ tr |n+1 |= ψ ⇐⇒ ψ ∈ Bn+1 .3.

tr [0] ∈ S0 (т. к. tr — начальная трасса в M) и ϕ1 ∈/ B0 (т. к.tr |0 |= ϕ1 ).Значит, последовательность(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .является маршрутом в графе Γϕ1 ,M , исходящим из нужнойвершины.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИ4. Осталось показать, что маршрут(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .является радужным.Рассмотрим произвольное число n, n ≥ 0 и произвольнуюформулу ψi ∈ URSubϕ1 .

Покажем, что существует такоеk, k ≥ 0, что вершина (tr [n + k], Bn+k ) окрашена в цвет i.ТАБЛИЧНЫЙ МЕТОД ВЕРИФИКАЦИИОграничимся рассмотрением Until-формулы ψi = χ Uχ2 .(Для формул вида ψi = χ Rχ2 доказательство проведитесамостоятельно. )/ Bn , и,1. Если tr |n |= X(χ1 Uχ2 ), то X(χ1 Uχ2 ) ∈следовательно, вершина (tr [n], Bn ) окрашена в цвет j.2. А если tr |n |= X(χ1 Uχ2 ), то tr |n+1 |= χ1 Uχ2 . Тогдасуществует такое k, k ≥ 1, что tr |n+k |= χ2 . Поэтомуχ2 ∈ Bn+k , и вершина (tr [n + k], Bn+k ) окрашена в цвет j.Таким образом, вершины цвета j встречаются в нашеммаршруте бесконечно часто. Поскольку ψi была произвольной(Until-Release)-формулой, это означает, что наш маршрут вграфе Γϕ1 ,M является радужным.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММНо как проверить, что из заданной вершины в графе Γϕ1 ,Mне исходит ни одного радужного маршрута?Ориентированный граф Γ называется сильно связным , еслидля любой пары вершин v и u в графе Γ существует маршрутиз v в u и маршрут из u в v .Всякий максимальный сильно связный подграф графа Γназывается компонентой сильной связности .Компоненту сильной связности графа (системы Хинтикки)Γϕ1 ,M будем называть радужной, если в ней содержатсявершины всех цветов.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММТеорема.Из вершины v в графе Γϕ1 ,M исходит радужный маршрут тогдаи только тогда, когда существует маршрут , ведущий извершины v хотя бы в одну из вершин хотя бы одной радужнойкомпоненты сильной связности.Доказательство.Самостоятельно.

Здесь все очевидно.АЛГОРИТМ ВЕРИФИКАЦИИ МОДЕЛЕЙПРОГРАММИсходные данные: формула PLTL ϕ и LTSM = AP, S, S0 , −→, ρ.1. Построить равносильную позитивную форму ϕ1 .2. Построить систему Хинтикки Γϕ1 ,M .3. Выделить множество подформул URSubϕ1 и раскраситьвершины графа Γϕ1 ,M .4. Выделить радужные компоненты сильной связности вграфе Γϕ1 ,M .5.