Ожидание происходит по причине выполнения специальных команд программы, которые называются семафорными инструкциями.
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 с.
