LectLog19 (1158011), страница 2
Текст из файла (страница 2)
. , xn , y )⇐⇒существует такой терм t(x1 , . . . , xn ), что|=I ϕ(x1 , . . . , xn , t(x1 , . . . , xn ))t(x1 , . . . , xn ) — это программа решения задачи ϕ.Это называется «изоморфизмом Карри–Ховарда».МОДАЛЬНЫЕ ЛОГИКИЗимой идет снегЗимой всегда идет снегЗимой иногда идет снегЭто разные высказывания.
И поэтому они должны бытьзаписаны разными формулами.Эти высказывания по смыслу связаны друг с другом. И этодолжно быть отражено в формулах. Поскольку высказыванияотличаются лишь словами всегда, иногда (модальностивремени ), нужно ввести какие-то логические конструкции длявыражения этих модальностей.Может быть для этой цели пригодны кванторы?МОДАЛЬНЫЕ ЛОГИКИСтуденты посещают лекцииСтуденты обязаны посещать лекцииСтуденты имеют право посещать лекцииобязан, имею право — деонтические модальности .А будут ли пригодны кванторы в этом случае для выражениямодальностей?МОДАЛЬНЫЕ ЛОГИКИЗадача имеет решениеИзвестно, что задача имеет решениеМожно допустить, что задача имеет решениезнаю, предполагаю — эпистемические модальности.А как быть здесь?МОДАЛЬНЫЕ ЛОГИКИМодальности (в естественном языке они, как правило,представлены наречиями или служебными глаголами)выражают различные оттенки истинности (уверенность,необходимость, доказуемость, осведомленность и др.).Эти оттенки можно классифицировать:Модальности необходимогонеобходимообязательновсегдадолжназнаюдоказуемоМодальности возможноговозможноне исключеноиногдаимею правопредполагаюнепротиворечиво♦МОДАЛЬНЫЕ ЛОГИКИСинтаксис модальных формулРасширим синтаксис классической логики предикатов, введядва логических оператора (модальность необходимого) и♦ (модальность возможного),при помощи которых разрешается строить формулыследующего вида:(ϕ)«необходимо ϕ»,(♦ϕ)«возможно ϕ».Во избежание большого количества скобок, будем считать, чтомодальные операторы имеют такой же приоритет, что икванторы.МОДАЛЬНЫЕ ЛОГИКИСемантика модальных формул многообразна и непроста.РассмотримПримерВерно ли, что формула ϕ → ϕ — это закон модальнойлогики?Если — модальность времени, «всегда», то ϕ → ϕ — этозакон модальной логики.Если студенты всегда ходят на лекции, то они ходят на лекции.А вот если — деонтическая модальность, «должны», тоформула ϕ → ϕ уже не может претендовать на статуслогического закона.Если студенты должны ходить на лекции, то они ходят на лекции.Это неправда, а законы логики не зависят от прихоти студентов.МОДАЛЬНЫЕ ЛОГИКИСемантика Крипке модальных формулОпределим самое общее отношение выполнимости длямодальных формул.Пусть P = {P1 , P2 , .
. . , 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- yw2HH6HHHI@6@@@@@@@@@@@@@@@@?R?@yyw3p = falsep = trueHHH w5j yHp = falseМОДАЛЬНЫЕ ЛОГИКИПримерМодель КрипкеI , w1 |= ♦pp = truew1 yI , w1 6|= pI , w1 |= ♦pI , w5 |= pI , w5 6|= ♦pw4p = false- yw2HH6HHHI@6@@@@@@@@@@@@@@@@?R?@yyw3p = falsep = trueHHH w5j yHp = falseМОДАЛЬНЫЕ ЛОГИКИПримерВыполнимостьI , w1 |= ♦pp = truew1 yI , w1 6|= pI , w1 |= ♦pI , w5 |= pI , w5 6|= ♦pw4p = false- yw2HH6HHHI@6@@@@@@@@@@@@@@@@?R?@yyw3p = falsep = trueHHH w5j yHp = 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 y?1 ? -2 y?3 ? -4 y?- y - y &666%r r rМОДАЛЬНЫЕ ЛОГИКИЛогика линейного времени LTL 0 y? 1 ? -2 y p, ¬qp, ¬q&? 3yp, q6? 4yp, ¬q6? y6p, ¬q%r r rМОДАЛЬНЫЕ ЛОГИКИЛогика линейного времени LTLI , 0 |= p,I , 0 6|= q, 0 y? 1 ? -2 y p, ¬qp, ¬q&? 3yp, q6I , 0 |= ♦q? 4yp, ¬q6? y6p, ¬q%r r rМОДАЛЬНЫЕ ЛОГИКИЛогика линейного времени LTLI , 0 |= p,I , 0 6|= q, 0 y?1 ? -2- y p, ¬qp, ¬q&?3y p, q6I , 0 |= ♦q?4y p, ¬q6?y p, ¬q6%r r rПрименение LTL для верификации моделей программ болееподробно будет обсуждаться в последующих лекциях.МОДАЛЬНЫЕ ЛОГИКИТемпоральные логикиВ других темпоральных логиках время — это ветвящаясяструктура; в каждый момент времени может быть несколькоальтернатив дальнейшего развития событий.yHHHyHHHHHj y@@@?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 |= ∀ps0s6yp = trueHHHHHHH s2s 1 Hj yp = trueyp = true@@@s3 ?s4s5@Ry@p = true yp = true yp = true@@@s7 ?s8s9 ?s10@?s11R y@yyyyyp = truep = truep = truep = truep = truep = trueМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∃ps0s6yyp = trueHHHHHHH s2s 1 Hj yp = truey@@@s3 ?s4s5@Ry@yp = true y@@@s7 ?s8s9 ?s10@?s11R y@yyyyp = trueМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∀♦ps0yHHHHHHH s2s 1 j yHy@@s3 ?p = true ys4p = true@s5@Ry@y@@s6ys7 ?y@s8@R y@s9 ?ys10yp = true?s11yp = trueМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∃♦ps0yHHHHHHH s2s 1 j yHy@@s3 ?ys4@s5@Ry@y@@s6ys7 ?yp = true@s8@R y@s9 ?ys10y?s11yМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLФормулы CTL можно использовать для формальнойспецификации многих интересных свойств поведения программ∀ ∃♦ Restart:на любом этапе функционирования системы можноосуществить ее перезапуск;∀ (Request → ∀♦ Response):когда бы ни был послан запрос, рано или поздно на негообязательно поступит отклик.МОДАЛЬНЫЕ ЛОГИКИА как проверить,что вычисления программудовлетворяют заданным спецификациям?И можно ли эту проверкуавтоматизировать?КОНЕЦ ЛЕКЦИИ 19..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
