Лекция 5. Логика линейного времени (LTL) (Лекции)

НАДЁЖНОСТЬ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯЛекция 5:Логика линейного времени(LTL)ВМиК МГУ им. М.В. Ломоносова,Кафедра АСВК, Лаборатория Вычислительных КомплексовАссистент Волканов Д.Ю.1План лекции• Свойства безопасности и живучести• Логика линейного времени (LTL)• Свойства, инвариантные к прореживанию• Практические приёмы формулированиясвойств на LTLРассуждения о правильностипрограммы• Требования правильности задаются как утверждения овозможных или невозможных вариантах выполнениямодели,• рассуждения о вероятности не допускаются из соображенийстрогости доказательства;• Мы утверждаем, что некоторые варианты выполнениямодели• либо невозможны,• либо неизбежны;• Двойственность утверждений:• если что‐то неизбежно, то противоположное – невозможно,• если что‐то невозможно, то противоположное – неизбежно,• используя логику, можно переходить от одного к другому припомощи логического отрицания.Свойства безопасности и(автор – LeslieживучестиLamport)безопасность•«ничего плохогоникогда не произойдёт»;живучесть• пример: инвариант системы•«рано или позднопроизойдёт что‐тохорошее»;• пример: «отзывчивость»– (х всегда меньше y);–• задача верификатора – найтивычисления, которые ведут кнарушению свойствабезопасности (то «плохое»,которое никогда не должнопроизойти)если отправлен запрос,то рано или поздно будетсгенерирован ответ;• задача верификатора – найтивычисления, в которых это«хорошее» можетоткладываться добесконечностиНемного подробнее…• Свойства безопасности – самые простыесвойства («состояние, где истинно φ,недостижимо»).• Можно ли в рамках свойства безопасностисформулировать, что φ неизбежно?• «состояние, где истинно !φ, недостижимо»– не то, это слишком сильное свойство;• «состояние, где истинно φ, достижимо»– а это, наоборот, слишком слабое.Немного подробнее…• «φ неизбежно» – означает, что φобязательно достижимо;• для спецификации такой модальностии нужны свойства живучести.Классическая логика не можетописать утвержденияКлассическая логикаПримитивная модель истины: “черно-белая” модель, не существует степениуверенности-неуверенности, высказывания статичны, неизменны во времени неадекватна для высказываний о времениПример - (некоммутативность конъюнкции, A&B  B&A):“Джону стало страшно и он убил”  “Джон убил и ему стало страшно”“Джон умер и его похоронили” “Джона похоронили и он умер”“Джейн вышла замуж и родила ребенка”  “Джейн родила ребенка ивышла замуж”В обычной логике высказываний не формализуются:Путин – наш президент (истинно только в какой-то период)Мы не друзья, пока ты не извинишьсяЕсли m поступит на вход в канал, то потом m появится на выходеКаждый запрос к лифту c произвольного этажа, поступивший в любой моментвремени, будет когда-нибудь в будущем удовлетворенЭлементарные (атомарные) утверждения о событиях обычно истинны в одинмомент времени и ложны в другой!Утверждения о событиях, происходящих в разные моменты времени, нельзякорректно выразить в обычной логике7Темпоральная логикаОпределение TL - это любая логическая система, которая позволяет, невводя явно понятие времени, формализовать утверждения, истинностькоторых изменяется со временем.

Используется для описанияпоследовательностей явлений и их взаимосвязи и зависимости во времениПрименения TLФИЛОСОФИЯ: формализм для прояснения философских вопросов о времени;ЕСТЕСТВЕННЫЙ ЯЗЫК: формализм для определения семантики утверждений вестественных языках, включающих время;ИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ: язык для представления знаний, связанных современем (Д.

А. Поспелов (ред) "Представление знаний о времени и пространстве винтеллектуальных системах«, 1987);ТЕХНИКА: для формализации утверждений о свойствах будущего поведениятехнических систем (программ, оборудования, систем управления, …), для описания свойствих поведения во времени после того, как они будут запущеныМы будем рассматривать TL с точки зрения верификации ПО итехнических систем8Примеры темпоральных свойств• p всегда истинно;• p рано или поздно станет всегда ложным;• p всегда рано или поздно станет ложнымхотя бы ещё один раз;• p всегда ведёт к ¬q;• p всегда ведёт к тому, что рано илипоздно станет истинным q.Темпоральные свойства наестественном языке?• нет строгой семантики => возможно множествотрактовок• в части области проверки: «индикатор не горит» ‐ в начальномсостоянии? или это инвариант?• в темпоральной части:• попробуйте объяснить разницу: «от события А до события Б» и «междусобытиями А и Б»• «деньги выплачиваются, как только работа будет выполнена» ‐‐ требуется ливыполнение работы?• значение зависит от контекста:• если нажата кнопка, рано или поздно будет выпущено шасси• от взлёта и до посадки, если нажата кнопка, то рано или поздно будетвыпущено шасси (область проверки вложенного свойства изменилась)• после взлёта, если была нажата кнопка, то до посадки будет выпущеношасси (более строгая формулировка)• зависит от знания и понимания естественного языка,который сложнее LTL.Темпоральная логика LTL• Ясный, лаконичный и непротиворечивый способописания требований к программам;• В явном виде время не присутствует, однакорассуждения ведутся в терминах «никогда»,«всегда», «рано или поздно», которыепредставлены в виде темпоральных операторов.• Мы рассматриваем темпоральную логикулинейного времени – LTL.

С её помощью можноописывать свойства, которым должныудовлетворять линейные последовательностинаблюдаемых состояний – трассы.• LTL предложена Амиром Пнуэли (Amir Pnueli) вконце 70‐х.Формулы LTL• Могут использоваться для описания каксвойств живучести, так и безопасности• LTL = пропозициональная логика+ темпоральные операторы• Формула LTL f ::=• p, q, … ‐ свойства состояний, включая true иfalse,• ( f ) – группировка при помощи скобок,• α f – унарные операторы,• f1 β f2 – бинарные операторы.• Унарные:Операторы LTL• ☐([]) всегда (в будущем),• ◊(<>) рано или поздно,– (Х) в следующем состоянии,– ¬ (!) логическое отрицание;• Бинарные:≡(¬pq)• U (U) пока,• (&&) логическое И,≡(p→q)(q→p)• (||) логическое ИЛИ,• →(->) логическая импликация,– ↔(<->) логическая эквивалентность.•ВыполнимостьформулПоследовательность состояний прохода σs0 , s1, s2 , s3,...• Набор пропозициональных формул p, q:i,i  0, и p, определено sip• Семантика LTL:s0σfs0sisi[] ffsiXfj, j  i : s jj, j  i : s jsi1 fsisi+1fffСлабый и сильный un†lслабый: sieWfсильный: sieUfsif  (sij, j  i : s j(Spin)fиk,i  k  j : skesiee  si1 (eWf ))sjeeefПрактически важные следствияe W false  true U feWf[]e  f[]eeUfppps0pppsisi+Примерыppp1qqppsn‐sn1 | []p | ◊ p | []◊ p | []q | ◊ q | []◊ q | pUq  | [](pUq)  | [](pWq) | qUp  | [](qUp) | qWp  | []qWpppps0pppsisi+Примерыppp1qqppsn‐sn1 | []p | ◊ p | []◊ p | []q | ◊ q | []◊ q | pUq  | [](pUq)  | [](pWq) | qUp  | [](qUp) | qWp  | []qWpЦикличность истабильность• Свойством цикличности называется любаятемпоральная формула, котораяпредставима в виде ☐◊p, где p – формулана состоянии;• Свойством стабильности называетсялюбая темпоральная формула, котораяпредставима в виде ◊☐p, где p – формулана состоянии.Распространённые LTL‐формулыФормулаОписаниеТип[]pвсегда pинвариант> pрано или поздно pгарантияp  <> qесли p, то рано или поздно qоткликp  qUrесли p, то q, затем rприоритет[]<> pвсегда рано или поздно будет p>[]pрано или поздно всегда будет pцикличность(прогресс)стабильность(бездействие)корреляция> p  <> q если рано или поздноp, то рано или поздно qЭквивалентные преобразованияПримеры темпоральных свойств[]p<>[]!p• p всегда истинно;• p рано или поздно станет всегда ложным;• p всегда рано или поздно станет ложным хотябы ещё один раз;• p всегда ведёт к ¬q;[](p->!q)[]<>!p• p всегда ведёт к тому, что рано или поздностанет истинным q.[](p-> <>q)Правильная интерпретацияформул LTLLTL: >b1  !b2Ub2   []!a31.Пусть b1 всегда ложно,p→q означает, что !pq;формула выполняется.!b1время2.Пусть b1 стало истинно,b1!b2b2формула выполняется.3.4.Пусть b1 стало истинно,затем – b2, однако a3всегда ложно; формулавыполняется.Пусть b1 стало истинно,затем – b2, затем –a3; формула невыполняется.b1время!b2!a3b2b1времяa3!b2!a3времяПравильная интерпретацияформул LTLLTL:1.2.3.>b1  >b2 Пусть b1 и b2 всегдаложно; формулавыполняется.Пусть и b1, и b2становятсяистинными; формулавыполняется.Пусть b1 становитсяистинным, но b2всегда ложно;формула невыполняется.!b1времяb2b1!b2время!b1b1!b1!b2времяПравильная интерпретацияформул LTLLTL: [] >b1  >b2 1.2.3.Пусть b1 и b2 всегдаложно; формулавыполняется.Пусть и b1, и b2бесконечночередуются; формулавыполняется.Пусть b2 становитсяистинным толькоодин раз; формулане выполняется.!b1время!b2b1b2!b1b1!b2!b1!b2b2!b1!b1время!b2b1b2!b1b1!b2!b1!b2времяОписание требований припомощи LTL“p приведёт к q”• p ‐> q• нет темпоральных операторов, т.е.

применяетсятолько к первому состоянию;• выполняется только если !pq в первомсостоянии, остальная трасса не рассматривается;• не подходит;• нужно использовать темпоральные операторы.Описание требований припомощи LTL“p приведёт к q”• [] p ‐> q–правила приоритета! [] применяется только к p;–означает ([]p) ‐> q;–не подходит;–нужно расставить скобки.Описание требований припомощи LTL“p приведёт к q”• [] (p ‐> q)–проверяем условие во всех состояниях, нопричинно‐следственная связь между p и q отсутствует;–выполняется, только если! pq во всехсостояниях;–не подходит;–нужно описать, что p является причиной q.Описание требований припомощи LTL“p приведёт к q”• [] (p ‐> <>q)–уже лучше;–тем не менее, формула выполнима, если q становитсяистинным в том же состоянии, что и p –причинно‐следственная связь отсутствует;–не подходит;–нужно описать, что q не может произойти раньшеследующего шага после p.Описание требований припомощи LTL“p приведёт к q”• [] (p ‐> X(<>q))–практически то, что нужно;–формула выполнима, если p всегда ложно;–возможно, не подходит;–нужно описать, что p обязательно произойдёт иприведёт к q.Описание требований припомощи LTL“p приведёт к q”• [] (p ‐> X(<>q)) && (<>p)–скорее всего, мы имели ввиду именно это;–несколько отличается от первоначального p‐>q;–LTL позволяет выразить множество различныхоттенков свойства;–подойдёт ли такое свойство для моделипараллельной программы?Оператор neXt• Оператор X нужно использовать аккуратно:• с его помощью делается утверждение овыполнимости формулы на непосредственныхпотомках текущего состояния;• в распределённых системах значение оператора Хнеочевидно;• поскольку алгоритм планирования процессовнеизвестен, не стоит формулироватьспецификацию в предположении о том, какоесостояние будет следующим;• стоит ограничиться предположением осправедливости планирования.Свойства, инвариантные кпрореживанию• Пусть φ – трасса некоторого вычислениянад пропозициональными формулами P,– по трассе можно определить, выполняется ли наней темпоральная формула,n1 n 2 n 3– трассу можно записать в виде  1 2 3 ...