Лекция 7. Логика линейного времени (LTL). Использование LTL в Spin (1158560), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

Свойства, инвариантные к прореживанию •  Пусть φ – трасса некоторого вычисления над пропозициональными формулами P, –  по трассе можно определить, выполняется ли на ней темпоральная формула, n1 n 2 n 3ϕ=ϕ–  трассу можно записать в виде 1 ϕ 2 ϕ 3 ... , где значения пропозициональных формул на каждом интервале совпадают. •  Обозначим E(φ) набор всех трасс, отличающихся лишь значениями n1, n2, n3 (т.е. длиной интервалов) –  E(φ) называется расширением прореживания φ.

Расширение прореживания x = 1 p: (x == mutex)q: (x != y)(y==0) mutex++ prin‘ mutex-­‐-­‐ x = 0 x==1 x==1 x==1 x==1 x==1 x==0 x==0 bit x,y;y==0 y==0 y==0 y==0 y==0 y==0 byte mutex;y==0 active proctype A()mutex==0 mutex==0 mutex==0 mutex==1 mutex==1 mutex==0 mutex==0 {x = 1;(y == 0) ->mutex++;printf(“%d\n”, _pid);mutex--;x = 0}трасса φ трасса φ1∈E(φ) p !p !p p p !p p !q q q q q q !q p !p p !p p !q q q q !q Свойства, инвариантные к прореживанию •  Свойство φ, инвариантное к прореживанию, либо истинно для всех трасс из E(φ), либо ни для одной из них: ϕf → ∀v ∈ E (ϕ ), vf•  истинность такого свойства зависит от порядка, в котором пропозициональные формулы меняют свои значения, и не зависит от длины трассы; •  Теорема: все формулы LTL без оператора X инвариантны к прореживанию.

•  Более того, в рамках LTL без X можно описать все свойства, инвариантные к прореживанию. Связь между LTL и автоматами Бюхи (конструкциями never) Связь LTL с автоматами Бюхи •  Удобно проверять допустимость трасс для некоторого автомата Бюхи; •  Удобно описывать свойства правильности при помощи темпоральных формул; •  Что дальше? •  Теорема: Для всякой формулы LTL f существует автомат Бюхи, который допускает те и только те прогоны, которым соответствуют трассы, на которых выполнима f. •  Пример: формуле <>[]p соответствует автомат true s0 p s1 p Переход от LTL к автоматам •  Привести свойство правильности LTL к форме never языка Promela достаточно просто: нужно построить отрицание формулы LTL f и поместить его в тело never: –  f выполняется на всех вычислениях ⇔–  !f не выполняется ни на одном вычислении ⇔–  автомат {!f} не допускает ни одного прохода, полученного в результате синхронного выполнения с системой.

! 〈〉 [] p ≡ []![] p ≡ []〈〉! ptrue s0 !p true s1 Примеры !p||q •  p -> qtrue !p||q •  []p -> qtrue true !p true •  [](p -> q)!p||q Примеры true •  [](p -> <>q)!p||q !p •  [](p -> X<>q)!p&&q q q true !p&&p true q true true И, наконец… •  [](p -> X<>q)&&(<>p)true true !p&&q p p&&q true true q !p&&q !p p true true !p true •  &&(<>p)!p p true p true !p !q Отрицания формул LTL Формулу LTL всегда можно переписать в таком виде, что отрицания будут появляться только перед пропозициональными символами •  •   – по определению логической импликации •  <>!(!p || <>q) – ![]p эквивалентно <>!p •  <>(p && !<>q) – По правилу ДеМоргана •  <>(p && []!q) – !<>q эквивалентно []!q И, наконец… •  !([](p -> X<>q)&&(<>p))–  )||!<>p!p –  <>!(!p || (X<>q))||[]!pp true –  <>(p && !(X<>q))||[]!p–  <>(p &&true (X[]!q))||[]!p!p p !q Используем Spin для трансформации формул LTL > ./spin -f '<>[]p'never {/* <>[]p */T0_init:if:: ((p)) -> goto accept_S4:: (1) -> goto T0_initfi;accept_S4:if:: ((p)) -> goto accept_S4fi;}> ./spin -f `!<>[]p'never {/* !<>[]p */T0_init:if:: (! ((p))) -> gotoaccept_S9:: (1) -> goto T0_initfi;accept_S9:if:: (1) -> goto T0_initfi;}true T0_init true T0_init p !p true s4 s9 p Правила синтаксиса > ./spin -f `([]p -> <> (a+b <= c) )'#define q (a+b <= c)Вводим строчные макроопределения для всех булевых подформул > ./spin -f `[] (p -> <> q)'never {/* [] (p -> <> q) */T0_init:if:: (((! ((p))) || ((q)))) -> goto accept_S20:: (1) -> goto T0_S27fi;accept_S20:if:: (((! ((p))) || ((q)))) -> goto T0_init:: (1) -> goto T0_S27fi;accept_S27:if:: ((q)) -> goto T0_init:: (1) -> goto T0_S27fi;T0_S27:if:: ((q)) -> goto accept_S20:: (1) -> goto T0_S27:: ((q)) -> goto accept_S27fi;}Следим за приоритетом операторов LTL для проверки правильности при помощи Spin int x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}Ограничено ли значение x? > ./spin -f `[] (x > 0 && x <= 100)'tl_spin: expected ')', saw '>'tl_spin: [] (x > 0 && x <= 100)----------------^>Синтаксическая ошибка! LTL для проверки правильности при помощи Spin int x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}#define p (x > 0 && x <= 100)> ./spin -f `[] p'never {/* []p */accept_init:T0_init:if:: ((p)) -> goto T0_initfi;}p Формула синтаксически корректна, но мы же будем проверять её невыполнимость! LTL для проверки правильности при помощи Spin int x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}#define p (x > 0 && x <= 100)> ./spin -f `![] p'never {/* ![]p */T0_init:if:: (! ((p))) -> gotoaccept_all:: (1) -> goto T0_initfi;accept_all:skip}true !p true То, что ![]p не может быть выполнено, означает, что []p не может быть нарушено (нет ни одного контрпримера) LTL для проверки правильности при помощи Spin int x = 100;#define p (x > 0 && x <= 100)active proctype A(){do:: x%2 -> x = 3*x + 1od> ./spin -a ltl1.pml}> gcc -o pan pan.cactive proctype B()> ./pan -a(Spin Version 5.1.4 -- 27 January 2008){+ Partial Order ReductiondoFull statespace search for::: !x%2 -> x = x/2never claim+odassertion violations+ (if within scope of claim)}acceptancecycles+ (fairness disabled)never {/* ![]p */invalid end states- (disabled by never claim)T0_init:...if:: (! ((p))) -> goto accept_all:: (1) -> goto T0_initfi;accept_all:skip}Ещё один пример int x = 100;active proctype A(){do:: x%2 -> x = 3*x + 1od}active proctype B(){do:: !x%2 -> x = x/2od}Пусть #define p (x == 1)Выполнимо ли свойство []<>p? Даже в таком простом случае метод пристального взгляда перестаёт работать Для проверки неизбежности []<>pпроверяем невозможность ![]<>p<>!(<>p)<>[]!pLTL для проверки правильности при помощи Spin int x = 100;#define p (x == 1)> ./spin -t -c ltl2.pmlactive proctype A()proc 0 = Aproc 1 = B{Never claim moves to line 18[(!((x==1)))]do[(!((x==1)))]:: x%2 -> x = 3*x + 1 Never claim moves to line 23<<<<<START OF CYCLE>>>>>odspin: trail ends after 3 steps}------------active proctype B()final state:{------------#processes: 2dox = 100:: !x%2 -> x = x/23:proc 1 (B) line 11 "ltl2.pml" (state 3)od3:proc 0 (A) line5 "ltl2.pml" (state 3)}3:proc - (:never:) line 22 "ltl2.pml" (state 9)never {/* ![]<>p */ 2 processes createdT0_init:>if:: (! ((p))) -> goto accept_S4:: (1) -> goto T0_initfi;> ./spin -a ltl1.pml> gcc -a pan pan.caccept_S4:> ./pan -aifpan: acceptance cycle (at depth 2):: (! ((p))) -> goto accept_S4pan: wrote ltl2.pml.trailfi;Практические приёмы описания свойств на LTL Практические приёмы описания свойств на LTL •  Выполнимость формулы LTL проверяется только для первого состояния в трассе •  Темпоральные операторы управляют проверкой выполнимости своих аргументов •  Сложное свойство можно (и нужно!) строить как суперпозицию простых •  Суперпозиция темпоральных операторов не ограничивает диапазон действия «вложенного» оператора.

Выполнимость формул LTL •  Выполнимость формулы LTL определена и проверяется для одного (первого) состояния трассы •  Распространение свойств на другие состояния управляется темпоральными операторами •  Единственный оператор, который может ограничить сверху проверку выполнимости формулы – Un†l Суперпозиция формул LTL •  Составлять сложные формулы LTL нужно методом суперпозиции простых формул •  Внешняя формула задаёт, на каких участках вычислений будет проверятся подформула •  Подформула задаёт свойства, проверяемые для участков вычислений •  Суперпозиция темпоральных операторов не ограничивает диапазон действия «вложенного» оператора. Пример •  В ходе одного вызова функции F() x всегда не превышает 3.

где проверяем (g) что проверяем(f) •  φ = g(f) •  Что проверяем? –  f = x <= 3 – в синтаксисе LTL нет таких символов! – определяем пропозициональный символ–  f = []a – вроде бы точно описывает свойство f –  #define a x <= 3Пример •  В ходе одного вызова функции F() x всегда не превышает 3. где проверяем (g) что проверяем(f) •  φ = g(f) •  Где проверяем? –  #define lab_f P@f_call – поставим метку на вызов f – не то, проверяем для всего участка пути за первым вызовом F –  g = [](lab_f -> f)f_call f_entry f_return f_call f_entry f_return – нужно проверять свойство #define f_e P@f_return внутри тела функции –  g = [](f_b -> (f U f_e)) – похоже на правду, проверяем от входа в функцию до выхода из неё –  #define f_b P@f_entryПример •  В ходе одного вызова функции F() x всегда не превышает 3. где проверяем (g) что проверяем(f) •  φ = g(f) •  Подставляем одно в другое –  φ = [](f_b -> ([]a U f_e))f_b Проверяем выполнимость φ Проверка выполнимости U f_e Проверка выполнимости []a Проверка выполнимости a –  зона действия [] по определению не ограничивается Until! –  φ = [](f_b -> (a U f_e))– правильная формула Помощь в формулировке свойств База шаблонов темпоральной логики hŸp://paŸerns.

projects.cis.ksu.edu Логические паттерны (LTL/CTL/GIL) встречаемость (occurence) отсутствие (absense) порядок (order, sequence) универсальность (universality) существование (existence) bounded existence приоритет (precedence) chain precedence отклик (response) База шаблонов темпоральной логики hŸp://paŸerns. projects.cis.ksu.edu •  Для каждого шаблона – пять вариантов формул: имя пример для “absense” и LTL всегда [](!p) перед r <>r -> (!p U r)В чём разница? после q [](q -> [](!p)) между r и q []((r && !q && <>q) -> (!p U q)) после r до q []((r && !q) -> ((!p U q) || []!p))База шаблонов темпоральной логики hŸp://paŸerns.

projects.cis.ksu.edu •  Для каждого шаблона – пять вариантов формул: имя всегда перед r после q между r и q после r до q пример для “absense” и LTL r r q q q r r q r r r q r r Спасибо за внимание!Вопросы?.

Характеристики

Список файлов лекций