Mosaic method for the logics of time

Tolstukhin Aleksei Post-graduate student, the department of Logics, M. V. Lomonosov Moscow State University 119234, Russia, Moskva oblast', g. Moscow, ul. Leninskie Gory, 1, of. 834 alexei.tolstukhin@gmail.com Other publications by this author

Введение

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

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

Метод мозаик

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

Мозаики впервые были использованы Истваном Немети для доказательства разрешимости эквациональных теорий некоторых классов алгебры отношений в ^{[8, 9]}. Однако фактическое использование данного метода можно также обнаружить в ^[3], где продемонстрирована аксиоматизация временной логики. Основная идея метода заключается в том, чтобы вместо того, чтобы иметь дело с <<большой>> моделью для некоторой формулы, можно попытаться показать, что для построения этой модели достаточно иметь конечное множество всех различных фрагментов модели. Из этих фрагментов воспроизводится вся модель, которая может быть бесконечной, путем пошаговой процедуры. При этом проблема разрешимости сводится к вопросу о наличии насыщенного множества фрагментов модели. Такие фрагменты и называются мозаиками. Стоит также отметить, что для каждой логики мозаика, то есть фрагмент модели, может определен по разному. Важно понимать, из каких схожих по структуре, нетривиальных фрагментов модели, может быть построена итоговая модель.

В том числе среди исследователей, которые работали с данным методом, ярко выделяется М. Рейнолдс, который использовал этот подход при рассмотрении многомерных модальных логик. Логика FP, рассматриваемая Рейнолдсом в ^[11] является по сути произведением логик LinS5, где Lin есть логика линейного времени прайоровского типа. Система LinS5 конечно аксиоматизируема, но не является финитно аппроксимируемой, что не дает возможности получить результат о разрешимости стандартным для модальных логик способом.

Идея мозаик также использовалась М. Марксом и И. Венемой в ^[7]. С их помощью они доказывают разрешимость и полноту систем модальной логики отношений.

М. Маркс, С. Микулас и М. Рейнолдс стали применять метод мозаик при исследовании систем временной с линейным временным потоком и модальностями и в языке. В их работе ^[6] доказаны результаты о полноте аксиоматизации логики линейного времени, её разрешимости, полноте аналитико-табличного формализма. Отдельно эти результаты были доказаны и ранее в отдельных работах, тем не менее авторы показывают, что возможности метода на этом не ограничиваются. Результаты о разрешимости могут быть получены и в случае обогащения языка временной логики сильными модальностями Untill и Since.

Кроме вышеперечисленных работ можно также упомянуть, что метод мозаик применялся для исследования вопросов, связанных с алгоритмической сложностью проблемы разрешимости. Среди работ, посвященных этой теме можно указать ^{[15, 14]}.

В ^[13] представлено табличное исчисление логики RTL, модель которой построена в ^[5] на множестве рациональных чисел, поэтому линейный поток времени обладает свойством плотности. Для обоснования простоты, непротиворечивости и полноты Рейнолдс использует технологии метода мозаик. Отметим, что ключевая лемма о насыщенном множестве мозаик была доказана им в ^[12].

Для логик с модальностями (Until) и (Since) в ^[2] мозаикам в качестве альтернативы были предложены, так называемые, частичные мозаики. Последние представляют собой более высокий уровень абстракции, чем <<полные>> мозаики. В классическом методе мозаик им сопоставляются максимально непротиворечивые множества, а в частичных мозаиках - просто пропозиционально непротиворечивые множества.

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

Мозаики для систем с прайоровскими модальностями

Пусть обозначает язык пропозициональной временной логики, содержащий счетное множество пропозициональных переменных , пропозициональные связки , , временные модальности и , которые обозначает <<когда-нибудь будет>> и <<когда-то было>>). Множество формул определяется стандартно.

Семантическими структурами для являются структуры Крипке , где есть непустое множество, а - отношение линейного порядка на множестве . Оценка переменных задана функций : . Моделью будем называть триаду . Истинность формулы в мире модели определяется как:

Истинность формулы с пропозициональными связками определяется стандартно. Оценка формул с временными модальностями производится следующим образом:

(1)

(2)

Структура Крипке, которая будет использована в данной работе обладает дополнительным свойством: множество линейно упорядочено. Обозначим подобный класс структур через Lin.

Временные мозаики.

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

Определение 1 Пара и функция : образует мозаику с базой , если для любой формулы из и для каждого , выполнены следующие условия:

1. ,

2. ,

3. ,

4. .

Возможны случаи, когда база мозаики состоит только из одного элемента. Такие мозаики с одноэлементной базой называют вырожденными мозаиками .

Теперь определим насыщенное множество мозаик.

Определение 2 Множество называется насыщенным множеством мозаик, если для всякой мозаики имеет место следующее:

1. Если и , то в найдется такая мозаика , , что , и ;

3. Если и , то в найдется такая мозаика , , что , и .

Стоит отметить, что множество мозаик , содержащее только один элемент - вырожденную мозаику, является насыщенным множеством. Через будем обозначать насыщенное множество мозаик для формулы (языка ), при условии, что есть замыкание множества .

Пусть имеется формулы языка и модель , Lin, выполняющая формулу .

Лемма 1 Если формулы выполняется в тогда и только тогда, когда существует согласованное насыщенное множество мозаик .

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

Теперь рассмотрим случай, когда содержит более одного элемента. Свяжем с каждой парой , где , соответствующую мозаику и , . В соответствии с определением 1 является мозаикой. А также легко убедиться, что есть насыщенное множество мозаик.

Доказательство (). Для доказательства леммы в обратную сторону, нам понадобится определение ассоциированной структуры с разметкой.

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

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

Определение 3 Структура с разметкой называется ассоциированной, если она удовлетворяет следующим условиям:

1. ,

2. ,

3. ,

4. .

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

Определение 4 Пусть есть фиксированная ассоциированная структура с разметкой, для некоторого , и не существует такого , что и . Тогда есть дефект будущего в данной структуре.

Определение 5 Пусть есть фиксированная ассоциированная структура с разметкой, для некоторого , и не существует такого , что и . Тогда есть дефект прошлого в данной структуре.

Далее необходимо представить, каким образом можно исправить дефекты структуры. Рассмотрим некоторую структуру с разметкой и пусть есть дефект будущего для какого-то . Тогда для всякого такого, что либо , либо и . То же самое будет, если - максимальный элемент . Отсюда дефекты бывают двух видов: максимальный, требующий наличие <<свидетеля>>, и внутренний, если <<свидетель>> должен быть вставлен где-то внутри порядка). Опишем процедуры устранения дефектов на примере дефектов прошлого.

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

Тогда исходя из пункта 3 определения насыщенного множества мозаик существует такая мозаика . Пусть таким образом, что и для всех является ассоциированная структура с разметкой. Это ясно из определения.

Пункт 1 выполняется в силу определения функции , посколько каждому приписывает то же значение, что и некоторая .

Для подтверждения пункта 2 нужно показать, что . Здесь возможны два случая. Первый - . Поскольку отображение . Согласно определениям . Далее по определению мозаики . Путем замены <<равного равным>> получаем .

Пункт 3 для зеркален пункту 2.

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

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

Приступим непосредственно к доказательству.

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

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

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

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

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

Пусть и . Определим оценку пропозициональных переменных таким образом, что: . Докажем, что для всякой формулы и для всякой точки верно, что . Доказательство проводится индукций по длине формулы. Случай с пропозициональной переменное следует из определения . Для формул вида и доказательство стандартно. Рассмотрим случаи для формул с внешними модальностями.

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

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

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

Мозаики для систем с модальностями Until и Since

Впервые попытка применить метод мозаик к временным логикам с модальностями и встречается в работе ^[6]. В ней исследователи только намечают вектор дальнейшей работы, дают первое определение мозаикам как тройственным структурам, определяют насыщенное множество мозаик.

Прежде, чем дать модифицированное определение мозаикам, необходимо определить истинность формулы с модальностями и в модели :

Интерес к выразительным возможностям временной логики с использованием U и S существует уже давно. При этом рассматриваются логики не только линейные логики, но и логики с плотным потоком, модели которых строятся на множестве рациональных и вещественных числах. Например в ^{[1, 4]} показано, что данные логики полезны для рассуждений о параллелизме и поведении аналоговых устройств, что в свою очередь вновь поднимает интерес к проблеме сложности разрешающей процедуры.

Метод мозаик, описанный выше, теперь используется для ответа на эти вопросы и служат основой для автоматизированных методов доказательства теорем в этой важной области ^{[14, 15]}.

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

Мозаики для и

Эти мозаики как и мозаики для и будут соотнесены с конечным множеством формул.

Определение 6 Для каждой формулы , определим замкнутое множество, как , где означает, что - подформула .

Определение 7 Пусть есть формула языка и . Будем называть множество максимально пропозиционально согласованное множество (MPC), если выполняются следующие условия:

1. ,

2. .

Каждое максимальное пропозиционально согласованное множество содержит ровно один элемент из пары, формула и её отрицание, из замкнутого множества.

Определим мозаику как триаду множеств формул, которые соотносятся с двумя точками структуры: есть множество формул истинных во фрагментах раньше, есть множество формул истинных во фрагментах позже и есть множество формул, которые находятся во всех точках строго между и .

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

Определение 8 Для модели , формулы , для всякого таких, что определим триаду для формулы в модели следующим образом:

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

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

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

1. Если и , то имеется две ситуации:

(a) ,а также или ,

(b) и .

2. Если и , то имеется две ситуации:

(a) или обе ситуации имеют место быть или ,

(b) и .

3. Если и , то имеется две ситуации:

(a) ,а также или ,

(b) и .

4. Если и , то имеется две ситуации:

(a) или обе ситуации имеют место быть или ,

(b) и .

Далее необходимо показать, что синтаксическая триада из определения 9 является мозаикой как фрагмента модели из определения 8. Иными словами, показать эквивалентность определений.

Лемма 2 Для любой модели , для всякой формулы языка , для любых является мозаикой.

Доказательство леммы приводится в ^[13].

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

Определение 10 Дефектом мозаики называется одна из представленных ниже ситуаций:

1. Если и при этом , или , или ;

2. Если и при этом , или , или ;

3. и при этом ;

4. ;

5. .

Отметим, что в логике с и существует 5 типов дефектов, первые три - внутренние, остальные - внешние.

Нам необходимо объединить мозаики в линейный порядок. Это возможно только при выполнении следующего условия. Представим идею композиции мозаик.

Определение 11 Пусть имеется мозаики , тогда они образуют композицию объединены композицией, то их композиция мозаика.

Лемма 4 Композиция мозаик ассоциирована.

Определение 12 Мозаику без внутренних дефектов будем называть целой.

Определение 13 Мозаику без дефектов будем называть совершенной.

Определение 14 Декомпозиция мозаики - конечная последовательность мозаики, образующих композицию .

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

Определение 15 Декомпозиция

мозаики является полной только в том случае, если выполняются все следующие условия:

1. Для всякой формулы вида :

(a) и при этом ( или ,

(b) или существует такой , что , и , (для всех ) и (для всех );

2. Условие зеркальное условию 1 для формулы виды ;

3. Для каждой такой, что найдется такой, что и .

Если условие 1.b определения выполняется в случае, когда (имеет место дефект типа 1), то мы можем утверждать, что дефект исправлен, поскольку имеется свидетель . Аналогично для зеркальной формулы (дефект типа 3) мы также говорим, что исправление этого дефекта засвидетельствовано в декомпозиции .

Таким образом, можно сформулировать следующую лемму.

Лемма 5 Если является полной декомпозицией , то каждый внутренний дефект в устранен в декомпозиции.

Дальнейшие рассуждения строятся вокруг демонстрации выполнимости мозаики. Для этого необходимо доказать лемму, что всякая выполнимая мозаика имеет полное расширение только из выполнимых мозаик. А также лемму о том, что если есть композиция из двух выполнимых мозаик, то она также является выполнимой. Подробные доказательства этих лемм можно изучить в ^[13].

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

Определение 16 Для всякой формул нашего языка, множество -мозаик является насыщенным, если и только если оно замкнуто относительно композиций его элементов и для всякой из существует полное расширение, содержащие мозаики только из множества .

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

Заключение

Таким образом, во временной логике существует очень удобный метод построения моделей для временной логики, что может служить хорошим основанием для построения разрешающей процедуры. В качестве перспективы дальнейшей работы можно указать необходимость построения исчисления, которое бы реализовывало идею мозаик, доказательство непротиворечивости и полноты этого исчисления. Перспективным в данном вопросе является применение -- -конструкций, модификации из ^[16].