2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010).djvu), страница 11

2.1), Однако возможность использования эюго формализма для верификации дискретных систем сомнительна. Прогресс в области верификации был достигнут на пути введения спеннадьных модаяьноссей в обычную логику высказываний. 2.2. Модельные и вреиенные логики. Телве 1 о91с В приведенных выше примерах высказываний время не присутствует явно. И нам действительно часто невюкно, прн каких конкретных значениях времени наступали те нли иные событлсь ввкно только выразить порядок событий, отлоиселие (раныпе/позже) между моментами времени, в которых эти события наступали (вспомним тезис Лесли Лампорта (Ьезйе Ьашрогс): "Время есть способ упорядочения событий").

Характеристики временных свойств систем используют категории вида "никогда не будет верно, что...", илн "в будущем обязательно случится, что..." и тому подобные, характеризующие истинность суждениа с учетом отношений между моментамн наступления различных событий во времени, Можно расширил классическую логику, разрешив использовать такие категории перед утверждениями логики, например, выралсение Р Получено(т) можно понимать так: "Когда-нибудь в булушем сообщение т обазательно будет получено".

Такие категории называются модсыьлослыми, они стоят перед высказыванивмн н каким-либо образом харысгернзуют высказывания. Модаяьнвсть в логике (от лат. тосю — способ, наклонение) вжщитсл дополнительным оператором, предваряющим высказывание.

Модальиый оператор харакюризуст высказывание, являкнцееся его операндом. В общем случае модальный оператор не обязательно связан со временем. Например, пусть с — некоторое высказывание. Можно выразить неполную уверенносгь в истинности утверждения а, сказав: "Возможно, по о истинно".

Для формалиыцни этого введем модавьный оператор М. Тогда Мс! имеет смысл "возможно, что ! ", или "мелеет быть, а истинно". .Формальные теории устанавливают соотношения между формулами. Например, введем модельный оператор Ь, имеющий смысл "с необходимоссью верно, что...". Тогда можно саваующим образом определись отношение между модальноспмн М и Ь: Ьа м-и-ч), что соглвсуегса с инсувтивно нс- гхееа я таиным утверждением, например: го, что а обазательно насгупит, зто то же самое, что неверно, что а, возможно, не наступит".

Лругой пример. Пусть р означает утверждение "писатель иммет". Тогда соотношение лчеи М р ингерпретнруегся совершенно правияьной фразой "Писатель докгеен писать тогда и талька тогда, когда он нг молгет не тлсать". Классическая логика, расшнреннал какими-нибудь операторамн модальности, напишется модальной логикой. Такое расширение можно определить поразному, вводя разного типа модальности и дшке разную их семантику (формальное определение смысла модапьностей). Возможность иапользования различной семантики проистекает из того, что в разных применениях трактовки одних и тех же модальных слов естественного языка часто различны, и даже в одной области применения они обмчно смутны, расплывчаты.

неоднозначны. Поэтому существует большое число различных модальных логик, юшанш из которых удобна в конкретной области применения. Модальности, которыми можно расширить классическую логику, могут быть связаны н а характеристикой момента времени, в котором утверждается истинность высказывания, зависящего от времени. Логики, расширенные такими модвльностями, назмваются темпоральнмми, или временными логиками.

Мы будем использовать термин тгмноральныг логики. а Опредаиеиие 2. т (твыпарвиьные лоеиви) Темпорапьные логики — зто логики, в которых нстиншютное значение логических формул зависит от момента времени, в котором вычисляются значения этих формул. Темпоральные логики давно использовались в философии лля изучения таких схем рассуждений, которые включают ссьлпщ на време. Основная идея темпоральной логики состоит в том, чтобы фиксировать только относительный норадок событий — фактически, текущее, будущее и прошедшее время.

Конечно, в некоторых приложениях, например в области верификации систем реального времени, явные значения времеви и численные ограничения иа время должны учитываться, и там мм введем другие формализмы (см. гл. (л). В опной из предшественниц современных темпорапьных логик — Тепле (лб)с, разработанной английским логиком Артуром Прайором (Агйшг Рг(ог) в середине прошлого века, бьши впервые ваелены две модальности: Р (от ригше): "когда-нибудь в будущем будет истинно.,." и Р (от Ршг): "когда-то в прошлом было истинно...".

На рнс. 22 поюкано, прн каких значениях времени испщны утверждения Ра и Ра, если заданы отрезки времени, в которых испынно утверждение а. Обо- ч р Р вчь ни, Рв . Ч папаню в Внаюию: РЧ - Ч пччююсь а арюсювс 99 Ч есина опег в еивювчс нч -ч асина всею в срсюпсьс ч !! нч но- ор!ня ск ,н гк, значим г1=Ф упюрюдение: "В момент времени г истинно угюсрмшенне Ф". Тогда (рис. 2.2): П утверюденне л истинно в момент времени г (г )=е) .

если угверюденне л истинно в момент с (что является, конечно, тавтолопюй); П угвермденне Ре истинно в момент времени г (г ~=рй ), если для какого. то момента времени г' в будущем е станет истинным; П утверягдение Ре истинно в момент времени с (г ! Рд) . если дяв квкогото момегпа времени с' в прошлом ушерюдение е было истинным. ч-аююсюююсасеача вмюи ге ч г! ч Рис.

2,2. Темпсрвльные свератсры Тессе Ьщ!с В Телес !.ой)с введены н два луальныл темпорвльных операторм С (от слоев О)ОЬа!)у) И Н (От СЛОаа Н)Ваху), С СООтпОШЕНИВМН: Сею-Р у, Нею-1Р у. Сприюдлнвость этих оютношеиггй очевидна. Например, первого: "Утвер- лщать, гго в будущем й будет всегда летнюю, это то же санов, что утверждать, что неверно, что когда-нибудь в будущем й станет ложным". Эти операторы можно определить и нешвнсимо аг Р н Р (см. Рис. 2 ДР П утверждение С у истинно в момент времени г (г )=Сй), если лля любого момента времени г' в будущем утверждение й истинно; П ушержденне Нй истинно в момент времени г (г ~=Но), если лпя любого момента времени г' в прошлом упир1кдение а истинно. Уже с помощью двух темпоразьных операторов Р и С можно выразить сложные свойства, зависящие от времени. Например: Утверждение а будет истинным.' П всегда в будущем: Са П хотя бы рзз в будущем: рй П ниюгла в будущем: Ра П бесюнечно много раз в будущем: Сйй П с какого-то момента посюянно: РСй Рассмотрим, как с помощью этих операторов формально записать некоторые угвержле пня.

П Собьпня р и й никогда не произойдутодновременно: С (рлй) П Любое посланное сообщение когда-нибудь в будущем будет получено: С(Послало юРПовучвкои) П Джейн вышла замуж и родила ребеняа: Р(Джейн выходит эанулслРДзсвйи ролсовт ребенка) П Дзкейн родила ребенка и вышла замуж Р(Джвйл рохсовт рвбенкалРДжвйл выходит замуж) П Ленин жил, Левин жшь Ленин будет жизьг РС Ленки жив П Пока ключ зюкигания не всшвлен, машина ив лопает: С( РЗ Стщ ) 0 В системах передачи информашщ формула 6 ((т и Явсвггт т) => Р(т я свтувг оьт)) вырткяст следующее свойство: канал передачи информашш не мажет спонтанно порождюь свои собственные сообщение.

А именно, всегда (6), если сообщение т появилось во вхолном буфере приемника (та йвсв)гвг.й), то когтг-то ранее (Р ) сообщение т находшикь в выходном буфере передатчика (т и щвн(вг.он! ) . В темпоральную логику макно ввести еще два оператора; у(як!у!те (Х) и Уньй (У). Оператор игл!у(тв: угвержление Хц истинно в момент'времени г, если ц истинно в следующий момент г+!: 0 Двюн убил, и ему стало страшно: Р(Джон убивает нХОДжону страшно). 0 Если я видел ее раньше, то я ве узнаю при встрече: 6 (Рувндвл => 6(йтнрвтня сь Х узная)) . 0 Джон умер и его похоронилн; Р(Джон умирает л ХРДжона хоронят). Оператор Ут!! (до тех пор, пока не наступит нечто) требует лвух аргументов — угаерждений. Утверждение рУ! истинно в момент времени г, если ц истинно в некоторый будущий момент временк, а во всем промежутке от момента !до !' истинно р: когда.

нибудь ц, а до твх нор р . Пример развертки во времени, показывмощей, когда будет истинно утверждение р Уц при различных истннностных значениях р и ц, показан на рнс. 2.3. !бого рпц - ц огрызся в бицяцем, в ло нто неяреамане й!цт Вьвзствггьгн )х г!аяза Р ХДТ р в р р Ути С оператором Уний многие славные угвержденйа.иегко представимы в формальной записи, например: (г Мы не друзья, пока ты не извинишься: (д(ы друзья)%Ты нзвыыешься П Лифт никогда не пройдет мимо втыка, вызов от которого поступил, но еще ие обслужен: С (Вызов(л) =>( Лифт(я)) 6 Обслулснвается (н)) Через оператор ИФ! лепго вырывается оператор р: Ра=оие ба в следовательно, и оператор С: Са= (Р а)--(~ ()-6).