ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Публикационная активность

(сведения по итогам 2017 г.)
2-летний импакт-фактор РИНЦ: 0,500
2-летний импакт-фактор РИНЦ без самоцитирования: 0,405
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 0,817
5-летний импакт-фактор РИНЦ: 0,319
5-летний импакт-фактор РИНЦ без самоцитирования: 0,264
Суммарное число цитирований журнала в РИНЦ: 6012
Пятилетний индекс Херфиндаля по цитирующим журналам: 404
Индекс Херфиндаля по организациям авторов: 338
Десятилетний индекс Хирша: 17
Место в общем рейтинге SCIENCE INDEX за 2017 год: 527
Место в рейтинге SCIENCE INDEX за 2017 год по тематике "Автоматика. Вычислительная техника": 16

Больше данных по публикационной активности нашего журнале за 2008-2017 гг. на сайте РИНЦ

Добавить в закладки

Следующий номер на сайте

2
Ожидается:
16 Июня 2019

Унифицированное представление формул логик LTL и CTL системами рекурсивных уравнений

The unified representation of LTL and CTL logics formulas by recursive equation systems
Дата подачи статьи: 2018-12-27
УДК: 519.767.2
Статья опубликована в выпуске журнала № 1 за 2019 год. [ на стр. 020-025 ][ 26.02.2019 ]
Аннотация:Для решения задачи верификации методом проверки на моделях Model Checking сегодня зачастую используются такие временные логики, как логика линейного времени LTL, логика ветвящегося времени CTL и логика CTL*, объединяющая возможности двух первых логик. Однако каждая из этих логик имеет свои недостатки, ограничения и проблемы выразительности, которые возникают ввиду их синтаксических и семантических особенностей. Именно поэтому на текущий момент не существует единой темпоральной логики. Авторы данной статьи убеждены, что использование специальных представлений, основанных на системах рекурсивных уравнений в отношении темпоральных логик, способно не только расширить их выразительную мощность, но и унифицировать синтаксические конструкции, позволив тем самым сформулировать некоторую общую и единую для всех логик нотацию. В статье предложена и рассмотрена специальная RTL-нотация, в основе которой лежат системы рекурсивных уравнений и привычные семантические определения логик LTL и CTL. Задача, которую призвана решить данная нотация, состоит в объединении выразительных возможностей обеих логик, что расширит выразительность каждой из них, а также в унификации их синтаксических конструкций, что даст возможность выработать единообразный подход к решению задачи верификации. Авторами дано подробное определение RTL-нотации, представлены соответствующие аксиомы и теоремы, приведен ряд примеров и утверждений, наглядно демонстрирующих выразительные возможности RTL. Целью статьи является демонстрация ключевых особенностей и возможностей RTL-нотации, которые в дальнейших работах авторов лягут в основу решения проблемы верификации моделей систем.
Abstract:Nowadays, to solve the formal verification problem using the Model Checking method, the following logics are often used: the linear-time temporal logic (LTL), the computation tree logic (CTL) and CTL* that combines the capabilities of both other logics. However, each of these logics has its own disadvantages, limitations and expressiveness problems due to their syntactic and se-mantic features. Therefore, there is no universal temporal logic at the moment. The authors are convinced that special representations, which are based on systems of recursive equations in regard to tem-poral logics, can extend their expressiveness, as well as unify their syntax. Thus, they allow building their common and uniform notation. The paper proposes and considers a special RTL notation that is based on systems of recursive equations and the accus-tomed LTL and CTL semantic definitions. The notation is intended to solve the problem of unification of expressiveness of both logics, which in turn expands the expressiveness each one of them. The unification of their syntactic structures will give an opportunity to develop a uniform approach for the Model Checking problem. The authors provide a detailed definition of the RTL notation; give corresponding axioms and theorems. The paper also rep-resents a number of examples and statements that clearly demonstrate the RTL expressiveness capabilities. The purpose of the paper is to demonstrate key features and capabilities of the RTL notation, which are the basis for the au-thors' further research on solving the problem of system models verification.
Авторы: Кораблин Ю.П. (y.p.k@mail.ru) - Российский государственный социальный университет, г. Москва, Москва, Россия, доктор технических наук, Шипов А.А. (a-j-a-1@yandex.ru) - Московский технологический университет (МИРЭА), Москва, Россия, Аспирант
Ключевые слова: формула временной логики, ctl, ltl, эквациональная характеристика rltl, model checking, верификация
Keywords: temporal logic formula, ctl, ltl, rltl equation characteristics, model checking, verification
Количество просмотров: 405
Статья в формате PDF
Выпуск в формате PDF (6.60Мб)

Размер шрифта:       Шрифт:

Верификация сложных программных и технических систем давно стала неотъемлемой частью их жизненного цикла. Существующие инструменты и средства верификации постоянно развиваются и совершенствуются с целью повышения их быстродействия, гибкости и расширения области применения. Так, одним из наиболее актуальных на сегодняшний день является метод формальной верификации на моделях, или Model Checking [1, 2].

Концептуальная особенность данного метода в том, что верификация выполняется путем анализа свойств моделей систем, построенных на базе некоторых формальных конструкций, относительно требований к ним, также заданных формально. Как правило, для задания требований оперируют такими временными логиками, как LTL, CTL, CTL* [3–6]. Однако выразительные способности этих логик не являются безграничными и в некоторых случаях невозможно задать с их помощью необходимые требования.

Авторами в ряде предыдущих работ уже были предприняты некоторые меры, способные значительно расширить выразительную способность логики линейного времени LTL путем использования специальной RLTL-нотации, описывающей формулы LTL в виде систем рекурсивных уравнений [7]. Помимо этого, было показано, что при помощи RLTL можно задавать не только сами требования, но и модели вери- фицируемых систем, что позволяет упростить процесс верификации и повысить его эффективность [8].

Логика CTL [6] является альтернативным по отношению к LTL способом формулирования временных свойств. Если в логике линейного времени свойства формулируются лишь относительно некоторого порядка их наступления внутри вычислительного процесса, то в логике ветвящегося времени, помимо порядка, учитываются также сами альтернативы развития вычислительного процесса. В отличие от логики линейного времени, формулы которой являются формулами пути, формулы логики ветвящегося времени являются формулами состояний. То есть любой темпоральный оператор формулы CTL предварен квантором пути, который определяет, на всех (квантор всеобщности A) или только на некоторых (квантор существования E) путях из текущего состояния соответствующая формула является истинной [1].

Верифицируемая система может работать в разных режимах в зависимости от условий или исходных данных, может поддерживать многопоточное/многопроцессное выполнение [9] или результаты работы системы носят вероятностный характер [10]. Во всех этих ситуациях логики линейного времени, скорее всего, будет недостаточно.

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

RTL-нотация

Предложенная авторами в работе [6] RLTL-нотация позволяет представлять операторы LTL и их композиции в виде систем рекурсивных уравнений (см. табл. 1, 2).

Таблица 1

Рекурсивные представления операторов LTL в RLTL

Table 1

Recursive representations of LTL operators in RLTL

LTL

RLTL

Fφ = φ ∨ XFφ

F = φ + ∆ ∘ F

Gφ = φ ∧ XGφ

G = φ ∘ G

φ1Uφ2 = φ2 ∨ φ1 ∧ X(φ1Uφ2)

U = φ2 + φ1 ∘ U

φ1 ∧ Xφ2

φ1 ∘ φ2

∆ ∘ φ

Таблица 2

Примеры представления композиций операторов LTL в RLTL

Table 2

The examples of composition representations of LTL operators in RLTL

LTL

RLTL

FGφ

F = φ ∘ G + ∆ ∘ F

G = φ ∘ G

GFφ

G = φ ∘ G + ∆ ∘ G

Формулам LTL в RLTL-нотации соответствуют системы рекурсивных уравнений. В левой части каждого уравнения записывается метапеременная, уникально идентифицирующая данное уравнение, в правой – темпоральное выражение, содержащее как метапеременные, так и терминальные символы (предикаты).

Замечание. Не следует путать использование метапеременных F, G и U в рекурсивных уравнениях с одноименными темпоральными операторами.

Символ ∘ обозначает оператор продолжения (конкатенация выражений), что позволяет использовать оператор X в неявном виде, а также упростить его восприятие, в частности, запись φ1 ∘ φ2 будем понимать как φ2 следует за φ1. Символом + соединяются альтернативные ветви выражений. Под символом ∆, именуемым предикатом неопределенности, будем понимать некоторое неопределенное подмножество символов входного алфавита, под отрицанием данного пре- диката – некоторое другое неопределенное под- множество символов алфавита, а под отрицанием отрицания – некоторое третье неопределенное подмножество. Таким образом, отрицание предиката неопределенности является неполным, а каждое последующее отрицание дает неопределенное подмно- жество символов. Каждое из этих подмножеств ввиду своей неопределенности также может быть обозна- чено через ∆. Таким образом, мы имеем следующее свойство: ˥∆ = ∆.

Запись вида ∆⍵ является расширением предиката неопределенности и представляет собой сокращенную запись для рекурсивного уравнения F = ∆ ∘ F, означающего наступление бесконечной последовательности предикатов неопределенности на всех путях вычислительного процесса, исходящих из данного состояния. При этом следует отметить, что наступление предиката неопределенности в некотором состоянии вычислительного процесса не отрицает наступление в этом же состоянии любого из символов входного алфавита.

Унифицированная нотация логик LTL и CTL, далее именуемая RTL-нотацией, представляет собой RLTL-нотацию, расширенную и дополненную рядом аксиом и условных обозначений формул логики ветвящегося времени. Для расширения RLTL-нотации в RTL следует ввести следующие допущения:

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

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

В таблице 3 представлены все основные операторы логики CTL и соответствующие им синтаксические конструкции RTL.

Таблица 3

Рекурсивные представления операторов CTL в RTL-нотации

Table 3

Recursive representations of CTL operators in RTL notation

CTL

RTL

1

AXφ

∆ ∘ φ

2

EXφ

∆ ∘ (φ + ∆)

3

AFφ = φ ∨ AX AFφ

F = φ + ∆ ∘ F

4

EFφ = φ ∨ EX EFφ

F = φ + ∆ ∘ (F + ∆⍵)

5

AGφ = φ ∧ AX AGφ

F = φ ∘ F

6

EGφ = φ ∧ EX EGφ

F = φ ∘ (F + ∆⍵)

7

A(φ1Uφ2) = φ2 ∨ φ1 ∧ AX A(φ1Uφ2)

F = φ2 + φ1 ∘ F

8

E(φ1Uφ2) = φ2 ∨ φ1 ∧ EX E(φ1Uφ2)

F = φ2 + φ1 ∘ (F + ∆⍵)

Обозначим через 𝒫(C) множество всех последовательностей предикатов, соответствующих формуле C логики ветвящегося времени, а через 𝒫(R(C)) – множество всех последовательностей предикатов, соответствующих представлению формулы C в RTL.

Теорема 1. Для всех формул C логики ветвящегося времени 𝒫(C) = 𝒫(R(C)).

Доказательство. Формула AXφ означает, что, каким бы ни было значение предиката на данном шаге, на следующем шаге будет истинным значение преди- ката φ. Запись ∆ ∘ φ означает, что на данном шаге вы- полняется некоторое неопределенное множество пре- дикатов (возможно, пустое), а на следующем шаге будет истинным значение предиката φ, что в точности совпадает со смыслом формулы AXφ.

Рассмотрим также доказательство теоремы для формулы EGφ. В соответствии с семантикой этой формулы в CTL множество последовательностей включает в себя, по крайней мере, одну ветвь, для которой на данном шаге справедливо утверждение (предикат) φ, а на каждом следующем шаге, опять же хотя бы в одной ветви, являющейся продолжением данной ветви, справедливо утверждение φ. Из представления данной формулы в RTL нетрудно понять, что на данном шаге хотя бы в одной ветви должно быть справедливым утверждение φ, а на каждом следующем шаге, опять же хотя бы в одной ветви, являющейся продолжением данной ветви, справедливо утверждение φ, что в точности совпадает со смыслом формулы EGφ.

Аналогичным образом можно показать и справедливость всех приведенных в таблице 3 представлений формул CTL.

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

Отметим, что RTL представляет собой именно нотацию для представления формул логик LTL и CTL, поскольку базируется на их семантических определениях, но никак не отдельную логику.

Сформулируем аксиомы и правила вывода нотации RTL, задающие систему эквивалентных преобразований формул CTL. Cимволом γ (с индексами и без) будем обозначать темпоральные выражения.

Аксиомы RTL:

A1. ˥Fγ = G˥γ

A2. ˥Gγ = F˥γ

A3. ˥Aγ = E˥γ

A4. ˥Eγ = A˥γ

A5. ˥∆ = ∆

A6. ∆⍵ ∘ γ = ∆⍵

A7. ∆⍵ = ∆ ∘ ∆⍵

A8. γ1 + γ2 = γ2 + γ1

A9. γ + γ = γ

A10. (γ1 + γ2) + γ3 = γ1 + (γ2 + γ3)

A11. γ1 ∘ (γ2 ∘ γ3) = (γ1 ∘ γ2) ∘ γ3

A12. (γ1 + γ2) ∘ γ3 = γ1 ∘ γ3 + γ2 ∘ γ3

A13. γ1 ∘ (γ2 + γ3) = γ1 ∘ γ2 + γ1 ∘ γ3

Правила вывода RTL:

R1. F = γ1 ∘ F ∘ γ2 → F = γ1 ∘ F

R2. F = γ1 ∘ F → F = γ1 ∘ F ∘ γ2 (и в обратную сторону правило справедливо)

Сочетания операторов CTL

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

Утверждение 1. Выражение вида AGAFφ логики CTL может быть представлено в RTL-нотации в виде F = φ ∘ F + ∆ ∘ F.

Доказательство. Обозначим через F выражение AGAFφ = AG(AFφ), а через F1 выражение AFφ.

F = AGAFφ = AG(AFφ) = (п. 5 табл. 3)

F1 ∘ F = (п. 3 табл. 3)

(φ + ∆ ∘ F1) ∘ F = (A12)

φ ∘ F + ∆ ∘ F1 ∘ F = (A11)

φ ∘ F + ∆ ∘ (F1 ∘ F) =

φ ∘ F + ∆ ∘ F, ч.т.д.

Утверждение 2. Выражение вида AGEFφ логики CTL может быть представлено в RTL-нотации в виде F = φ ∘ F + ∆ ∘ (F + ∆⍵).

Доказательство. Обозначим через F выражение AGEFφ = AG(EFφ), а через F1 выражение EFφ.

F = AGEFφ = AG(EFφ) = (п. 5 табл. 3)

F1 ∘ F = (п. 4 табл. 3)

(φ + ∆ ∘ (F1 + ∆⍵)) ∘ F = (A12)

φ ∘ F + ∆ ∘ (F1 ∘ F + ∆⍵ ∘ F) = (A6)

φ ∘ F + ∆ ∘ (F + ∆⍵), ч.т.д.

Утверждение 3. Выражение вида AFAGφ логики CTL может быть представлено в RTL-нотации в виде системы рекурсивных уравнений:

F = φ ∘ F1 + ∆ ∘ F

F1= φ ∘ F1

Доказательство. Обозначим через F выражение AFAGφ = AF(AGφ), а через F1 выражение AGφ.

F = AFAGφ = AF(AGφ) = (п. 3 табл. 3)

F1 + ∆ ∘ F = (п. 5 табл. 3)

φ ∘ F1+ ∆ ∘ F

F1 = φ ∘ F1 (п. 5 табл. 3), ч.т.д.

Утверждение 4. Выражение вида AFEGφ логики CTL может быть представлено в RTL-нотации в виде системы рекурсивных уравнений:

F = φ ∘ (F1+ ∆⍵) + ∆ ∘ F

F1 = φ ∘ (F1 + ∆⍵)

Доказательство. Обозначим через F выражение AFEGφ = AF(EGφ), а через F1 выражение AEφ.

F = AFEGφ = AF(EGφ) = (п. 3 табл. 3)

F1 + ∆ ∘ F = (п. 6 табл. 3)

φ ∘ (F1 + ∆⍵) + ∆ ∘ F

F1 = φ ∘ (F1 + ∆⍵) (п. 6 табл. 3), ч.т.д.

Докажем также теорему, существенно упрощающую формулировку некоторых верифицируемых условий.

Теорема 2. Справедливы следующие равенства:

1.    AFAFφ = AFφ;

2.    EFEFφ = EFφ;

3.    AGAGφ = AGφ;

4.    EGEGφ = EGφ.

Доказательство п. 1. Обозначим через F1 выражение AFAFφ, а через F2 выражение AFφ.

F1 = AFAFφ = F2 + ∆ ∘ F1 = φ + ∆ ∘ F2 + ∆ ∘ F1 =

= (A13) = φ + ∆ ∘ (F2 + F1) = φ + ∆ ∘ F3

F3 = (F2 + F1) = φ + ∆ ∘ F2 + ∆ ∘ (F2 + F1) = =(A13) =

= φ + ∆ ∘ (F2 + F2 + F1) = φ + ∆ ∘ (F2 + F1) = φ + ∆ ∘ F3.

Таким образом, для левой части равенства получаем систему из двух рекурсивных уравнений:

F1 = φ + ∆ ∘ F3

F3 = φ + ∆ ∘ F3.

Очевидно, что рекурсивное уравнение, представляющее выражение AFφ, можно расширить до системы уравнений вида

F1¢ = φ + ∆ ∘ F2¢

F2¢ = φ + ∆ ∘ F2¢.

Получаем систему уравнений, совпадающую с си- стемой уравнений для левой части равенства 1 с точ- ностью до переименования метапеременных, а следовательно, задающую то же самое множество последовательностей, ч.т.д.

Аналогичным образом нетрудно доказать справедливость равенств 2–4.

Примеры

Рассмотрим три примера для лучшего понимания принципов задания формул ветвящегося времени на базе RTL.

1. F = ∆ ∘ (Gφ1 + Gφ2). Формула истинна, если «из текущего состояния исходят два типа ветвей: либо во всех состояниях выполняется φ1, либо во всех состояниях выполняется φ2».

2. F = φ1 ∘ (Gφ3 + Gφ4) + φ2 ∘ Gφ5. Формула истинна, если «в текущем состоянии выполняется φ1 или φ2, при этом, если выполняется φ1, то из текущего состояния исходят два типа ветвей: либо во всех состояниях выполняется φ3, либо во всех состояниях выполняется φ4; если в текущем состоянии выполняется φ2, то исходят лишь те ветви вычислительных последовательностей, для которых во всех состояниях истинно φ5».

3. F = φ ∘ (F + ∆⍵). Формула истинна, если «в текущем состоянии выполняется φ и из него исходит хотя бы одна ветвь, в которой будет истинна эта же формула».

На рисунке представлены развертки моделей, удовлетворяющие примерам 1–3 соответственно.

Отметим, что переход в некоторое состояние, помеченное каким-либо символом предиката (например, предикатом φ), отображает на самом деле все множество переходов в состояния, в которых выполняется этот предикат.

Заключение

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

задачи Model Checking и ее сложности с помощью RTL-нотации будут подробно рассмотрены в последующих работах.

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

Литература

1.     Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб: БХВ-Петербург, 2010. 552 с.

2.     Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. М.: МЦНМО, 2002. 416 с.

3.     Pnueli A. The temporal logic of program. Proc. 18th Anny. Symp. on Foundation of Computer Science, 1977, pp. 46–57.

4.     Manna Z., Pnueli A. The temporal logic of reactive and concurrent systems. Specification, 1992, 427 p.

5.     Kroger F., Merz S. Temporal logic and state systems. Springer, 2008, 436 p.

6.     Huth M., Ryan M. Logic in computer science: modelling and reasoning about systems. Cambridge Univ. Press, 2004, 443 p.

7.     Кораблин Ю.П., Шипов А.А. Эквациональная характеристика формул LTL // Программные продукты и системы. 2015. № 4. С. 175–179.

8.     Кораблин Ю.П., Шипов А.А. Построение моделей систем на базе эквациональной характеристики формул LTL // Програм- мные продукты и системы. 2017. № 1. С. 61–66.

9.     Olderog E.-R., Apt K.R. Fairness in parallel programs: the transformational approach. ACM Transactions on Programming Languages and Systems, 1988, vol. 10, no. 3, pp. 420–455.

10.  Yongming Li, Yali Li, Zhanyou Ma. Computation tree logic model checking based on possibility measures. Fuzzy Sets and Systems, 2015, vol. 262, pp. 44–59.

References

  1. Karpov Yu.G. Model Checking. Verification of Parallel and Distributed Software Systems. St. Petersburg, BHV-Peterburg Publ., 2010, 552 p.
  2. Clarke E.M., Grumberg O., Peled D.A. Model Checking. MIT Press, Cambridge, MA, USA, 1999 (Russ. ed.: Moscow, MTsNMO Publ., 2002, 416 p.).
  3. Pnueli A. The temporal logic of program. Proc. 18th Annyv. Symp. on Foundation of Computer Science. 1977, pp. 46–57.
  4. Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. Specification, 1992, 427 p.
  5. Kroger F., Merz S. Temporal Logic and State Systems. Springer Publ., 2008, 436 p.
  6. Huth M., Ryan M. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge Univ. Press, 2004,
    443 p.
  7. Korablin Yu.P., Shipov A.A. LTL formula equational characteristics. Software & Systems. 2015, no. 4, pp. 175–179 (in Russ.).
  8. Korablin Yu.P., Shipov A.A. System models construction based on LTL formula equational characteristics. Software & Systems. 2017, no. 1, pp. 61–66 (in Russ.).
  9. Olderog E.-R., Apt K.R. Fairness in parallel programs: The transformational approach. ACM Trans. on Programming Languages and Systems. 1988, vol. 10, no. 3, pp. 420–455.
  10. Li Y., Li Y., Ma Zh. Computation tree logic model checking based on possibility measures. Fuzzy Sets and Systems. 2015,
    vol. 262, no. 1, pp. 44–59.

Постоянный адрес статьи:
http://swsys.ru/index.php?page=article&id=4552
Версия для печати
Выпуск в формате PDF (6.60Мб)
Статья опубликована в выпуске журнала № 1 за 2019 год. [ на стр. 020-025 ]

Возможно, Вас заинтересуют следующие статьи схожих тематик: