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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

Є два підходи темпоральной логіки, засновані на принципах здорового глузду і діалектики: «після цього» означає «внаслідок цього», або «після цього» означає «пізніше» в хронологічному сенсі.

Приклад[ред.ред. код]

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

Темпоральні оператори[ред.ред. код]

У темпоральній логіці буває два види операторів: логічні і модальні. В якості логічних операторів зазвичай використовуються (\neg,\or,\and,\rightarrow). Модальні оператори, які використовуються в логіці лінійного часу і логіці дерев обчислень, визначаються наступним чином.

Текстове значення Символьне значення Визначення Опис Діаграма
Бинарні оператори
\phi U \psi \phi ~\mathcal{U}~ \psi \begin{matrix}(B\,\mathcal{U}\,C)(\phi)= \\ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)))\end{matrix} Until (strong): \psi повинно виконатися в деякому стані в майбутньому (можливо, в поточному), властивість \phi мало виконуватися у всіх станах до позначеного (не включно).
\phi R \psi

\phi V \psi

\phi ~\mathcal{R}~ \psi

\phi ~\mathcal{V}~ \psi

\begin{matrix}(B\,\mathcal{R}\,C)(\phi)= \\ (\forall i:C(\phi_i)\lor(\exists j<i:B(\phi_j)))\end{matrix} Release: \phi освобождает \psi, якщо \psi істинно, поки не наступить момент, коли \phi перший раз стане істинно (або завжди, якщо такий момент не наступить). Інакше, \phi повинно хоча б раз стати істинним, поки \psi не стало істинним перший раз.
Унарні оператори
N \phi

X \phi

\circ \phi \mathcal{N}B(\phi_i)=B(\phi_{i+1}) NeXt: \phi повинно бути істинним в стані, безпосередньо наступним за даними.
F \phi \Diamond \phi \mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi) Future: \phi має стати істинним хоча б в одному стані в майбутньому.
G \phi \Box \phi \mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi) Globally: \phi має бути істинно у всіх майбутніх станах.
A \phi  \mathcal{A} \phi \begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix} All: \phi повинно виконуватися на всіх гілках, що починаються з даної.
E \phi  \mathcal{E} \phi \begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix} Exists: існує хоча б одна гілка, на якій \phi виконується.

Інші модальні оператори[ред.ред. код]

  • Оператор W, що означає Weak until: f W g еквівалентно f U g \or G f

Тотожності подвійності[ред.ред. код]

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

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

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

Темпоральні логіки[ред.ред. код]

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

Джерела[ред.ред. код]

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


Сигма Це незавершена стаття з математики.
Ви можете допомогти проекту, виправивши або дописавши її.