8 - Логика линейного времени (LTL) (1161372), страница 2

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

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

,где значения пропозициональных формул накаждом интервале совпадают.• Обозначим E(φ) набор всех трасс,отличающихся лишь значениями n1, n2, n3(т.е. длиной интервалов)– E(φ) называется расширением прореживания φ.Расширение прореживанияx=1p: (x == mutex)q: (x != y)x==0bit x,y;byte mutex;y==0active proctype A()mutex==0{x = 1;(y == 0) ->mutex++;printf(“%d\n”, _pid);mutex--;x = 0}трасса φтрасса φ1 E(φ)(y==0) mutex++printfmutex--x==1y==0mutex==0x==1y==0mutex==0x==1x==1y==0y==0mutex==1 mutex==1p!p!pp!qqqqp!pp!pp!qqqq!qx=0x==1y==0mutex==0x==0y==0mutex==0p!ppqq!qСвойства, инвариантные кпрореживанию• Свойство φ, инвариантное к прореживанию, либоистинно для всех трасс из E(φ), либо ни для однойиз них:f  v  E ( ), vf• истинность такого свойства зависит от порядка, вкотором пропозициональные формулы меняютсвои значения, и не зависит от длины трассы;• Теорема: все формулы LTL без оператора Xинвариантны к прореживанию.• Более того, в рамках LTL без X можно описать всесвойства, инвариантные к прореживанию.Связь между LTLиавтоматами Бюхи(конструкциями never)Связь LTL с автоматами Бюхи• Удобно проверять допустимость трасс длянекоторого автомата Бюхи;• Удобно описывать свойства правильности припомощи темпоральных формул;• Что дальше?• Теорема: Для всякой формулы LTL f существуетавтомат Бюхи, который допускает те и толькоте прогоны, которым соответствуют трассы, накоторых выполнима f.• Пример: формуле <>[]p соответствуетавтоматtrues0ps1pПереход от LTL к автоматам• Привести свойство правильности LTL к форме neverязыка Promela достаточно просто: нужно построитьотрицание формулы LTL f и поместить его в телоnever:– f выполняется на всех вычислениях – !f не выполняется ни на одном вычислении – автомат {!f} не допускает ни одного прохода,полученного в результате синхронного выполнения ссистемой.![] p  []![] p  []! ptrues0!ptrues1Примеры!p||q• p -> qtrue!p||q• []p -> qtruetrue!ptrue• [](p -> q)!p||qПримерыtrue• [](p -> <>q)true!p||q!pqtruetrue• [](p -> X<>q)!p&&qq!p&&ptrueqИ, наконец…• [](p -> X<>q)&&(<>p)true!p&&qptruep&&qtruetrueq !p&&q !pptrue!ptruetrue!p• &&(<>p)ptrueptrue!p!qОтрицания формул LTLФормулу LTL всегда можно переписать в таком виде,что отрицания будут появляться только передпропозициональными символами• •  – по определению логической импликации• <>!(!p || <>q) – ![]p эквивалентно <>!p• <>(p && !<>q) – По правилу ДеМоргана• <>(p && []!q) – !<>q эквивалентно []!qИ, наконец…• !([](p -> X<>q)&&(<>p))– )||!<>p!p– <>!(!p || (X<>q))||[]!pptrue– <>(p && !(X<>q))||[]!p– <>(p &&true(X[]!q))||[]!p!pp!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_initps4!ptrue T0_inittrues9pПравила синтаксиса> ./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 для проверки правильности припомощи Spinint 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 для проверки правильности припомощи Spinint 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 для проверки правильности припомощи Spinint 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!ptrueТо, что ![]p не может быть выполнено,означает, что []p не может бытьнарушено (нет ни одного контрпримера)LTL для проверки правильности припомощи Spinint 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)do+ Partial Order Reduction:: !x%2 -> x = x/2Full statespace search for:never 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 для проверки правильности припомощи Spinint 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;accept_S4:> ./spin -a ltl1.pmlif> gcc -a pan pan.c:: (! ((p))) -> goto accept_S4> ./pan -apan: acceptance cycle (at depth 2)fi;pan: wrote ltl2.pml.trail}Практические приёмыописания свойств на LTLПрактические приёмы описаниясвойств на LTL• Выполнимость формулы LTL проверяетсятолько для первого состояния в трассе• Темпоральные операторы управляютпроверкой выполнимости своих аргументов• Сложное свойство можно (и нужно!)строить как суперпозицию простых• Суперпозиция темпоральных операторовне ограничивает диапазон действия«вложенного» оператора.Выполнимость формул LTL• Выполнимость формулы LTL определена ипроверяется для одного (первого)состояния трассы• Распространение свойств на другиесостояния управляется темпоральнымиоператорами• Единственный оператор, который можетограничить сверху проверку выполнимостиформулы – UntilСуперпозиция формул LTL• Составлять сложные формулы LTL нужнометодом суперпозиции простых формул• Внешняя формула задаёт, на каких участкахвычислений будет проверятся подформула• Подформула задаёт свойства, проверяемыедля участков вычислений• Суперпозиция темпоральных операторовне ограничивает диапазон действия«вложенного» оператора.Пример• В ходе одного вызова функции F() x всегда не превышает 3.где проверяем (g)что проверяем(f)• φ = g(f)• Что проверяем?– в синтаксисе LTL нет таких символов!#define a x <= 3 – определяемпропозициональный символf = []a – вроде бы точно описывает свойство f– f = x <= 3––Пример• В ходе одного вызова функции F() x всегда не превышает 3.где проверяем (g)что проверяем(f)• φ = g(f)• Где проверяем?– #define lab_f P@f_call – поставим метку на вызов– g = [](lab_f -> f) – не то, проверяем для всегоучастка пути за первым вызовом Ff_call f_entryf_return– #define f_b P@f_entryf_call f_entryf_return– нужно проверять свойство#define f_e P@f_return внутри тела функции– g = [](f_b -> (f U f_e)) – похоже на правду,проверяем от входа в функцию до выхода из неёfПример• В ходе одного вызова функции F() x всегда не превышает 3.где проверяем (g)что проверяем(f)• φ = g(f)• Подставляем одно в другое– φ = [](f_b -> ([]a U f_e))f_bПроверяемвыполнимость φПроверкавыполнимости Uf_eПроверкавыполнимости []aПроверкавыполнимости a– зона действия [] по определению не ограничивается Until!– φ = [](f_b -> (a U f_e))– правильная формулаПомощь в формулировке свойствБаза шаблонов темпоральной логикиhttp://patterns.

projects.cis.ksu.eduЛогические паттерны (LTL/CTL/GIL)встречаемость(occurence)отсутствие(absense)порядок(order, sequence)универсальность(universality)существование(existence)boundedexistenceприоритет(precedence)chainprecedenceотклик(response)База шаблонов темпоральной логикиhttp://patterns. 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))В чём разница?База шаблонов темпоральной логикиhttp://patterns. projects.cis.ksu.edu• Для каждого шаблона – пять вариантов формул:имяпример для “absense” и LTLвсегдаrrqqqперед rпосле qrrqrrrqrмежду r и qпосле r до qrСпасибо за внимание!Вопросы?.

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

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