WWW.MASH.DOBROTA.BIZ
БЕСПЛАТНАЯ  ИНТЕРНЕТ  БИБЛИОТЕКА - онлайн публикации
 

«Институт проблем информатики Российской академии наук e-mail: amironov66 С. Л. ФРЕНКЕЛЬ Институт проблем информатики Российской академии наук e-mail: fsergei УДК ...»

Минимизация вероятностных моделей программ

А. М. МИРОНОВ

Институт проблем информатики

Российской академии наук

e-mail: amironov66@gmail.com

С. Л. ФРЕНКЕЛЬ

Институт проблем информатики

Российской академии наук

e-mail: fsergei@mail.ru

УДК 681.3

Ключевые слова: верификация, вероятностные системы переходов, вероятностная

темпоральная логика, редукция вероятностных моделей .

Аннотация

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

Abstract A. M. Mironov, S. L. Frenkel, Minimization of probabilistic models of programs, Fundamentalnaya i prikladnaya matematika, vol. 19 (2014), no. 1, pp. 121—163 .

In this paper, we consider a problem of reduction of probabilistic transition systems (PTS) in order to reduce the complexity of model checking of such systems. The problem of model checking of a PTS is to calculate truth values of formulas of the probabilistic temporal logic PCTL in an initial state of the PTS. We introduce a concept of equivalence of states of a PTS, and represent an algorithm for removing equivalent states. A result of this algorithm is a PTS such that all its properties expressed by formulas of PCTL coincide with those of the original PTS .

1. Введение

1.1. Постановка задачи, мотивация и научная новизна В настоящей работе рассматривается задача редукции вероятностных систем переходов (ВСП), целью которой является понижение сложности верификации свойств ВСП, выражаемых формулами вероятностной темпоральной логики PCTL .

Фундаментальная и прикладная математика, 2014, том 19, № 1, с. 121—163 .

c 2014 Изд

–  –  –

ВСП представляют собой один из наиболее широко используемых классов моделей дискретных динамических систем. Понятие ВСП является обобщением понятия цепи Маркова [2], имеющего широкие применения в естественных и гуманитарных науках. Понятие ВСП можно рассматривать также как частный случай понятия вероятностного автомата [1]. Главным отличием понятия ВСП от понятий цепи Маркова и вероятностного автомата является наличие выразительного логического формализма, позволяющего эффективно описывать различные свойства поведения ВСП. В качестве такого формализма выступает вероятностная темпоральная логика PCTL [13, 19], которая представляет собой вероятностный аналог темпоральной логики ветвящегося времени CTL [3], использующейся для спецификации свойств параллельных и распределённых программ, и является эффективным инструментом для описания различных свойств дискретных вероятностных динамических систем .

Формулы логики PCTL могут отражать различные вероятностные аспекты поведения анализируемых систем, к числу которых относятся, например,

• частота выполнения тех или иных действий или переходов в анализируемых системах;

• вероятность отказа компонентов анализируемых систем;





• вероятностный характер взаимодействия анализируемой системы с её окружением: частота поступления входных запросов или сообщений, частота получения искажённых сообщений (для протоколов передачи сообщений в компьютерных сетях) и т. п .

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

Результат верификации вероятностной модели анализируемой системы может отличаться от свойств исходной системы, и одной из актуальных научных задач является оценка степени расхождения свойств исходной системы и свойств её вероятностной модели. Однако эта задача не является предметом данного исследования. В настоящей работе мы рассматриваем следующую задачу. Мы предполагаем, что вероятностная модель анализируемой системы уже построена, и требуется преобразовать её в такую модель, чтобы задача анализа свойств исходной системы, выражаемых в виде формул вероятностной темпоМинимизация вероятностных моделей программ ральной логики, допускала более простое решение для редуцированной модели, а результаты верификации исходной и редуцированной модели были одинаковы .

Некоторые подходы к редукции ВСП изучались в различных работах по вероятностной верификации, однако в этих исследованиях были рассмотрены лишь частные методы редукции ВСП, такие, как редукция частичных порядков [5, 7] и редукция, основанная на понятии симметрии множества состояний ВСП [11, 17]. Данные методы можно эффективно использовать лишь для ВСП достаточно специального вида, как правило, это вероятностные модели параллельных и распределённых программ .

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

1.2. Исторический обзор и современное состояние дел в области верификации вероятностных систем переходов Верификация вероятностных систем переходов в настоящее время является одним из наиболее широко используемых методов верификации вычислительных систем. Главным достоинством этого метода является возможность полностью автоматического анализа модели верифицируемой системы. К числу его существенных недостатков относится высокая вычислительная сложность процедуры верификации .

Первые алгоритмы вероятностной верификации были предложены в 1980-е годы в [10,14,22]. Данные алгоритмы были предназначены для верификации качественных вероятностных свойств, т. е. таких свойств, которые выполняются с вероятностью 1 или 0. Затем эти алгоритмы были обобщены на случай верификации количественных вероятностных свойств (в спецификации таких свойств могло присутствовать любое значение вероятности). Эти алгоритмы были изложены в [8,9,13]. Программные реализации этих алгоритмов были представлены в [6, 12] .

Первые промышленные системы вероятностной верификации были разработаны в 2000-х годах [4, 15]. Эти системы вероятностной верификации успешно применяются во многих областях, в том числе в анализе распределённых алгоритмов, телекоммуникационных протоколах, компьютерной безопасности, криптографических протоколах, при моделировании биологических процессов .

С использованием этих систем верификации были обнаружены уязвимости и аномальные поведения анализируемых систем (подробнее см. в [16, 20]). При помощи систем вероятностной верификации могут быть вычислены такие характеристики программных систем, как, например, вероятность вторжения злоумышленника в компьютерную сеть, математическое ожидание времени отклика веб-сервиса, а также другие количественные и качественные характеристики .

124 А. М. Миронов, С. Л. Френкель Наиболее популярной практической системой вероятностной верификации в настоящее время является система PRISM [18, 20], разработанная на факультете компьютерных наук Оксфордского университета (Великобритания) в группе «Количественный анализ и верификация» под руководством Марты Квятковской [21] .

1.3. Структура статьи В разделе 2 мы определяем основное понятие настоящей работы — вероятностную систему переходов (ВСП) — и приводим два простых примера ВСП .

В разделе 3 мы вводим представление ВСП в терминах случайных функций и матриц. В разделе 4 мы описываем логику PCTL и определяем её семантику (т. е. правила вычисления значений формул логики PCTL в состояниях ВСП) .

Раздел 5 является центральным: здесь мы излагаем метод редукции ВСП, для чего вводим понятие эквивалентности состояний и описываем алгоритм вычисления классов эквивалентности на множестве состояний анализируемой ВСП .

Также мы излагаем алгоритм преобразования ВСП, связанный с удалением избыточных состояний, и обосновываем его корректность. В разделах 6 и 7 мы рассматриваем практические иллюстрации изложенного метода редукциии ВСП. В заключении мы формулируем актуальные проблемы для дальнейших исследований в области вероятностной верификации .

2. Вероятностные системы переходов

2.1. Понятие вероятностной системы переходов Мы предполагаем, что задано конечное множество AP, элементы которого называются атомарными утверждениями. Ниже запись 2AP обозначает множество всех подмножеств AP .

Вероятностная система переходов (ВСП) — это четвёрка D вида D = (S, s0, P, L), (1) компоненты которой имеют следующий смысл .

1. S — конечное множество, элементы которого называются состояниями ВСП D .

2. s0 S — выделенное состояние, называемое начальным состоянием ВСП D .

3. P — функция вида P : S S [0, 1], называемая функцией перехода ВСП D и удовлетворяющая условию

–  –  –

Состояния этой ВСП имеют следующий смысл .

— В состоянии s0 агент начинает очередной сеанс .

— В состоянии s1 агент предпринимает попытку выполнения действия (переход s1 s1 означает, что попытка выполнения действия пока неосуществима) .

— В состоянии s2 агент находится тогда, когда действие было выполнено успешно .

— В состоянии s3 агент оказывается тогда, когда попытка выполнения действия закончилась неудачей .

–  –  –

Мы будем называть X областью определения СФ f, а Y — областью значений СФ f .

Для каждого конечного множества X запись idX обозначает детерминированную СФ X X, которая отображает каждый x X в x .

–  –  –

Согласно определению произведения матриц из (9) следует, что матрица f · g является произведением матриц f и g .

3.3. Матрицы, соответствующие вероятностным системам переходов Пусть задана ВСП D = (S, s0, P, L), и список элементов множества S имеет вид (s1,..., sn ) .

Минимизация вероятностных моделей программ

–  –  –

def def определяемую индуктивно: P 0 = idS, P n+1 = P n · P для каждого n 0 .

Нетрудно убедиться, что матрицы, соответствующие СФ P i, имеют следующий вид: P 0 — единичная матрица и для каждого n 0 матрица P n является n-й степенью матрицы P .

Для любых n 0, s1, s2 S число P n (s1, s2 ) можно понимать как вероятность того, что если в текущий момент времени ВСП D находится в состоянии s1, то через n тактов времени D будет находиться в состоянии s2 .

4. Логика PCTL

4.1. Свойства вероятностных систем переходов Логика PCTL (её название является аббревиатурой англоязычного названия «Probabilistic Computation Tree Logic») — это темпоральная логика, предназначенная для формального описания свойств ВСП. Логика PCTL была введена в [13] .

Приведём несколько примеров свойств ВСП, которые могут быть описаны в виде формул логики PCTL .

1. Вероятность доставки сообщения в заданном временном интервале [t1, t2 ] не меньше 0,999 .

2. В результате работы алгоритма избрания процесса-лидера избрание такого процесса завершится с вероятностью 1 .

3. Вероятность успешной атаки на криптографический протокол не превышает 0,0001 % .

4.2. Формулы логики PCTL В определении понятия формулы логики PCTL мы будем использовать множество AP атомарных утверждений, введённое в разделе 2.1 .

Формулы логики PCTL делятся на два класса: StateFm — формулы состояний, PathFm — формулы путей. Формулы из классов StateFm и PathFm мы 130 А. М. Миронов, С. Л. Френкель будем обозначать через и соответственно (возможно, с индексами), а формулу произвольного вида — через f (возможно, с индексом) .

Классы StateFm и PathFm определяются следующим образом .

StateFm .

1. Каждое атомарное утверждение p из AP является формулой из StateFm .

и является формулами из StateFm. Данные символы обоСимволы значают тождественно истинное и тождественно ложное утверждение соответственно .

3. Если 1 и 2 — формулы из StateFm, то следующие знакосочетания являются формулами из StateFm:

¬1, 1 2, 1 2, 1 2, 1 2 .

4. Если — функциональный символ, которому соответствует функция (обозначаемая тем же символом) вида : [0, 1] [0, 1] {0, 1}, a — число из [0, 1] и — формула из PathFm, то знакосочетание P a является формулой из StateFm .

PathFm .

1. Если f — формула логики PCTL, то знакосочетание Xf является формулой из PathFm .

2. Если 1 и 2 — формулы из StateFm, то следующие знакосочетания являются формулами из PathFm: 1 U n 2, где n — натуральное число, 1 U 2 .

3. Если — формула из PathFm, то знакосочетание ¬ является формулой из PathFm .

В записи формул из PathFm могут использоваться символы F и G, которые являются сокращением знакосочетаний U и ¬F¬ соответственно (т. е., например, знакосочетания F и G n обозначают формулы U и ¬F n ¬ соответственно) .

4.3. Значения формул логики PCTL в состояниях вероятностных систем переходов Пусть D = (S, s0, P, L) — некоторая ВСП .

Для каждого состояния s S и каждой формулы f логики PCTL определено значение формулы f в состоянии s, обозначаемое s(f ). Если f StateFm, то s(f ) {0, 1} и в случае s(f ) = 1 формула f считается истинной в s, в случае s(f ) = 0 формула f считается ложной в s. Если f PathFm, то значение s(f ) является числом из [0, 1] и интерпретируется как вероятность того, что формула f истинна в состоянии s .

Минимизация вероятностных моделей программ

–  –  –

4.4. Смысл формул логики PCTL Формулы логики PCTL представляют собой утверждения, выражающие различные свойства ВСП. Эти свойства могут выражать, например, динамические аспекты поведения ВСП, т. е. описывать зависимость истинности какого-либо утверждения в некотором состоянии s рассматриваемой ВСП от истинности другого утверждения в состояниях, достижимых из s .

Смысл формул состояний логики PCTL непосредственно усматривается из определения значений этих формул в состояниях .

Смысл формул путей логики PCTL можно описать следующим образом .

1. Формулу X можно интерпретировать как утверждение «в следующий момент времени будет верно », а значение формулы X в состоянии s — как вероятность того, что будет истинна в произвольном состоянии, в которое можно перейти из s за один такт времени .

2. Значение формулы 1 U n 2 в состоянии s можно интерпретировать как вероятность того, что для произвольного пути, выходящего из s, существует состояние s, такое что длина начального отрезка [s, s ] пути не превосходит n и в каждом состоянии этого отрезка, кроме, может быть, s, верна формула 1, а в состоянии s верна формула 2 .

3. Значение формулы 1 U 2 в состоянии s можно интерпретировать так же, как значение предыдущей формулы, без упоминания того, что длина [s, s ] не превосходит n .

4.5. Пример формулы логики PCTL, выражающей свойство вероятностной системы переходов В этом разделе мы приведём пример формулы логики PCTL, выражающей одно из свойств первого протокола из раздела 2.3 (представленного ВСП (6)) .

Данное свойство заключается в том, что каждое сообщение, полученное отправителем от внешнего источника, будет с вероятностью не меньше 0,9 доставлено получателю не более чем за пять шагов .

Для формального представления этого свойства мы будем предполагать, что среди атомарных утверждений имеются утверждения, комбинации значений которых соответствуют состояниям ВСП. Обозначим эти утверждения записями Минимизация вероятностных моделей программ

–  –  –

где символ обозначает функцию вида : [0, 1] [0, 1] {0, 1}, которая ставит в соответствие паре (a, b) [0, 1] [0, 1] элемент 1, если a b, и 0 иначе .

5. Метод редукции вероятностных систем переходов

5.1. Задача редукции вероятностных систем переходов Если анализируемая ВСП имеет большой размер, то анализ её свойств, выражаемых формулами логики PCTL (т. е. вычисление значений формул логики PCTL в состояниях этой ВСП), может быть связан с трудновыполнимыми требованиями к вычислительным ресурсам, с использованием которых производится этот анализ. В связи с этим представляет большую актуальность проблема редукции ВСП, т. е. удаления части состояний и переходов анализируемой ВСП с таким расчётом, чтобы получившаяся ВСП была эквивалентна исходной в следующем смысле: для каждой формулы состояний f логики PCTL формула f истинна в начальном состоянии исходной ВСП тогда и только тогда, когда она истинна в начальном состоянии редуцированной ВСП .

Основная идея предлагаемого в настоящей работе метода редукции ВСП основана на понятии эквивалентности состояний ВСП. Мы называем состояния эквивалентными, если значения всех формул логики PCTL в этих состояниях совпадают. Алгоритм редукции ВСП представляет собой вычисление классов эквивалентности состояний анализируемой ВСП и удалении эквивалентных состояний .

134 А. М. Миронов, С. Л. Френкель

–  –  –

Мы будем называть состояния s1 S1 и s2 S2 эквивалентными, если для каждой формулы f логики PCTL верно равенство s1 (f ) = s2 (f ) .

Если состояния s1 и s2 эквивалентны, то мы будем обозначать этот факт записью s1 s2 .

Мы будем называть ВСП D1 и D2 вида (10) эквивалентными, если s0 s0 .

Если ВСП D1 и D2 эквивалентны, то мы будем обозначать этот факт D1 D2 .

Если ВСП D1 и D2 совпадают и S — множество их состояний, то бинарное отношение на S, состоящее из всех пар (s1, s2 ), таких что s1 s2, является отношением эквивалентности. Мы будем обозначать это отношение через .

Отношение может быть найдено при помощи алгоритма, излагаемого в разделе (5.4). Для обоснования этого алгоритма мы введём необходимые понятия и докажем несколько вспомогательных утверждений .

5.3. Вспомогательные понятия и утверждения 5.3.1. Эквивалентности и связанные с ними разбиения множества состояний Пусть заданы ВСП D = (S, s0, P, L) и некоторое множество Fm формул логики PCTL. Мы будем обозначать (Fm) бинарное отношение на S, определяемое следующим образом:

def (Fm) = {(s1, s2 ) S 2 | s1 (f ) = s2 (f ) для каждого f Fm} .

Нетрудно убедиться, что (Fm) — отношение эквивалентности и

–  –  –

Докажем (22). Поскольку все компоненты матрицы P и вектора j неотрицательны, то все компоненты вектора P · j (который совпадает с (21)) тоже неотрицательны. Однако совокупность компонентов вектора (21) совпадает с множеством {a1j,..., akj }, так как в каждой строке матрицы один элемент равен 1, а все остальные элементы равны 0 и для каждого j {1,..., k} найдётся s S, такой что элемент в строке s и столбце Sj матрицы равен 1 .

Утверждение (23) можно переформулировать в виде равенства · 1 = 1, где 1 — вектор-столбец, все компоненты которого равны 1. Данное равенство следует из цепочки равенств · ( · 1 ) = ( · ) · 1 = (P · ) · 1 = P · ( · 1 ) = P · 1 = 1 и описанного в предыдущем пункте свойства матрицы .

Ниже мы будем обозначать через PCTL совокупность всех формул логики PCTL .

Лемма 5. Для любой ВСП D = (S, s0, P, L) разбиение множества S, соответствующее эквивалентности (PCTL), совместимо с функцией перехода P .

Доказательство. Пусть имеет вид {S1,..., Sk } и 1,..., k — столбцы матрицы, которая соответствует детерминированной СФ : S .

r

–  –  –

имеет одинаковые компоненты, соответствующие состояниям из одного из того же класса разбиения, т. е. вектор P ·j является линейной комбинацией векторов 1,..., k. Согласно лемме 4 отсюда следует, что совместимо с функцией перехода P .

Теорема 1. Пусть заданы ВСП D = (S, s0, P, L) и множество Fm формул логики PCTL, содержащее все атомарные утверждения из AP .

Тогда следующие утверждения эквивалентны :

1) разбиение, соответствующее (Fm), совместимо с P ;

2) (Fm) = (PCTL) .

Доказательство. Импликация 2) = 1) следует из леммы 5 .

Докажем импликацию 1) = 2). Поскольку Fm PCTL, то (PCTL) (Fm) .

Согласно (11) для доказательства обратного включения достаточно доказать, что для каждой формулы f логики PCTL верно включение (Fm) (f ). (25) Докажем это включение индукцией по структуре формулы f .

Если f AP, то (25) следует из предположения AP Fm .

Предположим, что для каждой подформулы f формулы f верно включение (25), в котором f заменено на f. Докажем, что в этом случае будет верно включение (25) .

Пусть f является булевой комбинацией. Рассмотрим, например, случай f = ¬f. Если (s1, s2 ) (Fm), то s1 (f ) = s1 (¬f ) = 1 s1 (f ) = 1 s2 (f ) = s2 (¬f ) = s2 (f ) .

Другие случаи возможного вида f, когда f является булевой комбинацией, рассматриваются аналогично .

Пусть f = P a. Если (s1, s2 ) (Fm), то s1 (f ) = (s1 (), a) = (s2 (), a) = s2 (f ) .

Для рассмотрения остальных возможных вариантов вида f мы введём дополнительные обозначения. Обозначим через разбиение, соответствующее отношению эквивалентности (Fm). Пусть состоит из классов S1,..., Sk .

Заметим, что включение (25) равносильно утверждению s1 (f ) = s2 (f ) для любых j = 1,..., k, s1, s2 Sj. (26)

Нетрудно убедиться, что (26) можно переформулировать следующим образом:

найдётся S(f ), такой что S(f ) = · S(f ), (27) где — матрица, соответствующая СФ (18) .

Минимизация вероятностных моделей программ

–  –  –

5.4. Редукция вероятностных систем переходов 5.4.1. Задача редукции ВСП Пусть задана ВСП D = (S, s0, P, L). Задача редукции ВСП D заключается в построении ВСП D, которая эквивалентна D и число состояний которой меньше, чем число состояний ВСП D .

Излагаемый в настоящем разделе алгоритм редукции ВСП является вероятностным обобщением алгоритма редукции детерминированных автоматов.

Идея данного алгоритма основана на отождествлении неразличимых состояний ВСП:

Минимизация вероятностных моделей программ — алгоритм вычисляет классы эквивалентности S1,..., Sk множества S, соответствующие разбиению (P CT L), — ВСП D преобразуется путём удаления состояний в классах эквивалентности S1,..., Sk (и соответствующего переопределения функции перехода) до тех пор, пока не останется по одному состоянию в каждом из этих классов .

В результате этих удалений получается искомая ВСП D .

–  –  –

(каждый из которых, как легко заметить, является суммой некоторых столбцов матрицы P : для каждого j = 1,..., k вектор-столбец (38) является суммой таких столбцов s матрицы P, для которых s Sj ) — классы разбиения i+1 получаются путём измельчения классов разбиения i : в один и тот же класс разбиения i+1 попадают такие состояния, для которых соответствующие им компоненты векторов (38) совпадают для каждого j = 1,..., k .

142 А. М. Миронов, С. Л. Френкель

–  –  –

2. i = i+1. В этом случае мы увеличиваем i на 1 и возвращаемся в начало цикла (т. е. выполняем шаг 2 с увеличенным значением i) .

Нетрудно убедиться, что таких возвращений может быть не больше количества элементов множества S (так как разбиение i+1 является измельчением разбиения i ) .

5.4.3. Удаление эквивалентных состояний из вероятностных систем переходов

–  –  –

Поскольку состояния s1 и s2 по предположению эквивалентны, то по определению понятия эквивалентности состояний верно равенство s1 (f ) = s2 (f ) .

Следовательно, (47) совпадает с SD (f ) .

Из приведённых утверждений следует, что левая часть доказываемого равенства (46) совпадает с его правой частью, что и требовалось доказать .

4. Пусть f = 1 U n 2. Обозначим эту формулу через n. Докажем индукцией по n, что SD1 (n ) = SD (n ) \ s1 .

Если n = 0, то по определению S(n ) = S(2 ) и доказываемое утверждение верно потому, что 2 — подформула формулы f .

Если n 0, то по определению S(n ) = max S(2 ), S(1 ) S(Xn1 ) и истинность доказываемого утверждения следует из его истинности для 1, 2, n1 и Xn1, а также из определения операций max и на вектор-столбцах .

5. Пусть f = 1 U2. Согласно определению вектор-столбцы SD (f ) и SD1 (f ) удовлетворяют соотношениям

–  –  –

5.4.4. Описание алгоритма редукции ВСП Теорема 2 является обоснованием излагаемого ниже алгоритма редукции ВСП D = (S, s0, P, L). Этот алгоритм имеет следующий вид .

–  –  –

6. Пример редукции вероятностной системы переходов В этом разделе мы рассмотрим пример использования предложенного в настоящей работе алгоритма редукции ВСП .

6.1. Описание редуцируемой ВСП ВСП, рассматриваемая в этом примере, является вероятностной абстракцией последовательной незавершающейся программы, представляемой блок-схемой

–  –  –

где символы A0, A1, A2, A3 рядом с условными операторами можно рассматривать как имена данных операторов .

Программа содержит булевы переменные p, u, v (которые мы будем рассматривать как существенные переменные данной блок-схемы) и некоторые другие переменные, не указанные на данной блок-схеме (их мы будем рассматривать как несущественные переменные данной блок-схемы). В условных операторах данной блок-схемы используются булевозначные выражения B0 и т. д., в каждом из которых в скобках указаны лишь существенные переменные, от которых зависит данное булевозначное выражение .

Значения переменных p, u и v изменяются операторами присваивания, в правой части которых стоит терм, зависящий от u, v и других переменных блок-схемы. Операторы присваивания, которые изменяют значения переменных, отличных от p, u и v, не принимаются во внимание и изображены многоточием .

Предположим, что анализируется какое-либо частное свойство данной блок-схемы, связанное со статистическими закономерностями изменения значения переменной p. Для анализа свойства данного типа мы построим ВСП, являющуюся вероятностной абстракцией данной блок-схемы .

Процесс функционирования данной блок-схемы можно интерпретировать как процесс перехода от одного условного оператора Ai к другому оператору Aj с выполнением операторов присваивания, которые встречаются на пути от Ai к Aj, т. е .

переходе от A0 к A1 выполняются операторы присваивания — при..., u : = e11, v : = e12, p : = 1, переходе от A0 к A2 выполняются операторы присваивания — при..., u : = e21, v : = e22, p : = 0 — и т. д .

Напомним (см. [3]), что полная диаграмма состояний, соответствующая блок-схеме, представляет собой граф, вершины которого отвечают состояниям блок-схемы, где под состоянием понимается набор значений, поставленных в соответствие переменным блок-схемы, а также управляющей переменной, которая не входит в число переменных блок-схемы и значениями которой являются операторы блок-схемы .

Построим упрощённую диаграмму состояний данной блок-схемы, соответствующую такому уровню абстракции, при котором из переменных блок-схемы мы будем учитывать лишь переменные p, u и v и множество значений управляющей переменной будем считать равным {A0, A1, A2, A3 } (принимая во внимание высказанное выше замечание о том, что каждый шаг функционирования блок-схемы можно интерпретировать как переход от оператора вида Ai к оператору вида Aj с выполнением присваиваний, находящихся на пути от Ai к Aj ) .

Таким образом, при выбранном уровне абстракции диаграмма состояний должна содержать 2 · 2 · 2 · 4 состояний. Однако из визуального анализа блок-схемы мы можем заключить, что значение переменной p однозначно определяется значением управляющей переменной (в операторах A0 и A2 значение p равно 0, Минимизация вероятностных моделей программ

–  –  –

В этой ВСП множество AP атомарных утверждений состоит из одного утверждения p, т. е. множество 2AP состоит из двух элементов: и {p}. Мы будем обозначать эти элементы символами 0 и 1 соответственно .

Начальным состоянием данной ВСП является состояние s0, оно обозначено двойным кружком. Рядом с каждым состоянием s приписана метка, которая равна значению L(s) .

Матрицу P, соответствующую данной ВСП, мы представим в виде следующей таблицы:

–  –  –

Левый столбец и верхняя строка в этой таблице не являются элементами матрицы P, они предназначены для интерпретации коэффициентов в этой таблице:

для каждой пары состояний (si, sj ) S S значение P (si, sj ) располагается в пересечении строки, содержащей si, и столбца, содержащего sj .

6.2. Вычисление эквивалентности (PCTL) для редуцируемой ВСП Вычисление эквивалентности (P CT L) для ВСП (56) происходит следующим образом .

1. Вычисляется отношение эквивалентности 0, которое состоит из всех пар (s1, s2 ) S S, удовлетворяющих равенству L(s1 ) = L(s2 ) .

Нетрудно убедиться, что 0 состоит из двух классов

–  –  –

По матрице (60) нетрудно вычислить отношение 1 и соответствующее ему разбиение 1. Из определения отношения 1 непосредственно следует, что состояния s1 и s2 находятся в одном и том же классе разбиения 1 тогда и только тогда, когда они оба находятся в одном и том же классе из списка (59), и, кроме того, строки матрицы (60), соответствующие состояниям s1 и s2, совпадают .

Разбиение 1 будет состоять из трёх классов (измельчится первый класс в (59), а второй класс останется тем же), эти классы имеют следующий вид:

–  –  –

3. Затем вычисляется матрица 1, соответствующая детерминированной СФ : S 1. Она будет иметь следующий вид:

r 8 0 1 0 .

Произведение P · 1 имеет следующий вид:

–  –  –

Принимая во внимание ограничения (58), данную матрицу можно упростить до 0 0 1/2 1/2 4 1/2 0 1/2 5 1/2 0 1/2 8 0 0 1 .

После этого, действуя аналогично предыдущему пункту, вычисляем классы разбиения 2, соответствующего эквивалентности 2.

Таких классов будет четыре (измельчится третий класс в (61), а первый и второй классы останутся теми же), эти классы имеют следующий вид:

–  –  –

Принимая во внимание ограничения (58), данную матрицу можно упростить до 1/2 1/2 1 0 0 1/2 1/2 3 0 0 1/2 1/2 4 1/2 0 0 1/2 5 1/2 0 0 1/2 6 0 0 1/2 1/2 8 0 0 1/2 1/2. (63) После этого, действуя аналогично предыдущему пункту, вычисляем классы разбиения 3, соответствующего эквивалентности 3. Нетрудно проверить, что классы разбиения 3 будут иметь точно такой же вид, что и классы эквивалентности разбиения 2. Это означает, что искомое разбиение множества S на классы эквивалентных состояний построено, оно имеет вид (62) .

6.3. Удаление избыточных состояний Теперь можно приступить к удалению избыточных состояний (чтобы среди оставшихся состояний было ровно по одному состоянию из каждого класса эквивалентности (62)). Нетрудно убедиться, что можно удалить состояния s3, s6, s8, s7, s5 .

156 А. М. Миронов, С. Л. Френкель

1. Удаление состояния s3. Совокупность всех рёбер ВСП (57) с концом s3 и ненулевыми метками имеет следующий вид: ребро из s0 в s3 с меткой b2 /2 и ребро из s5 в s3 с меткой u1 /2. В соответствии с алгоритмом к меткам рёбер из s0 в s1 и из s5 в s1 мы прибавляем b2 /2 и u1 /2 соответственно и удаляем состояние s3 и все связанные с ним рёбра. После удаления состояния s3 и связанных с ним рёбер ВСП (57) примет следующий вид:

–  –  –

2. Удаление состояния s6. Совокупность всех рёбер ВСП (64) с концом s6 и ненулевыми метками имеет следующий вид: ребро из s0 в s6 с меткой b4 /2 и ребро из s4 в s6 с меткой v2 /2. В соответствии с алгоритмом к меткам рёбер из s0 в s1 и из s4 в s1 мы прибавляем b4 /2 и v2 /2 соответственно и удаляем состояние s6 и все связанные с ним рёбра. Принимая во внимание соотношение v1 +v2 = 1, получаем, что после удаления состояния s6 и связанных с ним рёбер

ВСП (64) будет иметь следующий вид:

Минимизация вероятностных моделей программ

–  –  –

свидетельствует о пользе предложенного в настоящей работе подхода редукции анализируемой ВСП перед вычислением значений формул логики PCTL в её состояниях .

8. Заключение В настоящей работе изложен алгоритм редукции вероятностных систем переходов, идея которого заключается в удалении избыточных состояний. Отметим, что в результате такой редукции может получиться ВСП, которая, хотя и не содержит различных эквивалентных состояний, может не являться минимальной по числу состояний среди всех ВСП, эквивалентных исходной ВСП. В связи с этим встаёт вопрос об алгоритме нахождения минимальной по числу состояний ВСП, эквивалентной заданной ВСП, и исследовании единственности такой минимальной ВСП (с точностью до подходящим образом сформулированного понятия изоморфизма). Также представляет интерес исследование проблем минимизации других классов моделей, связанных с вероятностной верификацией, в частности минимизации марковских решающих процессов .

Кроме этих задач, для вероятностной верификации актуальны все задачи, связанные с классической теорией Model Checking, в частности — разработка методов верификации ВСП «на лету» (см. [3]), т. е. методов, связанных с построением тех фрагментов ВСП, которых достаточно для проверки анализируемого свойства;

— построение символьных методов вероятностной верификации (в том числе нахождение аналогов понятия бинарных разрешающих диаграмм [3] для ВСП) .

Литература [1] Бухараев Р. Г. Основы теории вероятностных автоматов. — М.: Наука, 1985 .

[2] Кемени Дж., Снелл Дж. Конечные цепи Маркова. — М.: Наука, 1970 .

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

[4] De Alfaro L., Kwiatkowska M., Norman G., Parker D., Segala R. Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation // Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00) / S. Graf, M. Schwartzbach, eds. — Berlin: Springer, 2000. — (Lect. Notes Comput. Sci.; Vol. 1785). — P. 395—410 .

[5] D’Argenio P., Niebert P. Partial order reduction on concurrent probabilistic programs // Proc. 1st Int. Conf. on Quantitative Evaluation of Systems (QEST’04). — IEEE Comput. Sci. Press, 2004. — P. 240—249 .

[6] Baier C., Clarke E., Hartonas-Garmhausen V., Kwiatkowska M., Ryan M. Symbolic model checking for probabilistic processes // Proc. 24th Int. Colloq. on Automata, 162 А. М. Миронов, С. Л. Френкель Languages and Programming (ICALP’97) / P. Degano, R. Gorrieri, A. Marchetti-Spaccamela, eds. — Berlin: Springer, 1997. — (Lect. Notes Comput. Sci.; Vol. 1256). — P. 430—440 .

[7] Baier C., Gr sser M., Ciesinski F. Partial order reduction for probabilistic systems // o Proc. 1st Int. Conf. on Quantitative Evaluation of Systems (QEST’04). — IEEE Comput .

Sci. Press, 2004. — P. 230—239 .

[8] Baier C., Haverkort B., Hermanns H., Katoen J.-P. Model-checking algorithms for continuous-time Markov chains // IEEE Trans. Software Engineering. — 2003. — Vol. 29, no. 6. — P. 524—541 .

[9] Bianco A., de Alfaro L. Model checking of probabilistic and nondeterministic systems // Proc. 15th Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’95) / P. Thiagarajan, ed. — Berlin: Springer, 1995. — (Lect. Notes Comput. Sci.; Vol. 1026). — P. 499—513 .

[10] Courcoubetis C., Yannakakis M. Verifying temporal properties of nite state probabilistic programs // Proc. 29th Annual Symp. on Foundations of Computer Science (FOCS’88). — IEEE Comput. Soc. Press, 1988. — P. 338—345 .

[11] Donaldson A., Miller A. Symmetry reduction for probabilistic model checking using generic representatives // Proc. 4th Int. Symp. Automated Technology for Verication and Analysis (ATVA’06) / S. Graf, W. Zhang, eds. — Berlin: Springer, 2006. — (Lect .

Notes Comput. Sci.; Vol. 4218). — P. 9—23 .

[12] Hansson H. Time and Probability in Formal Design of Distributed Systems. — Amsterdam: Elsevier, 1994 .

[13] Hansson H., Jonsson B. A logic for reasoning about time and reliability // Formal Aspects Computing. — 1994. — Vol. 6, no. 5. — P. 512—535 .

[14] Hart S., Sharir M., Pnueli A. Termination of probabilistic concurrent programs // ACM Trans. Programming Languages Systems. — 1983. — Vol. 5, no. 3. — P. 356—380 .

[15] Hermanns H., Katoen J.-P., Meyer-Kayser J., Siegle M. A Markov chain model checker // Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00) / S. Graf, M. Schwartzbach, eds. — Berlin: Springer, 2000. — (Lect. Notes Comput. Sci.; Vol. 1785). — P. 347—362 .

[16] Kwiatkowska M., Norman G., Parker D. Probabilistic model checking in practice:

Case studies with PRISM // ACM SIGMETRICS Performance Evaluation Review. — 2005. — Vol. 32, no. 4. — P. 16—21 .

[17] Kwiatkowska M., Norman G., Parker D. Symmetry reduction for probabilistic model checking // Proc. 18th Int. Conf. on Computer Aided Verication (CAV’06) / T. Ball, R. Jones, eds. — Berlin: Springer, 2006. — (Lect. Notes Comput. Sci.; Vol. 4114). — P. 234—248 .

[18] Kwiatkowska M., Norman G., Parker D. PRISM 4.0: Verication of probabilistic real-time systems // Proc. 23rd Int. Conf. on Computer Aided Verication (CAV’11) / G. Gopalakrishnan, S. Qadeer, eds. — Berlin: Springer, 2011. — (Lect. Notes Comput .

Sci.; Vol. 6806). — P. 585—591 .

[19] Kwiatkowska M., Parker D. Advances in Probabilistic Model Checking. — http:// qav.comlab.ox.ac.uk/papers/marktoberdorf11.pdf .

[20] http://www.prismmodelchecker.org/ .

[21] http://qav.comlab.ox.ac.uk/ .

Минимизация вероятностных моделей программ [22] Vardi M. Automatic verication of probabilistic concurrent nite state programs // Proc. 26th Annual Symp. on Foundations of Computer Science (FOCS’85). — IEEE Comput. Soc. Press, 1985. — P. 327—338 .





Похожие работы:

«Учреждение образования "Белорусский государственный университет информатики и радиоэлектроники" УТВЕРЖДАЮ Проректор по учебной работе Е.Н. Живицкая 20.03.2017 Регистрационный № УД-5-686/р "Проектирование и разработка информационных систем" Учебн...»

«Беспроводная мышь А4 TECH c технологией “V-Track” Работает без коврика на любой поверхности модель: G9-500F www.a4-gcube.ru Подготовка к работе 1. Извлеките приемник, который закреплен в основании мыши и подключите его к USB-порту компьютера.2. Установите бат...»

«ДОГОВОР № г. Санкт-Петербург " 2014 года " Закрытое акционерное общество "Петроэлектросбыт", именуемое в дальнейшем "Заказчик", в лице Генерального директора Горшковой Е.С., действующей на основании Устава, с одной стороны, и общество...»

«Темы Дипломных проектов Информационные системы и технологии Информационные системы и технологии в телекоммуникациях Внедрения беспроводного сегмента в ЛВС вашего предприятия; 1 . Обеспечения защищённого удалённого доступа к информационным ресурсам ЛВС...»

«Доклад по теме: Администрирование локальных сетей. Жгулев С.В. Королев 2003 Администрирование локальных сетей. 2 Оглавление . Администрирование локальных сетей Удаленное управление Управление питанием Установка Настройка Управление Полный контроль Обзор Remote Administra...»

«Основы информатики и математики Д. В. Иванов, А. С. Карпов, Е. П. Кузьмин, В. С. Лемпицкий, А. А. Хропов АЛГОРИТМИЧЕСКИЕ ОСНОВЫ РАСТРОВОЙ МАШИННОЙ ГРАФИКИ Учебное пособие Допущено учебно-методическим советом по прикладной математике и информат...»

«Рынок марганцевых сплавов – 2009 – сентябрь ООО Инфометгео / Александр Терешин Информационный обзор РЫНОК МАРГАНЦЕВЫХ СПЛАВОВ – 3кв. 2009 Москва 2009 © ООО Инфометгео / Александр Терешин / http://www.infogeo.ru/metalls, post@infogeo.ru 1 Рынок марганцевых с...»







 
2019 www.mash.dobrota.biz - «Бесплатная электронная библиотека - онлайн публикации»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.