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

Например, если / - формула пути, то Е/ и А / - формулы состояния и при фиксированном состоянии sq дерева они интерпретируются: Е/истинна, если/истинна хотя бы для одной из путей, исходящих из Sq ; А/истинна, если/истинна для всех путей, исходящих из Sq . Определение формул пути логики CTL^: - если/- формула состояния, то/ - формула пути; - если/и g -формулы состояния, то f&g, fvg, X / Щ G/ j\]g, /Rg - фор­ мулы пути. Запись М,5' ^ / означает, что формула состояния / выполнена на модели М со стартовой вершиной s. В случаях, когда ясно, о какой модели Крипке идет речь, то букву Мне записывают. Из введенных десяти операторов —i, с&, к А, Е, X, F, G, U, R оказывается можно оставить только пять, например: —i, к Е, X, U, а остальные выражаются через них: f&g-^i^fv^g); /Rg~ ^ Ь / и ^g); F/~ True U^/; Темпоральные логики CTL яЬТЬ Логика CTL * является достаточно общей и это дает ему большую вырази­ тельную силу. Однако в ней очень сложна проблема распознавания выполни­ мости формул. Логика деревьев вычислений CTL представляет собой фрагмент CTL *, в которой каждый темпоральный оператор X, F, G, U и R должен следо­ вать непосредственно за квантором пути, при этом формулы пути определяют­ ся только одним условием: если/и g -формулы состояния, тоX / F/ G/ ДJg и JRg - формулы пути. Линейная темпоральная логика LTL состоит из всех формул вида Af, г д е / формула пути, в которой все формулы состояния - это атомарные высказыва­ ния. Используя введенные логики, можно осуществлять верификацию аппара­ туры и программного обеспечения, причем важно, что этот процесс можно осуществлять в автоматическом режиме. Для заданной анализируемой про­ граммы строится ее абстрактная формальная модель, например система пере­ ходов. Проверяемое свойство или требование к программе выражается в виде формул указанных логик. После этого верификация программы сводится к вы­ яснению выполнимости формулы на абстрактной модели программ. Модели Крипке используются для описания программ, а темпораль- ные логики для описания требований к ним (спецификации программ). Основная проблема эффективных алгоритмов верификации состоит в экс­ поненциальном росте числа состояний в модели Крипке. 211