Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Ветвящаяся {древовидная) модель времени предполагает, что в каждый момент времени может существовать несколько различных последующих мо­ ментов времени (несколько альтернатив будущего). В рассмотренных ниже логиках смысл каждой формулы темпоральной ло­ гики всегда определяется по отношению к размеченному графу переходов мо­ дели Кринке. Темпоральная логика деревьев вычислений CTL* Содержательно формулы CTL * описывают свойства деревьев вычислений. Это дерево образуется выделением некоторого состояния в модели Крипке в качестве начального состояния и последующей развертки модели в бесконеч­ ное дерево с корнем в выделенной вершине (см. Рис. 6.7 ). В дереве вычислений показываются все состояния, которые следуют из начального состояния. Обо­ значение CTL получено от английского выражения «Computational Tree Logic». В теории CTL* различают формулы состояния и формулы пути, которые строятся с помощью кванторов пути и пяти основных временных операторов. Кванторы пути: А: «выполнено для всех путей (вычислений)»; Е: «выполнено для некоторого пути {вычислений)». Темпоральные операторы: X: «в следующий момент времени». Этот оператор требует, чтобы свойст­ во выполнялось во втором (следующем) состоянии пути; G: «всегда, повсюду»; F: «когда-то в будущем». Эти три оператора одноместные, а следующие - двуместные: U: - «до тех пор пока». Оператор выполняется, если на пути имеется со­ стояние, в котором соблюдается второе свойство, и при этом каждое предшест­ вующее на этом пути состояние обладает первым свойством, т.е. когда-нибудь наступит свойство 2, а до него всегда будет свойство 1; R: - «высвободить». Этот оператор логически двойственен оператору U. Он требует, чтобы второе свойство выполнялось на пути до такого состояния, в котором выполняется первое свойство. Однако первое свойство не обязательно должно когда-нибудь быть выполнено. Обозначения X, F, G, U, R получены из английских слов «neXttime», «Fu­ ture», «Generally» («Globally»), «Until» и «Release» соответственно. Пусть P заданное множество (атомарных) высказываний. Определение формул состояния логики CTL^: если ре Р,тор - формула состояния; если/и g -формулы состояния, то —i/ f&g nfvg - формулы состояния; если/- формула пути, то Е/ и А/- формулы состояния. 210