18-19. Интуиционистская логика. Модальные логики (В.А. Захаров - Лекции), страница 2

. . , Pn , . . . } — множество атомарныхформул (элементарные высказывания).Модальная интерпретация или модель Крипке — этореляционная система I = hW , R, ξi, в которой1. W 6= ∅ — множество состояний (возможные миры);2. R ⊆ S × S — отношение достижимости на W ,3. ξ : W × P → {true, false} — оценка атомарных формул.Система hW , Ri называется шкалой Крипке (frame).Если (w , w 0 ) ∈ R, то возможный мир w 0 называетсяальтернативным миром для s.МОДАЛЬНЫЕ ЛОГИКИОтношение выполнимости для модальных формулПусть I = hW , R, ξi — модель Крипке.

Тогда отношениевыполнимости I , s |= ϕ формулы ϕ в мире s модели Iопределяется так:1. если ϕ = P ∈ P, то I , s |= ϕ ⇐⇒ ξ(w , P) = true;2. I , w |= ϕ1 &ϕ2 ⇐⇒ I , w |= ϕ1 и I , w |= ϕ2 ;3. I , w |= ϕ1 ∨ ϕ2 ⇐⇒ I , w |= ϕ1 или I , w |= ϕ2 ;4. I , w |= ϕ1 → ϕ2 ⇐⇒ I , w 6|= ϕ1 или I , w |= ϕ2 ;5. I , w |= ¬ϕ1 ⇐⇒ I , w 6|= ϕ1 ;6. I , w |= ϕ ⇐⇒для любого альтернативного мира w 0если hw , w 0 i ∈ R, то I , w 0 |= ϕ;7.

I , w |= ♦ϕ ⇐⇒cуществует такой альтернативный мир w 0 ,что hw , w 0 i ∈ R и I , w 0 |= ϕ.МОДАЛЬНЫЕ ЛОГИКИПримерМодель КрипкеI , w1 |= ♦pp = truew1 yI , w1 6|= pI , w1 |= ♦pI , w5 |= pI , w5 6|= ♦pw4p = false- yw2H 6 HHHI@6@@@@@@@@@@@@@@@@?R?@yyw3-p = falsep = trueHHHw5HHj yp = falseМОДАЛЬНЫЕ ЛОГИКИПростейшие свойства1.

|= ♦ϕ ≡ ¬¬ϕ;2. |= (ϕ1 → ϕ2 ) → (ϕ1 → ϕ2 );3. |= ϕ =⇒ |= ϕ (правило необходимости).В разных приложениях модальность необходимого можетпониматься по разному. Отсюда большое разнообразиемодальных логик. В разных модальных логиках отношениевыполнимости определяется на разных классах шкал. Каждаяразновидность шкал (отношения достижимости R)характеризуется определенным законом (формулой) модальнойлогики.МОДАЛЬНЫЕ ЛОГИКИХарактеристические формулы1. ϕ → ϕрефлексивные шкалы∀w R(w , w );2.

ϕ → ϕтранзитивные шкалы∀w1 ∀w2 ∀w3 (R(w1 , w2 )&R(w2 , w3 ) → R(w1 , w3 ));3. ♦ϕ → ϕсимметричные шкалы∀w1 ∀w2 (R(w1 , w2 ) → R(w2 , w1 )).Рассмотрим некоторые разновидности модальных логик,которые используются информатике.МОДАЛЬНЫЕ ЛОГИКИЭпистемические логики и мультагентные системыЭпистемические логики — это разновидности модальных логик,изучающие модальности знания и мнения (веры)идеализированных агентов. Интерес представляют вопросы отом, какими знаниям располагает субъект, насколько оносознает свои знания (и незнания), и какиепричинно-следственные связи возникают междуутверждениями, касающимися вопросов знания и веры.В эпистемической логике модальный оператор ϕ следуетпрочитывать «Я знаю, что ϕ», а ♦ϕ — «Я допускаю, что ϕ».МОДАЛЬНЫЕ ЛОГИКИЭпистемические логики и мультагентные системыОсновные законы (аксимы) эпистемической логики:1.

Аксиома адекватности знания:«Мои знания верны».ϕ → ϕ2. Аксиома позитивной интроспекции: ϕ → ϕ«Я вполне представляю все, что мне известно».3. Аксиома негативной интроспекции: ♦ϕ → ϕ«Я вполне сознаю, что именно мне неизвестно».Но чаще всего возникают задачи, когда коллектив субъектов(мультиагентная система) пытается совместными усилиямиили в конкурентной борьбе достичь какой-то цели. В такомслучае каждый агент должен принимать в расчет не толькознания о предметной области, но и представления о том,какими знаниями располагают другие агенты.МОДАЛЬНЫЕ ЛОГИКИЗадача.Три мудреца спорили о том, кто из них мудрее. Прохожийвзялся разрешить их спор.

Он сказал: «У меня в мешке пятьшапок: 3 черных и 2 белых. Я завяжу вам глаза, наденукаждому на голову одну из шапок, а потом развяжу глаза. Тотиз вас, кто первым догадается, какого цвета шапка у него наголове, будет признан мудрейшмим». Мудрецы согласились, ипрохожий исполнил все то, о чем он говорил. После того, как сглаз мудрецов были сняты повязки, некоторое время никто непроизнес ни слова. И после этого один из мудрецов заявил:«На моей голове черная шапка». Он оказался прав, и былпризнан мудрейшим.Вопрос: Докажите, что мудрейший из мудрых слеп.МОДАЛЬНЫЕ ЛОГИКИЭпистемические логики и мультагентные системыВ мультиагентных системах нужно ввести более специальныемодальные операторы.Пусть A = {a1 , a2 , .

. . an } — множество агентов. Тогдаa ϕ означает «Агент a знает, что ϕ верно».C ϕ означает «Все агенты знают, что ϕ верно».Специальные разновидности эпистемических логикприменяются для описания и проверки требованийбезопасности сетевых протоколов.МОДАЛЬНЫЕ ЛОГИКИТемпоральные логикиТемпоральные (временные) логики применяются для описанияи исследования причинно-следственных зависимостей,развивающихся во времени.Модальный оператор означает «всегда»,а оператор ♦ — «когда-нибудь».Семантика темпоральных логик существенно зависит от тойматематической модели, которая используется для описанияфеномена времени. В самом общем случае в качестве моделивремени можно взять любое частично упорядоченноемножество.

Элементы этого множества соответствуютразличным моментам времени.В качестве темпоральных моделей могут выступать любыемодели Крипке, построенные на основе частичноупорядоченных шкал. Разные отношения частичного порядкапорождают разные темпоральные логики.МОДАЛЬНЫЕ ЛОГИКИТемпоральные логикиПоскольку вычисление — это процесс, развивающийся вовремени, состояния которого находятся впричинно-следственной связи друг с другом, темпоральныелогики используются для спецификации и верификациипрограмм.

Наиболее широкое распространение получили дверазновидности темпоральных логик.Логика линейного времени LTLШкала Крипке для LTL (L inear T emporal L ogics) — этонатуральный ряд с естественным отношением порядка hN, ≤i. ? 0 y1 ? -2 y &? 3y6? 4y6? y6%r r rМОДАЛЬНЫЕ ЛОГИКИЛогика линейного времени LTL 0 y? 1 ? -2 y p, ¬qp, ¬q&? 3yp, q6? 4yp, ¬q6? yp, ¬q6%r r rМОДАЛЬНЫЕ ЛОГИКИЛогика линейного времени LTLI , 0 |= p,I , 0 6|= q, 0 y? 1 ? -2 y p, ¬qp, ¬q&? 3yp, q6I , 0 |= ♦q? 4yp, ¬q6? yp, ¬q6%r r rМОДАЛЬНЫЕ ЛОГИКИЛогика линейного времени LTLI , 0 |= p,I , 0 6|= q, 0 y1 ? -2? y p, ¬qp, ¬q&3?yp, q6I , 0 |= ♦q4?yp, ¬q6?yp, ¬q6%r r rПрименение LTL для верификации моделей программ болееподробно будет обсуждаться в последующих лекциях.МОДАЛЬНЫЕ ЛОГИКИТемпоральные логикиВ других темпоральных логиках время — это ветвящаясяструктура; в каждый момент времени может быть несколькоальтернатив дальнейшего развития событий.yHHHHHHHHj yy@@@?y@y@Ry@@y?y@@R y@?yy?yМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLТемпоральные логики такого вида называются логикамиветвящегося времени (BTL, Branching Time Logics).Одной из логик ветвящегося времени является логика деревьеввычислений (CTL, Computational Tree Logic), используемая дляспецификации и верификации распределенных программ имикроэлектронных схем.В логике CTL имеются темпоральные операторы двух типов —универсальные и экзистенциальные.∀,∀♦,∃,∃♦.Тип темпорального оператора указывет на то, будет ливыполнимость формулы проверяться на всех ветвях древесноймодели или только на одной ветви.МОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLПусть I = hS, R, ξi — древесная модель Крипке для логикиCTL, s0 ∈ S — одно из состояний модели.

ТогдаI , s0 |= ∀ϕ ⇐⇒в каждом состоянии s, достижимом из состояния s0 , верноI , s |= ϕ;I , s0 |= ∃ϕ ⇐⇒существует ветвь, исходящая из состояния s0 , в каждомсостоянии s которой верно I , s |= ϕ;I , s0 |= ∀♦ϕ ⇐⇒в каждой ветви, исходящей из состояния s0 , есть состояние s, вкотором верно I , s |= ϕ;I , s0 |= ∃♦ϕ ⇐⇒существует ветвь, исходящая из состояния s0 , в одном изсостоянии s которой верно I , s |= ϕ.МОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∀ps0s1s3p = trueyHp = trueHHHHHs2HHj yp = true@@@s4s5@Ry@p = true yp = trueyp = true?y@@s6yp = trues7 ?yp = true@s8@R y@p = trues9 ?yp = trues10s11y?yp = truep = trueМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∃ps0s1yHp = trueHHHHHs2HHj yp = true@@@s4s5@Ry@p = true yys3 ?y@@s6ys7 ?y@s8@R y@s9 ?yp = trues10ys11?yМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∀♦ps0yHHHs1HHHs2Hj yH@@ys3 ?p = true ys4p = true@s5@Ry@y@@s6ys7 ?y@s8@R y@s9 ?ys10s11y?yp = truep = trueМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∃♦ps0yHHHs1HHHs2Hj yH@@ys3 ?ys4@s5@Ry@y@@s6ys7 ?yp = true@s8@R y@s9 ?ys10ys11?yМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLФормулы CTL можно использовать для формальнойспецификации многих интересных свойств поведения программ∀ ∃♦ Restart:на любом этапе функционирования системы можноосуществить ее перезапуск;∀ (Request → ∀♦ Response):когда бы ни был послан запрос, рано или поздно на негообязательно поступит отклик.МОДАЛЬНЫЕ ЛОГИКИА как проверить,что вычисления программудовлетворяют заданным спецификациям?И можно ли эту проверкуавтоматизировать?КОНЕЦ ЛЕКЦИИ 18-19..