Темпоральная математическая логика .

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

3.2 Синтаксис CTL

Синтаксис ветвящейся темпоральной логики (логики деревьев вычислений) определяется следующим образом. Элементарными выражениями в CTL являются атомарные предложения, как и в определении LTL. Будем определять синтаксис CTL в нотации Бэкуса-Наура (р принадлежит множеству атомарных предложений AP):

φ ::=р | φ | (φ ˄ φ) | EX φ | Е[φ U φ] | А[φ U φ].

Используются темпоральные операторы следующего вида:
EX (в следующий момент для некоторого пути);
Е (для некоторого пути);
А (для всех путей);
U (до тех пор).
Здесь X и U - линейные темпоральные операторы, которые выражают свойства на фиксированном пути, в то время как экзистенциальный квантификатор пути E выражает свойство на некотором пути, а универсальный квантификатор пути А - свойство на всех путях. Квантификаторы пути Е и А могут быть использованы только в комбинации с X или U. Отметим, что оператор AX неэлементарен и определяется ниже.
Булевы операторы true, false, ˄, → и ↔ определяются как обычно. Из равенства F φ = true U φ следуют два сокращения:

EF φ = E[true U φ];
AF φ = A[true U φ].

EF (φ произносится как «φ выполняется потенциально», a AF (φ - как «φ неизбежно».
Так как G φ = F φ и A φ = E φ то дополнительно:

EG φ = AF φ
AG φ = EF φ;
AX φ = EX φ

Например, справедливо:

A(F φ)
<=> A φ ≡ E φ
.E .(F φ)
<=> G φ ≡ F φ вычисления }
EG φ.

EG φ произносится «потенциально всегда φ», AG φ - «безусловно φ», a АХ φ - «для всех путей в следующий момент φ».
Синтаксис CTL требует, чтобы линейным темпоральным операторам X, F, G и U немедленно предшествовали квантификаторы пути Е или А. Если это ограничение опустить, то получится более выразительная ветвящаяся темпоральная логика CTL .
Логика CTL позволяет квантификаторам Е и А предшествовать любой LTL-подформуле. Она содержит, ряд формул, которые не являются синтаксическими термами CTL. Логика CTL может быть рассмотрена как ветвящийся аналог логики LTL, так как каждая подформула LTL может быть использована в CTL-формуле. Точные взаимоотношения между LTL, CTL и CTL будут рассмотрены ниже. Несмотря на то, что CTL не обладает выразительной силой CTL , рассмотрение большого числа примеров показало, что она часто достаточно выразительна для формулировки большинства требуемых свойств.

3.3 Семантика CTL

Как было отмечено в соответствующем разделе, интерпретация линейной темпоральной логики LTL определяется в терминах модели М= (S, R, Label), где S - множество состояний, Label - назначение атомарных предложений состояниям, a R - тотальная функция, которая каждому заданному состоянию ставит в соответствие единственное состояние-потомок. Так как потомок R(s) состояния s только один, модель М порождает для каждого состояния s последовательность состояний s, R(s), а также R(R(s)).
Такие последовательности представляют вычислительные пути, которые начинаются в s, а так как LTL-формула обращается к одному пути, интерпретация LTL определена в терминах таких последовательностей.
Ветвящаяся темпоральная логика, однако, обращается не к одному вычислительному пути, а к некоторым (или всем) вычислительным путям. Одной последовательности, таким образом, недостаточно для того, чтобы это промоделировать. С целью адекватно представить моменты, в которых возможно ветвление, понятие последовательности было заменено понятием дерева. Соответственно, CTL-моделью называют модель, порождающая дерево. Формально, CTL-модель является моделью Крите, так как Саул Крипке использовал сходные структуры с целью дать семантику модальной логике, типу логики, который тесно связан с темпоральной логикой [27].
Отметим, что единственное различие с LTL-моделью в том, что R теперь является тотальным отношением вместо тотальной функции.

3.4 Перечень некоторых аксиом CTL

В разделе реферата, где говориться про линейную темпоральную логику, было показано, что аксиомы могут быть полезными для того, чтобы доказывать эквивалентность между формулами: часто вместо доказательства эквивалентности с использованием семантических определений достаточно применять аксиомы, которые определены в терминах синтаксиса формул. Это облегчает доказательство эквивалентности формул. Важной аксиомой для проверки LTL-моделей является правило расширения оператора U:

φ U ψ≡ ψ \/ ((р ˄ X [φ U ψ]).

При подстановке этого правила в определения F и G получим:

G φ ≡ φ ˄ XG φ
F φ ≡ φ \/ XF φ.

Для логики CTL существуют аналогичные аксиомы. Учитывая, что каждый линейный темпоральный оператор U, F или G должен быть предварен экзистенциальным или универсальным квантификатором, получаем аксиомы, перечисленные в табл. 1.

Таблица 1 – Перечень аксиом расширения для CTL

EG φ ≡ φ ˄ EX EG φ AG φ ≡ φ ˄ АХ AG φ EF φ ≡ φ \/ EX EF φ AF φ ≡ φ \/ АХ AF φ Е [φ U ψ] ≡ ψ \/ φ ˄ ЕХ(Е[φ U ψ])) А [φ U ψ] ≡ ψ \/ (φ ˄ АХ(А[φ U ψ]))

У всех этих аксиом базовая идея состоит в выражении справедливости формулы предложением о текущем состоянии (где нет необходимости в использовании темпоральных операторов) и предложением о прямых потомках этого состояния (с использованием ЕХ или АХ в зависимости от того, с экзистенциальным или универсальным квантификатором рассматривается формула). Например, формула ЕС φ верна в состоянии V, если φ верна в V (предложение о текущем состоянии) и φ выполняется для всех состояний вдоль пути, начинающегося с прямого потомка .V (предложение о потомках состояний). Первые четыре аксиомы могут быть выведены из последних двух.


Заключение

Итак, в заключение необходимо отметить, что основная проблема в развитии программных систем состоит в том, что проверка правильности реализуемой программной системы является очень сложным механизмом. При разработке такой системы обычно основное время уходит не столько на написание кода, сколько на его анализ и отладку. Существует много методов проверки правильности программ, и они соответствуют различным их классам.
В данном реферате рассмотрена задача для достижения целей спецификации и верификации предложен иной тип темпоральной логики. Он основан на ветвящемся представлении о времени, а не на линейном. Такой вид логики формально приспособлен для моделей, где в каждый момент может существовать несколько разных возможных будущих событий. В силу наличия такого фактора, который ветвится на представлении о времени, этот класс темпоральных логик носит название ветвящихся темпоральных логик.
Если говорить уж совсем строго, то процесс ветвления будет сведен к тому, что у состояния возможно наличие нескольких допустимых различных потомков. Представление о семантике ветвящейся темпоральной логики, таким образом, базируется на дереве состояний вместо последовательности.
В данном случае возможно определение экспоненциальной сложности формальной проверки, что может наложить значительные ограничения на применимость метода к крупным моделям. В данном случае лучше применять динамические методы, которые обеспечивают возможность более лучшей производительности верификации так называемых LTL-ограничений.
Несмотря на проблему низкого покрытия пространства состояний системы, которая зависит от внешнего теста в динамических методах, а также нелинейный рост размера проверяющих автоматов в зависимости от структурной сложности формулы, использование СTL и LTL-логик во время симуляции даст возможность обеспечения обнаружения большинства функциональных нарушений с более приемлемой производительностью в сравнении с формальными методами.
В данной работе также достигнута основная цель – описание темпоральной логики, применяемой в программировании.
В этом реферате были поставлены и решены следующие задачи:
определение основных понятий темпоральной логики;
приведение основного синтаксиса и синтематики CTL;
осуществление проверки моделей для ветвящейся темпоральной логики.


Список использованных источников

Ricardo Caferra. Logic for Computer Science and Artificial Intelligence. — John Wiley & Sons, 2013. — 537 p.
Темпоральная логика – Википедия [Электронный ресурс].Режим доступа : https://ru.wikipedia.org/wiki/Темпоральная_логика, свободный. – Загл. с экрана.
Многомерная математическая физика и многомерные приложения: Монография/А.В.Коротков, П.Д.Кравченко, В.Е.Мешков, Е.В.Мешкова, В.С.Чураков, Т.А.Брыкина. - (Серия «Многомерная парадигма А.В. Короткова в информатике, искусственном интеллекте и когнитологии». Вып.З). -Новочеркасск: Изд-во «НОК», 2016. - 193 с.
С.А. Зайченко, В.И. Хаханов. Формальная семантика сложных операторов линейной темпоральной логики. Автоматизированные системы управления и приборы автоматики. Х.: №148.– 2008. – С. 14-28.
Кораблин Ю.П., Косакян МЛ. Анализ моделей программ на языке асинхронных функциональных схем средствами темпоральной логики линейного времени. Программные продукты и системы 2014 №02 (106). Тверь: НИИ Центрпрограммсистем. — 200 c.
Потапов Д.К.Неклассические логики: Учебное пособие. - СПб.: СПбГУ, 2006. - 108 с.
Вельдер С. Э., Лукин М. А., Шалыто А. А., Яминов Б. Р. Верификация автоматных программ. СПб: Наука, 2011. 244 с.











3