Русская Википедия:Темпоральная логика
Темпоральная логика (временна́я логика; Шаблон:Lang-en) — логика, в высказываниях которой учитывается временной аспект. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале.
В древности применение логики во временно́м аспекте изучали философы мегарской школы, в частности Диодор Крон, и стоики. Современная символическая темпоральная логика, впервые концептуализированная и сформулированная в 1950-е годы Шаблон:Iw[1] на основе модальной логики, наибольшее распространение и развитие получила в информатике благодаря трудам лауреата Тьюринговской премии Амира Пнуэли.
Пример
Смысл утверждения: «я голоден» не меняется со временем, однако его истинность может измениться: в конкретный момент времени оно может быть истинным, либо ложным, но не одновременно. В противоположность нетемпоральным логикам, где значения утверждений не меняются со временем, в темпоральной логике значение зависит от того, когда оно проверяется. Темпоральная логика позволяет выразить утверждения типа «я всегда голоден», «я иногда голоден» или «Я голоден, пока я не поем».
Темпоральные операторы
В темпоральных логиках бывает два вида операторов: логические и модальные. В качестве логических операторов обычно используются (<math>\neg,\lor,\land,\rightarrow</math>). Модальные операторы, используемые в логике линейного времени и логике деревьев вычислений, определяются следующим образом.
| Текстовое обозначение | Символьное обозначение | Определение | Описание | Диаграмма |
|---|---|---|---|---|
| Бинарные операторы | ||||
| <math>\phi</math> U <math>\psi</math> | <math>\phi ~\mathcal{U}~ \psi</math> | <math>\begin{matrix}(B\,\mathcal{U}\,C)(\phi)= \\ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)))\end{matrix}</math> | Until (strong): <math>\psi</math> должно выполниться в некотором состоянии в будущем (возможно, в текущем), свойство <math>\phi</math> обязано выполняться во всех состояниях до обозначенного (не включительно). | <timeline>
ImageSize = width:240 height:94 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:1 till:3 bar:q color:red width:10 align:left fontsize:S from:3 till:5 bar:pUq color:red width:10 align:left fontsize:S from:1 till:5 </timeline> |
| <math>\phi</math> R <math>\psi</math>
<math>\phi</math> V <math>\psi</math> |
<math>\phi ~\mathcal{R}~ \psi</math>
<math>\phi ~\mathcal{V}~ \psi</math> |
<math>\begin{matrix}(B\,\mathcal{R}\,C)(\phi)= \\ (\forall i:C(\phi_i)\lor(\exists j<i:B(\phi_j)))\end{matrix}</math> | Release: <math>\phi</math> освобождает <math>\psi</math>, если <math>\psi</math> истинно, пока не наступит момент, когда <math>\phi</math> первый раз станет истинно (или всегда, если такого момента не наступит). Иначе, <math>\phi</math> должно хотя бы раз стать истинным, пока <math>\psi</math> не стало истинным первый раз. | <timeline>
ImageSize = width:240 height:100 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:4 bar:q color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 bar:pRq color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 </timeline> |
| Унарные операторы | ||||
| N <math>\phi</math>
X <math>\phi</math> |
<math>\circ \phi</math> | <math>\mathcal{N}B(\phi_i)=B(\phi_{i+1})</math> | NeXt: <math>\phi</math> должно быть истинным в состоянии, непосредственно следующим за данным. | <timeline>
ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:3 from:5 till:6 bar:Np color:red width:10 align:left fontsize:S from:1 till:2 from:4 till:5 </timeline> |
| F <math>\phi</math> | <math>\Diamond \phi</math> | <math>\mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi)</math> | Future: <math>\phi</math> должно стать истинным хотя бы в одном состоянии в будущем. | <timeline>
ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:2 till:3 from:4 till:5 bar:Fp color:red width:10 align:left fontsize:S from:0 till:5 </timeline> |
| G <math>\phi</math> | <math>\Box \phi</math> | <math>\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)</math> | Globally: <math>\phi</math> должно быть истинно во всех будущих состояниях. | <timeline>
ImageSize = width:240 height:60 PlotArea = left:30 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:1 till:3 from:4 till:6 bar:Gp color:red width:10 align:left fontsize:S from:4 till:6 </timeline> |
| A <math>\phi</math> | <math> \mathcal{A} \phi </math> | <math>\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}</math> | All: <math>\phi</math> должно выполняться на всех ветвях, начинающихся с данной. | |
| E <math>\phi</math> | <math> \mathcal{E} \phi </math> | <math>\begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix}</math> | Exists: существует хотя бы одна ветвь, на которой <math>\phi</math> выполняется. | |
Другие модальные операторы
- Оператор W, означающий Weak until: <math>f W g</math> эквивалентно <math>f U g \lor G f</math>
Тождества двойственности
Подобно правилам де Моргана существуют свойства двойственности для темпоральных операторов:
- <math>\phi ~\mathcal{U}~ \psi = \neg(\neg \phi ~\mathcal{V}~ \neg \psi)</math>
- <math>\neg \Diamond \phi = \Box \neg \phi</math>
- <math> \neg \mathcal{A} \phi = \mathcal{E} \neg \phi </math>
Приложения
Темпоральные логики часто применяются для выражения требований формальной верификации. Например, свойства типа «если поступил запрос, то на него обязательно придёт ответ» или «функция вызывается не более одного раза за вычисление» удобно формулировать с помощью темпоральных логик. Для проверки таких свойств используются различные автоматы, например, автоматы Бюхи для проверки свойств, выраженных логикой линейного времени LTL.
Варианты
Основной универсальный вариант темпоральной логики — Шаблон:Iw (Скотт — де Баккер, 1969); оно в качестве подмножества включает Шаблон:Iw и Шаблон:Iw, а основные используемые в информатике варианты — Шаблон:Нп2 и Шаблон:Нп2 — являются фрагментами CTL*.
Кроме того, существуют и другие варианты темпоральной логики, не сводимые к модальному μ-исчислению, например, Шаблон:Iw и Шаблон:Iw
Некоторые практические варианты используют комбинации темпоральной логики с другими логиками, в частности, такова темпоральная логика действий (созданная для языка спецификаций TLA⁺), соединяющая темпоральную логику и логику действий.
Примечания
Литература
- Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. М.: МЦНМО. 2002. ISBN 5-94057-054-2
