LectLog19 (1158011), страница 2

Файл №1158011 LectLog19 (Старые лекции, в целом тоже самое) 2 страницаLectLog19 (1158011) страница 22019-09-18СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 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..

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

Тип файла
PDF-файл
Размер
568,02 Kb
Тип материала
Высшее учебное заведение

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

Свежие статьи
Популярно сейчас
Зачем заказывать выполнение своего задания, если оно уже было выполнено много много раз? Его можно просто купить или даже скачать бесплатно на СтудИзбе. Найдите нужный учебный материал у нас!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6513
Авторов
на СтудИзбе
302
Средний доход
с одного платного файла
Обучение Подробнее