Темпоральная логика. 
Математическая логика

Классическая логика высказываний статична. По этой причине некоторые очевидные законы классической логики не выполняются, если по смыслу подразумевается время. Например, конъюнкция некоммутативна (А & В * В & А): «Джону стало страшно, и он сбежал» * «Джон сбежал, и ему стало страшно». Не формализуются следующие высказывания: «Клинтон — президент США» (истинно только в какой-то период), «Любой запрос к лифту с произвольного этажа, поступивший в любой момент времени, будет обязательно удовлетворен».

Темпоральная логика, соединяющая понятия классической логики и время, свойственное динамическим системам, в частности исполняемым программам, была разработана Артуром Прайором на основе модальной логики. Ближайшей моделью логики работы дискретных динамических систем является модель Кринке^[1].

Модель относится к классу недетерминированных конечных автоматов и определяется как структура (5₀, S, R, XV), где 5₀ — множество начальных состояний; .9 — множество состояний; R = S х S — множество ориентированных ребер; W — множество высказываний, связанных с переходами между состояниями.

Истинность высказываний определяется предикатом г;(ср, w), удовлетворяющим следующим условиям:

• ?;(ср & V)/, w) = 1, если ?;(cp, w) = а (|/, w) = 1;
• ?;(ф v ф, w) = 1, если г;(ф, w) = 1 или г;(ф, w) = 1;
• ?;(ф —> ф, w) = 1, если v ((f>, w) = 0 или w) = 1.

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

Необходимость (всеобщность) в модели Крипке означает истинность во всех возможных достижимых состояниях.

Возможность (существование) — истинность хотя бы в одном из достижимых состояний.

Возможность (0) и необходимость (?) во временной логике Прайора определяются через символы F и G следующими соотношениями:

0ф = cp v Лр, Пф = ф & Сф. Для любой формулы ф формула Ftp интерпретируется как «будет ф», а формула Сер читается как «всегда будет ф» и связана с формулой /чр аксиомой G (p = —iF—"ф — всегда в будущем и неверно, что когда-нибудь в будущем не ф.

К исчислению высказываний во временной логике добавляются схемы аксиом F (ф v р) = Ftp v Fp, FF (p = F (p и правила вывода (Г —" ф) —> (Г —> Яр), (ф —> ф) —> (Яр —> Яр), где Г — гипотеза.

К исчислению высказываний в темпоральной логике добавляются квантор прошедшего времени Р — «было», аксиомы темпоральной логики —iF—|(ф —> |/) —> (F.

Fp), F-iF-пф —> ф, IР I (ф —> |/) —> (Ар —> Ар),.

P-*F—i (p —> ф и правила вывода (Г —> ф) —> (Г —> -iF-пф), (Г —> ф) —> (Г —>

—> -iP-пф).

Во временной логике к исчислению высказываний может быть добавлена бинарная связка Г, позволяющая, но формулам ф и р строить формулу (ф7р), которая читается как «сейчас происходит событие ф, а затем в следующий момент времени произойдет событие vp». С помощью формул (ф₁Г (ф₂Г (ФзГ…р…)))> где ф₁₅ …, ф" являются описаниями состояний, и описывается история. Любая такая формула называется фрагментом истории.

К исчислению высказываний добавляются аксиомы ((ф! v Ф₂Ж?1 V V 1|/₂)) s ((pjTVi) V (ф, 7|/₂) V (ф₂7'ч/₁) V (ф₂7ф₂), (фГф) & (ф7х) -> (фДф & & %)). Ф = (фДф v -, ф)), ->(фТ (/ & -, ф)) и правило вывода ((Г, ф, -> ф₂); (Г,.

Vi -> ?2″ -" ((Г, (Ф^Ф,)) -> (Ф₂7?₂)).

Время в темпоральной логике дискретно и линейно упорядочено. Если число полных состояний 2″, то число возможных историй в m последующих моментах равно 2^тп.

Различаются линейная темпоральная логика LTL (linear temporal logic) и расширенная темпоральная логика ветвящегося времени CTL (extended computational tree logic).

В простом случае LTL — множество последовательных во времени состояний (рис. 6.26).

Синтаксис LTL включает пропозициональные переменные, булевы связки (-1, &, v) и темпоральные операторы, которые применяются для составления утверждений о событиях в будущем.

Темпоральные операторы:

Хр — в следующий момент выполнено р

Fp — в некоторый момент в будущем будет выполнено р

Gp — всегда в будущем выполняется р

pUq — существует состояние, в котором выполняется q, и до него во всех предыдущих состояниях выполнено р;

pRq — либо во всех состояниях выполняется q, либо существует состояние, в котором выполняется р, а во всех предыдущих состояниях выполнено q.

Примеры формализации временных высказываний^[2].

1. Джейн вышла замуж и родила ребенка:

• 2. Еще вчера «сегодня» было «завтра»: Х~^{(Хр) = р.
• 3. Вчера он сказал, что придет завтра, значит, он придет сегодня:

• 4. Джон умер, и его похоронили: Р (Джон_умирает & XF Джона_хоронят).
• 5. Если я видел ее раньше, то я ее узнаю при встрече:

6. Любое посланное сообщение будет получено:

7. Сократ умер:

Множество Р7Х-формул: если ф и р — формулы, то -.ф, ф & ф, ф v i — формулы; АУр, /чр, (Уф, ф Ui, фRi — формулы.

Пусть необходимо проверить, удовлетворяет ли представленный алгоритм свойству: «Любому обращению к семафору предшествует операция его инициализации».

Или «Когда-либо в будущем выполнится операция инициализации семафора (-ф) Ua, а до тех пор не будет ни одного обращения к семафору или же обращение к семафору не произойдет никогда С (-ф)». На языке темпоральной логики линейного времени LTL свойство будет записано формулой высказывания (-ф)На v С (-ф).

Примеры формализации высказываний в LTL.

1. Dum spiro, spero (пока живу — надеюсь):

2. Мы придем к победе коммунистического труда!:

3. р = «я люблю Машу», q = «я люблю Дашу», тогда:

Fp — «я когда-нибудь обязательно полюблю Машу», qUp — «я полюблю Машу, а до этого буду любить Дашу»,.

FGp — «когда-нибудь в будущем я полюблю Машу навечно»,.

GFq — «я буду бесконечно влюбляться в Дашу».

• 4. «Раз Персил — всегда Персил» (раз попробовав, будешь использовать всегда):
• 17Х-формула описывает желаемое поведение объекта верификации, и факт присутствия ошибки может быть подтвержден существованием в структуре Кринке последовательности состояний, нарушающей эго поведение. Структура Крипке для двух связанных процессов (рис. 6.27):
• 5₀ — начальное состояние;

.*0 — s₂ ^— основной процесс, в состоянии s_x разрешение, а семафора и передача данных;

5₁₀ — 5₁₃ — процесс ожидания, прием и обработка данных (3.

/чр = trueUq — ср когда-то в будущем выполнится, а что будет до этого — неважно (true);

?ф = «существует такой путь из данного состояния, на котором ф истинна»;

Лф = «для всех путей из данного состояния формула пути ф истинна» (?ф, Лф — кванторы пути).

Очевидно, что Лф = -if-пф.

Основное применение темпоральной логики — формальное описание временных процессов для решения задачи верификации работы динамических систем и программ. В литературе^[3] подробно представлены разработайные фирмой Bell средства верификации Spin, которые используют язык Promela (protocol meta language) и Spin (simple Promela integrated).

На рис. 6.28 приведена общая схема верификации.

• 1. Формулируется задача в виде модели Крипке.
• 2. Решение задачи оформляется в Promela.
• 3. Спецификация задачи формулируется в LTL.
• 4. Интерпретатор Spin контролирует выполнение требований спецификации.

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

Типы языка Promela — процессы (proctype), объекты, каналы посланий (channel).

В языке используется синтаксис языка Си.

Пример программы Promela'.

Byte state = 2.

Ptroctype A () ((state = = 1) —> state = 3}.

Ptroctype В () (state = state — 1}.

Init (run A (); run BO) // запускаются два процесса в модели Крипке // Связь между процессами организуется в виде каналов Channel declaration Chan name = [16] of (byte).

Chan name = [5] of (byte, int).

Sending messages // передача данных через канал.

name ! expr.

name ! exprl, expr2.

Receiving messages // прием данных через канал.

Name? var.

Name? varl, var2.

Отметим, что формальное описание семантики и синтаксиса утверждений в темпоральной логике, естественно, интуитивное, как и всякая формализация в логике. Иногда приводится некоторое интуитивное описание, при исполнении которого в Spin могут быть найдены ошибки^[4].

• [1] Карпов Ю. Г. Model checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010; Mads Dam Promela and SPIN Royal Insituteof Technology KTH, 2004.
• [2] Карпов Ю. Г. Указ. соч.
• [3] Карпов Ю. Г. Указ, соч.; Mads Dam Promela and SPIN Royal Insitute of Technology KTH2004; Лифшии, 10. Верификация программ и темпоральные логики. Лекция 3 курса «Современные задачи теоретической информатики». СПб.: Изд-во НИУ ИТМО, 2005. С. 3—8;Черемисинов Д. И. Проектирование и анализ параллелизма в процессах и программах. Белорусская наука, 2011; Шошмина И. В., Карпов Ю. Г.

  Введение

  в язык Promela и систему комплексной верификации Spin. СПб.: Изд-во Политехнического университета, 2010; AczelР. The Russell-Prawitz modality // Mathematical Structures in Computer Science. 2001. Vol. 11(4). P. 541—554; Goldblatt R. Mathematical modal logic: a view of its evolution // Modalities inthe Twentieth Century. Vol. 7 of the Handbook of the History of Logic / ed. by D. M. Gabbav andJ. Woods. Elsevier, 2006. P. 1—98; Sagar C. Introduction to spin and promela CMU. Roadmap. Historical perspective. Overview of Spin. Overview of Promela. Simulation with Spin. Overviewof LTL; URL: http://cm.bell-labs.com/cm/cs/what/spin.

• [4] Конкретные примеры можно найти в следующих работах: Карпов Ю. Г. Указ, соч.; Чере-мисинов Д. И. Указ, соч.; Шошмина И. В., Карпов 10. Г. Указ, соч.; Егоров К. В. Шалыто А. А. Разработка верификатора автоматных программ // Научно-технический вестник СПбГУИТМО. 2008. № 8. С. 177—188. Однако с этими примерами вряд ли можно согласиться, таккак недостаточно интуитивной информации. Предполагается известный опыт в решениизадач этого вида.