2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 12
Текст из файла (страница 12)
Подобно тому, квк оператор Н являешя аналогом оператора С в прошлом, в этой логши н для операторов Х н () существуют их аналоги в прошлом: Х' (в щмдыдущкй момент еремеяи, "вчера) и 8 (этсе, "с тек нор, как"). Тенге (ой(с позвалшт формально предсшвить некоторые философские мысли о времени. Например, обозначим атомарное утверждение "нечет есть" символом а .
Тогда следующее глубокомысленное абсолютно истинное заключение (тввтшюгию): Будет. что нечто бьыо, если и только еглн оно или есть сейчас, иеи будет. нвн улсе бьыо можно формализовать так: Ррд дчРйчРа. Тоягдественно истиннымн явяяютсл н такие формулы: р юНРр — если нечто есть, то в щюыюм оно всегда собиралась наступить. р ыгСРр — если нечто есть то е будущем оно всегда будет настуиивФплософская мысль о времени: Любое "вчера" было когда-ню "завтра", любое "завтра" когда-нибудь слизнет "вчера" формально запишется тюс (РХ ~а кэРХа) л (РХ(( юРХла) . ом, зм: ТаждсьтВЕННО Иетнииай фОрМуЛОИ днХ"ЗХа МОЖНО фаритщвааатЬ МЬИЛЬ Иосифа Брсдскогт Настоящему, чтобм обресвпг буфщее, требуется вчера. Временная логика помогает точно и однозначно выразить вреьюнные соотношение межлу собьппями, о которых повествуют гчасто неоднозначные) фразы естественного взыка.
Обозначим; Д(к): к — й дру; П(к): к — р т) Использув зги обозначения, можно формально записать несколько совершенно различных интерпрепщий прадложения "Леой др)н ЛЩГ будет нрезиденнюм": Б Д(МЕ)лРХП(Лйг): сейчас ИМ вЂ” мой друг, а в будущем он ставен президентам. Х РХ(Д(ЛГЛг) л П(Мт)); в будущем ЛЛГ станет моин другам, и в зто гремя он унсе будет нрвзю деллют.
5. Р(Д(МУ) А РХ П()тдг)): в будущем Мч'станет моин другом, и нотам он станет нренн.'интам. 2.3. Темпоральная логика линейного времени((ЛЦ Современная темпоральнвя логика линейного времени П.Т3 Баеве Типе соус) является наслелницей временной логики Тепзе 1.оус Арзурв Прапора. ЬТЬ рвзрабаЪзна израильским ученым Амиром Пи)оли ГАщи Рпиев лля спецификации свойств параллельных технн неких систем. В ПЪ максимально упрощены все вкяючеиные в нее концепции и строго формально определена интерпретация се формул. Во-первых, в БТБ темпорвльными операторами рзсширена прсстейцищ логика высказываний, формулы которой строятся щ конечного числа атомарных прелнкатов и булевых операций. "Предикат" — зто высказывание, принимающее значение либо "истина", либо "лоэсь" в зависимости от значений его аргументов.
Например, истинность высказывания "к > 5" щвисит от значения аргумента к. В лапте линейного времени опермруют атомариымн преднкатвмн, т.е. здесь нас интересует только истинность либо лакность злементвр- гзгаеа 2 ных высказываний, а не тс, как зти высказывания построены нли как определяется их нстннностное значение. Ф Определение 22(втомирнььй мт, ламп!с Атомарный предикат (атомарное утверждение) — это угверждеиие, которое может принимать истинное или ложное значение и от струкгуры которого мы абстрагируемся. Во-вторых, в новую логику включено минимальное число темпоральных операторов, которые определиот хараггеристикн истинности высктываннй, упорядоченных во времени. Таких операторов только дея, 0 и Х.
Логика (.Т). не вкпючест темпоральных операторов прошлого. Основания дла этого очевидны: прошлое для технических систем менее важно, чем их будущее поведение, начинающееся с момента их включения, запуска. В качестве интерпрещцин формул темпоральной логики рассматривается дискретная во времени бесконечная линейная направленная в будущее последовательность "миров", а каждом нз которых существует сжж интерпретация атомарных утверждений (рис.
24). Инымн словами, формулы ).Т(. принимают истинное или ложное значение на последовательности миров, и в мекком из миров лля всех введенных атомарных утверждений определены свои конкретные истиниостные значения. Такой взгляд на изменчивость во времени значения истинности атомарных ущерждений (атомарных преликатов) имел еще Аристотель, который говорил, что "угверлщения и мнения" могут имегь разные значения истинности в зависимости от моментов, в которые они делмотся, отражен изменения в объекпщ, свойства котормх они предс щаляют. рнс. 24. Интерпретация темпорельной логики ВТ — бесконечная псслелоеательность миров Линейная темпоральная логика является расширением обычной логики высказываний для рассуждений о бесконечной последовательности "миров" (например, пней илн лет нашей жизни, как у Лермонтова: "е,цюкаялье беснюдном еепчнл я лень яиэккемх лкт...").
В псслцповательвктн миров время можно считкгь изоморфным щпуральному раду б, 1, 2, ..., все миры в цепочке щпкно считать пронумерованными, н в нюкдом мире логические переменные (атомарные щюликаты) принимают конкретные истинностные значеиин— ых ий, !КЭ >го тс День как челы Π— не лаеторитоя, Дель коичнясл. Что было е иаи? На эиаю, прачетел, как лжива. Ои быч обыкновенным днем. А ясе-люки ие иоетарится. ЗилаидаГиллиус г чо ьь'эч с чтс гл ч в" т- ля ж- П.
чв во ю- ни либо истину, либо ложь. Например, сегодня я числюсь студентом н Путин— президент, а завтра я отчислен, Пугин уже не президент, а Джейн родила ребенка. Направленность последовательности миров от прошлого к булущему позволяет проводить рассуждения об относительном времени. в терминах "до" и "после". На рис. 2.4 дан пример такой интерпрспщни.
На последовательности миров иб,м1,м2,...,мл,... задано множество атомарных предикатов (р, Ф г). В мире чО атомарные лреднкаты р и а истинны, а г — ложен, в мире м1 утверищеиия О и г истинны, а р — ломаю, н т. п. Инымн словами, кткцый мир макет быть не похожим на другой: Будем считать, по в этом примере, начиная с м2, асе нстннностные значения р,,1 и г во всех мирах этой конкретной бесконечной последовкптьности (рис. 2.4) одинаковы и совпадан1т с нх значениями в м2. Как происходит переключение от одного мира к следующему, теория не раг сматриваст, от этого она абстрагируется. Поскольку в каягдом мире каждый атомарный прцликат имеет свое стабильное и неизменное в этом мире истинностное значение — истину илн лакь, лъе или уа(зе, то и формулы обычной логики выстпмваний в разных мирах могут иметь различные истннностные значения, вычисленные по этим интерпретациям своих аргументов.
Например, в мире иО формула а ~ г ложна, а во всех следующих мирах данной цепочки миров она истинна. Формула г л О в мире нО ложна, а в м2 — истинна. Рис. 2.5 показывает, в какам мирах упомянутые формулы выполняются, а в каких — нет (онн представль ны тогда со знаком отрицания " ").
Рнс. 2.6. В каждом мире итипорые иропознцвоиамаще фсрмулм нсгнииы, яругие — ист Гаева 2 Очевидно, что иа конкретной цепочке миров можно, в принципе, подсчитать и истинность формул, включающих темпоргльные операторы.. Например, формула гл и истинна, начиная с гг2, поэтому в нО истинна формула О()(г л д); действительно, существует такое )20 (равиое 2), что до вй истинно О, а начиная с вй истинно г л ) (ниже дано формальное определение всех темпорваьных операторов). чмг, л" гл-с, ' '" чц(ь,-.ч). Рне. 2.6. В каждом мире пекоторыс темпореяыще формулы истинны, изуми — нет Формула линейной темпоральной логики Ф выполняется на последовательности миров ип,мйгг2,..., если Ф истинна в начальном мире иО этой последовательности.
Твкая привязка к начаяьиому моменту времени вюкна дяя технических систем: дла нас обычно винно знать, будет лн некоторое свойство будущего поведения выполиэтьса в системе, стартующей нз пачгыьнаео состояния. Это означает, что для приведенной цепочки миров вьпкжняюэся формулы р, о, г, (джэг), (гл-,д), О()(гл д) ит.д.— именноони истинны в чО. Отметим, что существуют трактовки, которые счгпают формулу темпоральной логики истинной на цепочке миров только тогда, когда она истинна ла всех мнргх этой цепочки.
Первая точка зрения (в английской терминологии она называстса "огю)гогрг(", привязалися к началу) кажется более предпочтительной, чем вторая (которая в английской терминологии называется "г(гт))глб", дрейфующая), потому что вторую можно лепю выразить через первую: г(ггу)гпб н С агмЬогед ' Формулы ИЪ построены иэ атомарных предиюпов с помощью булевых операций н темпоральных операторов. Значения истинности обычных булевых формул в каждом конкретном мире определяется очевидным образом по значениям истинности, которые имеют атомарные преднкаты в этом мире.
Для темпоральных формул их нстннностные значения в каждом мире определя- гать иерз »ула нс- цо ире льна ни сигея ер- пеых на(ля зя- Т альные лаанян Ы ются по значениям истинности ик аргументов в цепочке миров, начинающей- са с этого мира. Темпораяьные формулы характер»цуют развитие аизуации ао времени, они мо»уг использоваться для задания свойств бесконечных процессов. Так, формула Хр истинна, если в слелующем мире (например, на следующий день) утвержденна р будат истинным. Формула р()а истинна в текущем мире, если а узка истинно в этом мире, илн же в этом мире истинно р, н оно будег истинным ао всех будущих "мирах" до тех пор, пока не станет истинным й. В логике ЬТ).
через темпоральный оператор () можно определить темпоральные операторы Р и С . Поэтому операторы $г и С называютая "выводимыми" а логике ВТ)., Например, формула Рр истинна в текущем мире данной цепочки миров, если когда-нибудь в будущем в этой цепочке станет истинным р (возможно, неоднократно). Мшкно строить н композицию темпоральных операторов. Например, формула СРр истинна в текущем мире. если а любом будущем мире верно, что в дальнейшем когяа-нибудь станет истинным р. В мирах, которые »нцт после тех, в которых р стало истинным, пике выполняется йр, поэтому СРр определяет, что в будущем р будет истинным бесконечно много раз. Формула РСр истинна, сали когда-нибудь в будущем утверждение р станет истинным н останетса истинным навсегда.
Прн записи формул темпоральной логики будем считать, что все темпоральные операторы имеют одинаковый приоритет, больший, чем приоритет лю. бой логической спермами. поэтому, например, формулу рг)р ч са будем понимать, как (р()й) ч(Сй). Для более ясной ншнси и выделения структуры формул рекомендуется всегда использовать окобки. Пример 2.1 рассмотрим несколько примеров формалнщции вьюказываннй естественного юыка. Такую формализацию зачасгую макно выполнить по-разному, поскольку высказывания естественного языка не всегда однозначны.
а) Формаанзуем известное латинское изречение "0нн» зр)га, араго" (пока живу, надеюсь). Его нельзя представить простой импликацией "Есзн я ленц ню я надеюсь" (формально: Я лене ~ Я нааеюсь), поскольку формула р н» а показывает связь двух атомарных утверждений р н а только в текущий моменг. Утверждение "Пока лонер, надеюсь" говорит, что я буду надеяться есегда, пока буду жив.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
