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

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

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

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

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

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

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

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

Текстове значення Символьне значення Визначення Опис Діаграма
Бинарні оператори
U Until (strong): повинно виконатися в деякому стані в майбутньому (можливо, в поточному), властивість мало виконуватися у всіх станах до позначеного (не включно).
R

V

Release: освобождает , якщо істинно, поки не наступить момент, коли перший раз стане істинно (або завжди, якщо такий момент не наступить). Інакше, повинно хоча б раз стати істинним, поки не стало істинним перший раз.
Унарні оператори
N

X

NeXt: повинно бути істинним в стані, безпосередньо наступним за даними.
F Future: має стати істинним хоча б в одному стані в майбутньому.
G Globally: має бути істинно у всіх майбутніх станах.
A All: повинно виконуватися на всіх гілках, що починаються з даної.
E Exists: існує хоча б одна гілка, на якій виконується.

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

  • Оператор W, що означає Weak until: еквівалентно

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

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

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

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

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

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

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


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