9. МОДАЛЬНОСТЬ В СИТУАЦИОННОМ ИСЧИСЛЕНИИ

В этой главе рассказано, что такое модальность и какую роль она играет в ситуационном исчислении, превращая его в модальное ситуационное исчисление или модальную логику. Особое внимание уделено применению модальной логики для анализа корректности поведения параллельных процессов. Изложены основы использования модальной логики для анализа корректности параиельных процессов. Описана используемая для этого анализа модель параллельных процессов. Подробно рассмотрены наиболее типичные свойства корректности параллельных процессов, их формальная запись в языке модальной логики. Приведены сведения о принципах формального доказательства (проверки) свойств корректности.

9.1. Модальность и модальная логика

При развитии различных исчислений как формальной основы для рассуждений о тех или иных явлениях нашей среды постоянно наблюдается стремление по возможности полно и точно выразить и учесть динамику изменений этой среды. Самым простым исчислением является логика высказываний (см. гл. 2). Для того чтобы выразить динамику изменений среды, например во времени, средствами логики высказываний, придется ввести переменные, истинность которых будет означать наступление того или иного момента времени. Если таких моментов много, то описание в логике высказываний становится крайне неудобным. Логика предикатов первого порядка (см. гл. 3) является более сложным, но и более выразительным исчислением в результате введения кванторов, функций и предикатов. Функции и предикаты могут зависеть от временных переменных, которые позволяют описывать динамику среды. Ситуационные исчисления еще более удобны для описания динамики среды, поскольку они основаны на использовании специальных ситуационных переменных, значения которых могут зависеть от времени или пространства.

В некоторых случаях рассуждения о динамике изменения во времени ситуаций и связанных с этими ситуациями фактов не требуют знания ни точного времени наступления этих ситуаций, ни использования самих ситуаций (ситуационных переменных). Достаточным является установление истинности того, что та или иная формула, выражающая определенные отношения между объектами среды, станет, в конце концов, истинной, не станет истинной, станет истинной с какой-либо степенью уверенности и т.п. при определенных значениях объектных переменных в некоторой ситуации, явное значение которой нас не интересует. На естественном языке для выражения этих отношений обычно используют слова типа “допустимо”, “необходимо”, “возможно” и другие, выражающие определенную степень уверенности наступления каких-либо событий во времени или пространстве, но без указания точного времени или места. Возможность делать в логике высказывания, содержащие выразительные средства, которые характеризуют подобную степень уверенности или «силу» высказывания, называют модальностью. Исчисления, в которых введены специальные символы или слова (модальные операторы), с помощью которых это делается, называют модальными исчислениями.

В настоящей главе рассмотрим пример одного из таких исчислений, основанного на логике предикатов первого порядка и называемого обычно временным модальным исчислением или временной модальной логикой. Слово “временное” появляется здесь в связи с тем, что изменение подразумеваемых ситуаций происходит во времени. В нашем случае время течет линейно. Ситуации, естественно, тоже изменяются линейно в этом времени. Обсудим более подробно концептуальную суть временного модального исчисления.

Рассмотрим, например, утверждение: «Идет дождь». Очевидно, что истинность этого утверждения зависит от двух факторов (параметров): даты и места, которые подразумеваются, но не употреблены. Выбирая определенные дату и место и уточняя с их помощью указанного утверждения, получаем другое утверждение: «Идет дождь в месте во время Это утверждение полностью определено и должно быть либо ложным, либо истинным. Теперь можно ввести атом дождь «Идет дождь в месте во время который имеет равные приоритеты для обоих параметров Модальный подход предполагает два различных приоритета или уровня для параметров Параметр с более высоким приоритетом определяет ситуацию и не употребляется явно в высказываниях. Так, если в качестве переменной, полностью определяющей ситуацию, выбрать время, то вместо атома дождь будет использоваться атом дождь Значение этого предиката зависит как от ситуации (в данном случае времени или даты), так и от места. Но точное значение ситуации нас не интересует, поскольку мы собираемся рассуждать о таких вещах, как возможность дождя в месте в принципе или неизбежность дождя в месте когда-либо вообще и т.п.

Переход от логики предикатов к модальной логике не такой резкий, как переход от логики исчисления высказываний к логике предикатов. При этом выбор переменных, определяющих ситуацию, произволен и зависит от субъективной точки зрения. Имеются очевидные преимущества введения модального формализма. Он позволяет нам сделать переменные, определяющие ситуацию, более важными, чем все остальные, и ввести неявную зависимость формул модальной логики от ситуаций и тем самым от переменных, ее определяющих. Временная модальная логика предполагает наличие базисного отношения достижимости между ситуациями: которое определяет возможность перехода из одной ситуации в другую ситуацию Это отношение имеет место, если ситуация достижима из ситуации

Вернемся снова к примеру о дожде. Как уже отмечалось, здесь ситуации определяются датами (днями), т.е. ситуация и день или дата в данном случае одно и то же. Между ситуациями можно установить отношение достижимости: если ситуация (день) следует за ситуацией (днем) Главная идея обозначений, принятых в модальной логике, состоит в стремлении избежать обозначения ситуаций в нашем примере) и отношения достижимости. Вместо этого вводят два специальных модальных оператора, описывающих свойства ситуаций, достижимых изданной ситуации: оператор необходимости и оператор возможности 0.

Смысл этих операторов заключается в следующем. Пусть является некоторой формулой модальной логики. Тогда также формулы модальной логики. Значение формул неявно зависит от некоторой текущей ситуации Формула считается истинной в ситуации если формула истина на всех ситуациях, достижимых из ситуации включая собственно ситуацию Формула считается истинной в ситуации если формула истинна хотя бы в одной ситуации, достижимой из ситуации Обозначим значение формулы в ситуации Тогда правила вывода истинных значений модальных формул и можно записать следующим образом:

Эти правила введены только для того, чтобы пояснить смысл модальных операторов. На самом деле, как уже говорилось, в формулах модальной логики символ ситуации не используется, но подразумевается. Модальная формула записывается с помошью пропозициональных символов, предикатных символов (включая равенство), функциональных символов, констант, переменных, классических операторов (связок) и кванторов, а также модальных операторов.

Формулу без модальных операторов, являющуюся по существу формулой логики предикатов первого порядка, называют иногда статической.

Модальная формула, называемая иногда динамической, содержит статические подформулы, к которым применены классические и модальные операторы. Истинностное значение модальной формулы в некоторой ситуации можно найти на основе правил (9.1). При этом предполагается, что в каждой рассматриваемой ситуации все классические символы формулы можно интерпретировать и конкретизировать таким образом, что ее истинностное значение будет определено. Например, формула

эквивалентна утверждению «если в какой-либо день в каком-либо месте идет дождь, то наступит другой день, когда в этом же месте не будет дождя». Для того чтобы эта формула стала истинной при некотором конкретном значении места должен существовать день в который дождь начался и затем прошел в этом же месте. Утверждению «если в какой-либо день в каком-либо месте идет дождь, то он будет идти и в любой другой день в этом же месте соответствует формула

Для того чтобы эта формула стала истинной при некотором конкретном значении места должен существовать день в который дождь начался и затем уже никогда не прекращался в этом месте.

Приведем примеры формул модальной логики, поясняя на основе правил (9.1), при каких условиях эти формулы будут истинными.

Формула истинна в ситуации если существует хотя бы одна ситуация достижимая из ситуации в которой истинна формула Иными словами, истинность формулы означает, что существует ситуация достижимая из ситуации такая, что в ситуации и во всех достижимых из нее истинна формула

Формула истинна в ситуации если во всех ситуациях достижимых из ситуации истинна формула Иными словами, истинность формулы означает, что для всех ситуаций достижимых из ситуации можно найти хотя бы одну достижимую из ситуацию, в которой истинна формула

Формула истинна, если для всех ситуаций достижимых из истинна формула Истинность формулы в ситуации означает истинность формулы во всех ситуациях, достижимых из ситуации Таким образом, истинность формулы означает, что формула становится всегда истинной в любой ситуации достижимой из и остается истинной для всех ситуаций, достижимых из

Модальная логика построена на базе логики предикатов первого порядка, и в ней, естественно справедливы понятия, используемые в последней: общезначимость, выводимость и др. В частности, формулы

общезначимы. Формула

также общезначима. Это означает (на основе правила модус поненс), что истинность формулы всегда влечет истинность формулы

Задавая различные офаничения на отношение достижимости можно получать различные модальные исчисления. В нашем случае полагаем, что отношение всегда рефлексивно и транзитивно Вследствие этого общезначимы все следующие формулы:

благодаря рефлексивности (если во всех оитуациях, достижимых из истинна то истинна и в ситуации

благодаря транзитивности отношения (если существует ситуация достижимая из которая в свою очередь достижима из причем в ситуации формула истинна, то существует достижимая из в которой формула также истинна, и

Как уже отмечалось, модальная логика, рассматриваемая в настоящей книге, в своем названии имеет добавку «временная». В связи с этой добавкой на модальную логику, а точнее на базовое отношение достижимости, налагаются дополнительные условия, состоящие в том, что ситуация достижима из ситуации если ситуация может перейти в ситуацию благодаря изменениям среды во времени. В настоящей книге ограничиваемся линейным и дискретным изменением ситуаций. Это означает, что рассматриваемая нами временная модальная логика имеет дело с последовательностями вида причем достижимо из тогда и только тогда, если есть единственная начальная ситуация.

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

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