Статья 459

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

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

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