Темпоральна логіка

Темпоральна логіка (англ. temporal logic) в сучасній (некласичній логіці) — логіка, яка враховує причинно-наслідкові зв'язки в умовах часу. Використовується для опису послідовностей явищ та їх взаємозв'язку з часовою шкалою. Вона була розроблена в 1960-х ^[en] на основі модальної логіки і отримала подальший розвиток у інформатиці завдяки праці лауреата Премії Тюрінга Аміра Пнуелі. В античності теорії темпоральних логік вивчали філософи мегарської школи, зокрема, Діодор Крон та стоїки.

Є два підходи темпоральної логіки, засновані на принципах здорового глузду і діалектики:

1 — «після цього» означає «внаслідок цього»;

2 — «після цього» означає «пізніше» в хронологічному сенсі.

Приклад

Розглянемо твердження: «Я голодний»:

Хоча зміст виразу не змінюється з часом, його істинність може змінитися. Твердження в конкретний момент часу може бути істинним, або хибним, але не одночасно. На противагу нетемпоральним логікам, де значення тверджень не змінюються з часом, в темпоральної логіці значення залежить від того, коли воно перевіряється. Темпоральна логіка дозволяє висловити затвердження типу «Я завжди голодний», «Я іноді голодний» або «Я голодний, поки я не поїм».

Темпоральні оператори

У темпоральній логіці буває два види операторів: логічні і модальні. Як логічні оператори зазвичай використовуються (${\displaystyle \neg ,\lor ,\land ,\rightarrow }$). Модальні оператори, які використовуються в і , визначаються наступним чином.

Текстове значення	Символьне значення	Визначення	Опис	Діаграма
Бинарні оператори
${\displaystyle \phi }$ U ${\displaystyle \psi }$	${\displaystyle \phi ~{\mathcal {U}}~\psi }$	${\displaystyle {\begin{matrix}(B\,{\mathcal {U}}\,C)(\phi )=\\(\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))\end{matrix}}}$	Until (strong): ${\displaystyle \psi }$ повинно виконатися в деякому стані в майбутньому (можливо, в поточному), властивість ${\displaystyle \phi }$ мало виконуватися у всіх станах до позначеного (не включно).
${\displaystyle \phi }$ R ${\displaystyle \psi }$ ${\displaystyle \phi }$ V ${\displaystyle \psi }$	${\displaystyle \phi ~{\mathcal {R}}~\psi }$ ${\displaystyle \phi ~{\mathcal {V}}~\psi }$	${\displaystyle {\begin{matrix}(B\,{\mathcal {R}}\,C)(\phi )=\\(\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))\end{matrix}}}$	Release: ${\displaystyle \phi }$ вивільняє ${\displaystyle \psi }$, якщо ${\displaystyle \psi }$ істинно, поки не наступить момент, коли ${\displaystyle \phi }$ перший раз стане істинно (або завжди, якщо такий момент не наступить). Інакше, ${\displaystyle \phi }$ повинно хоча б раз стати істинним, поки ${\displaystyle \psi }$ не стало істинним перший раз.
Унарні оператори
N ${\displaystyle \phi }$ X ${\displaystyle \phi }$	${\displaystyle \circ \phi }$	${\displaystyle {\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})}$	NeXt: ${\displaystyle \phi }$ повинно бути істинним в стані, безпосередньо наступним за даними.
F ${\displaystyle \phi }$	${\displaystyle \Diamond \phi }$	${\displaystyle {\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )}$	Future: ${\displaystyle \phi }$ має стати істинним хоча б в одному стані в майбутньому.
G ${\displaystyle \phi }$	${\displaystyle \Box \phi }$	${\displaystyle {\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )}$	Globally: ${\displaystyle \phi }$ має бути істинно у всіх майбутніх станах.
A ${\displaystyle \phi }$	${\displaystyle {\mathcal {A}}\phi }$	${\displaystyle {\begin{matrix}({\mathcal {A}}B)(\psi )=\\(\forall \phi :\phi _{0}=\psi \to B(\phi ))\end{matrix}}}$	All: ${\displaystyle \phi }$ повинно виконуватися на всіх гілках, що починаються з даної.
E ${\displaystyle \phi }$	${\displaystyle {\mathcal {E}}\phi }$	${\displaystyle {\begin{matrix}({\mathcal {E}}B)(\psi )=\\(\exists \phi :\phi _{0}=\psi \land B(\phi ))\end{matrix}}}$	Exists: існує хоча б одна гілка, на якій ${\displaystyle \phi }$ виконується.

Інші модальні оператори

• Оператор W, що означає Weak until: ${\displaystyle fWg}$ еквівалентно ${\displaystyle fUg\lor Gf}$

Тотожності подвійності

Подібно правилам де Моргана існують властивості подвійності для темпоральних операторів:

• ${\displaystyle \phi ~{\mathcal {U}}~\psi =\neg (\neg \phi ~{\mathcal {V}}~\neg \psi )}$
• ${\displaystyle \neg \Diamond \phi =\Box \neg \phi }$
• ${\displaystyle \neg {\mathcal {A}}\phi ={\mathcal {E}}\neg \phi }$

Темпоральні логіки часто застосовуються для вираження вимог формальної верифікації. Наприклад, властивості типу «Якщо надійшов запит, то на нього обов'язково прийде відповідь» або «Функція викликається не більше одного разу за обчислення» зручно формулювати за допомогою темпоральої логіки. Для перевірки таких властивостей використовуються різні автомати, наприклад, для перевірки властивостей, виражених .

Темпоральні логіки

Відомі такі темпоральні логіки:

• Інтервальна темпоральна логіка
• μ-числення
  • • LTL
    • CTL

Джерела

• Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. М.: МЦНМО. 2002.

Література

• Логіка часу // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — 742 с. — 1000 екз. — ББК (87я2). — .