Лекции В.А. Захарова, страница 31

ϕ → ϕрефлексивные шкалы∀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.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.

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

Описать строго (формально) требования правильностивычислений;2. Проверить, что все вычисления программы удовлетворяютэтим требованиям.ПРАВИЛЬНЫЕ ПРОГРАММЫОписание требований правильности функционированияпрограммы называется спецификацией программы.Проверка соблюдения вычислениями программы требованийправильности функционирования называется верификациейпрограммы.Если спецификации программ записать на формальномлогическом языке и строго определить операционнуюсемантику программ, то для доказательства правильностипрограмм можно использовать методы математической логики(логический вывод).ПРАВИЛЬНЫЕ ПРОГРАММЫФормальная верификация программПреимуществаПроблемы1.

Абсолютно точная проверкаправильности программ.1. Как заставить программистов писать формальные спецификации?2. Возможность автоматизации построения логическоговывода.2. Как заставить прувер работать эффективно?И, тем не менее, попробуем...ИМПЕРАТИВНЫЕ ПРОГРАММЫОпределим синтаксис и семантику императивных программ.Пусть задана сигнатура σ = hConst, Func, Predi, в которойопределно множество термов Term и множество атомарныхформул Atom.Условимся, что ⇐ — это служебный символ, непринадлежащий сигнатуре σ.Определениеприсваивание ::= «переменная» ⇐ «терм»условие::= «атом» | (¬условие ) |(условие & условие ) | (условие ∨ условие )программа::= присваивание |программа ; программа |if «условие» then программа else программа fi |while условие do программа odИМПЕРАТИВНЫЕ ПРОГРАММЫПримерПрограмма вычисления наибольшего общего делителя двухнатуральных чисел.Const = {0, 1, 2, .