«АЛГОРИТМЫ ВЫЧИСЛЕНИЯ ОТНОШЕНИЙ ПОДОБИЯ В ЗАДАЧАХ ВЕРИФИКАЦИИ И РЕСТРУКТУРИЗАЦИИ ПРОГРАММ ...»

Понятие отношения симуляции между моделями программ было впер­ вые введено Миллнером (Millner) в 1971 году в работе [74]. Миллнер рассмат­ ривал симуляции только между детерменированными моделями программ и предлагал использовать эти отношения как формализм, позволящий прове­ рять эквивалентность программ на некотором уровне абстракции. Позднее, в 1980 году Миллнер обобщил это понятие симуляционной эквивалентности на случай недетерменированных программ и ввёл понятия строгой и слабой би­ симуляций [75]. В 1981 году Парк (Park) обобщил понятие симуляции на слу­ чай недетерменированных моделей программ, задаваемыми автоматами Бю­ хи [81]. Важным свойством отношения симуляции, по словам Парка, является то, что с одной стороны отношение симуляции является более сильным, чем широко используемое отношение трассового (языкового) включения [104], а с другой стороны, проверка выполнимости отношения симуляции является ал­ горитмически более простой задачей, чем задача проверки трассового вклю­ чения. В дальнейшем в литературе было приведено множество примеров ис­ пользования отношений симуляций. В частности, отношения симуляции ис­ пользовались в процессе инкрементального построения моделей, при котором каждая новая версия модели является уточнением предыдущей [21]. Кроме того, отношения симуляции могут использоваться для вычисления инвариан­ тов бесконечных параметризованных семейств моделей [65], для нахождения симметрии в моделях [106], для автоматического уменьшения размеров мо­ делей [20, 111], для проверки свойств конфиденциальности многопоточных программ [94].

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

Универсальная система проверки симуляций должна состоять из двух компо­ нент: формального языка, позволяющего описывать различные симуляции, и программно-инструментального средства, которое по двум размеченным си­ стемам переходов и описанию симуляции проверяет, выполняется ли заданная симуляция между этими системами переходов.

В качестве формализма задания моделей нами были выбраны струк­ туры Крипке (которые, фактически, являются конечными автоматами) по двум причинам. Во-первых, структуры Крипке используются во многих по­ пулярных средствах проверки моделей программ, в частности, в средствах NuSMV [77] и Spin [57]. С другой стороны, отношения симуляции между структурами Крипке достаточно хорошо исследованы, и для всех известных нам отношений симуляций на множестве структур Крипке существуют алго­ ритмы их проверки.

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

Гибридные автоматы [1] являются удобным формализмом для описания так называемых гибридных систем, т. е. систем, в которых дискретные управ­ ляющие устройства взаимодействуют с непрерывным физическим окружени­ ем. Гибридный автомат состоит из системы переходов, каждое состояние кото­ рой снабжено системой дифференциальных уравнений над некоторым множе­ ством вещественных переменных. Вычисление гибридного автомата состоит из последовательности дискретных переходов, перемежаемой обновлениями значений вещественных переменных в соответствии с дифференциальными уравнениями.

Гибридные автоматы часто используются при имитационном моделиро­ вании, однако для формального анализа в общем виде они слишком сложны.

В частности, даже задача проверки достижимости заданного состояния в ги­ бридном автомате является алгоритмически неразрешимой [55].

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

Во временных автоматах системы дифференциальных уравнений, описываю­ щих изменения переменных, имеют вид = (1, 1,..., 1), т. е. все переменные растут с одинаковой скоростью. Таким образом, формализм временных авто­ матов является достаточно выразительным для описания систем, в которых единственным непрерывно изменяемым параметром являются часы. Для вре­ менных автоматов является разрешимой задача проверки достижимости за­ данного состояния [5], более того, для таких автоматов разрешима проблема проверки выполнимости формул темпоральной логики Timed CTL(TCTL) [4].

Временные автоматы также используются в качестве удобной математи­ ческой модели при решении задачи синтеза систем автоматического управле­ ния исходя из спецификации требуемого поведения устройства управления и возможного поведения среды [71]. Эта задача синтеза состоит в построении такого алгоритма работы устройства управления (контроллера), что объект управления будет корректно функционировать в независимости от действий среды. Например, автопилот должен вести самолёт по курсу вне зависимо­ сти от внешних условий. При решении этой задачи система автоматическо­ го управления может быть представлена автоматом, множество переходов которого состоит из переходов двух типов, контролируемых и неконтроли­ руемых устройством управления. Такой автомат фактически представляет собой описание игры двух участников — контроллера и внешней среды. И действительно, в работе [71] было показано, что задача синтеза работы кон­ троллера сводится к задаче нахождения его выигрышной стратегии в этой игре. В этой же работе было установлено, что задача синтеза разрешима для случая, когда цель контроллера — перевести систему за определённое вре­ мя из начального состояния в заданное состояние, избегая при этом попада­ ния в некоторые выделенные (аварийные) состояния (такие свойства можно задавать формулами логики ATCTL). Позже в работе [41] был предложен алгоритм решения этой задачи “на лету” (on-the-fly). Этот алгоритм был ре­ ализован в рамках среды UPPAAL Tiga [103], которая была использована в нескольких промышленных приложениях, в частности, компанией Skov A/S для автоматического синтеза контроллера для поддержания стабильной тем­ пературы в современных свино- и птицефермах [51]; и для автоматического синтеза контроллеров, управляющих автономным поведением роботов [84] (в обоих случаях осуществлялся контроль десятками параметров).

Отношения симуляции между временными автоматами не так хорошо исследованы, как отношения симуляции между конечными автоматами. Глав­ ной причиной этого является то, что временные автоматы имеют бесконеч­ ное число состояний (поскольку каждое состояние включает в себя значения вещественных переменных-часов), и поэтому разработка алгоритмов провер­ ки временных симуляций является сложной задачей. В то же время, поми­ мо перечисленных выше примеров применения симуляций между конечными автоматами существуют и специфические примеры применения отношений симуляции в задачах анализа временных игровых автоматов. В частности, отношения временных симуляций могут использоваться в случае, когда со­ стояние полной модели себя информацию о состоянии среды и/или объекта управления, которая не должна использоваться в алгоритме работы контроллера. Например, оно мо­ жет включать в себя информацию о местоположении робота в пространстве, однако контроллеру робота должны быть доступны только показания датчи­ ков, но не его точное местоположение. Чтобы решить задачу синтеза алго­ ритма работы контроллера в такой системе, можно разработать модель которую не будет входить информация о скрытом состоянии среды и объекта управления. Затем необходимо построить выигрышную стратегию контрол­ лера для модели A и проверить существование симуляции между A и S. Если эта симуляция выполняется, то из подобия моделей и что построенная выигрышная стратегия контроллера для A будет выигрыш­ ной и для S. Поскольку в данной стратегии используется только доступная контроллеру информация о состоянии среды и объекта управления, то эта стратегия может лежать в основе алгоритма работы контроллера.

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

Обнаружение подобных фрагментов в 1.1. Постановка задачи Из-за использования программистами операции copy&paste и других факторов в программах появляются большие похожие фрагменты кода, ко­ торые принято называть клонами. В литературе достаточно хорошо иссле­ дован феномен программных клонов (см., например, обзор [93]) и показано, что наличие большого числа клонов в программе приводит к увеличению стоимости её поддержки и к другим негативным факторам. К сожалению, в отличие от многих других широко используемых в программировании по­ нятий (например, процедуры, алгоритма) в настоящее время не существует строгого математического определения понятия клона. Но все исследователи сходятся в том, что клоном называются фрагменты, имеющие незначитель­ ные синтаксические отличия друг от друга.

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

Как указывается в обзоре [93], клоны могут быть удалены с использо­ ванием операций “Выделение метода” (Extract Method) и “Подъём метода” (Pull Up Method), изложенных в монографии Мартина Фаулера “Рефакто­ ринг: улучшение существующего кода” [121]. “Выделение метода” (в русско­ язычной литературе называемое процедурной абстракцией) заключается в s1: int fib(int n) { s5: for (i=0; i < n-1; i++) { выделении общего кода в новую функцию (или метод класса, если речь идёт об обьектно-ориентированном программировании). “Подъём метода” заклю­ чается в перемещении общего метода двух классов в их базовый класс. Если два класса не являются потомками одного базового класса, то перед опе­ рацией “Подъём метода” можно создать новый базовый класс при помощи операции “Выделение родительского класса” (Extract Superclass).

Опишем вид фрагментов кода, входящих в клон, который может быть легко удалён при помощи описанных методов рефакторинга. Понятно, что ми­ нимальным фрагментом кода, который может быть безболезненно выделен в отдельную функцию, является последовательность операторов (возможно, со­ стоящая из одного элемента). Из-за существования составных (и вложенных) операторов понятие последовательности операторов может быть истолковано неоднозначно, поэтому мы будем считать, что в клоны могут входить только линейные последовательности операторов. Рассмотрим фрагмент кода, изоб­ ражённый на рисунке 1.1. В соответствии с нашим определением, линейная последовательность операторов (s2, s3, s5) может входить в клон, а последо­ вательность (s4, s5) — нет, поскольку оператор s4 относится к блоку if, а оператор s5 находится на самом верхнем уровне тела функции.

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

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

Для примененимости операции “Выделение метода” мы можем допустить более широкие отличия одного фрагмента клона от другого, например, заме­ ну одной константы на другую или замену одного подвыражения на другое подвыражение. И подвыражения, и константы являются частными случая­ ми синтаксических единиц, т. е таких фрагментов кода, к которым может быть применено синтаксическое правило языка программирования. Напри­ мер, фрагменты “a+b” и “a” являются синтаксическими единицами, а фраг­ мент “a+” не является таковым. Легко видеть, что наиболее простыми для рефакторинга являются клоны, один фрагмент которых может быть полу­ чен из другого фрагмента путём замены одних синтаксических единиц на любые другие синтаксические единицы.

На рисунке 1.2 приведён пример такого клона и результат применения к нему операции “Выделение метода”. Видно, что первый фрагмент может быть получен из второго фрагмента заменой всех выражений вида b>>8 на OPC.

Это позволило провести процедурную абстракцию (применить “Выделение метода”) и заменить эти два фрагмента на вызов функции f, имеющей один Рисунок 1.2. Клон, удовлетворяющий определению, используемому в данной работе, и его процедурная абстракция жество {| () = 1} содержит все выигрышные состояния игрока Spoiler ранга 1. В самом деле, множество {| 1 () = 1} является множеством выигрышных состояний игрока Spoiler ранга 0, поскольку оно со­ держит все те игровые состояния игрока Duplicator, из которых он не может сделать переход. Справедливость индуктивного перехода является следстви­ ем того, что игровое состояние игрока Spoiler (соответственно Duplicator) является выигрышным ранга, где > 1, тогда и только тогда, когда хотя бы один его потомок (соответственно, все его потомки) являются выигрышными ранга 1.

Таким образом, для того, чтобы убедиться, что игрок Duplicator выиг­ function Solve return ((0 ) 0) рывает в игре, достаточно найти такое, что +1 (0 ) (0 ), и про­ верить, что (0 )(0 ) = 0. Этот алгоритм приведён на рисунке 2.3. Легко видеть, что последовательность Клини сходится спустя не более чем | | + шагов, и на каждом шаге для построения очередной функции разметки тре­ буется | ||| операций. Таким образом, сложность алгоритма Solve равна (| |2 ||).

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

Правила игр для нахождения некоторых отношений В некоторых случаях правила игры для нахождения симуляции непо­ средственно вытекают из определения симуляции. Для более сложных отно­ шений необходимо вручную создавать правила игры и доказывать их кор­ ректность. В качестве примера здесь приводятся правила игры для проверки строгой бисимуляции, описанные в работах [44, 76, 98], и правила игры для нахождения прореженной симуляции, описанные в работе [17].

Строгая бисимуляция Рассмотрим две размеченные системы переходов 1 и 2, где = для нахождения строгой бисимуляции между 1 и 2 :

Теорема 2.2. [76, 98] Для любых двух размеченных систем переходов и 2 выполняется: 1 2 тогда и только тогда, когда игрок Duplicator выигрывает в игре,1,2.

Прореженная симуляция Рассмотрим две размеченные системы переходов 1 и 2, где = Рисунок 2.4. Пример игры для проверки прореженной симуляции для нахождения прореженной симуляции между 1 и 2 :

Будем говорить, что в модели есть цикл по одинаково помеченным вершинам, если в есть вычисление = (0, 1,... ), в котором для всех, начиная с некоторого, выполняется ( ) = ( ).

Теорема 2.3. [17] Для любых двух размеченных систем переходов 1 и без циклов по одинаково помеченным вершинам выполняется: тогда и только тогда, когда игрок Duplicator выигрывает в игре,1,2.

В работе [17] также приводится способ проверки прореженной симуляции между моделями с циклами одинаково помеченных вершин, который заклю­ чается в предварительном избавления от таких циклов.

На рисунке 2.4 показаны две модели 1 и 2, для которых выполняется 1 2, и, следовательно, выполняется 1 2 и 2 1 ; и приведён граф игры,1,2.

2.3.2. Теоретико-игровой язык описания симуляций Нами было замечено, что для всех известных отношений симуляции задача проверки выполнимости отношения 1 2 между двумя LTS сво­ дится к задаче поиска выигрышной стратегии в антагонистической игре двух игроков,1,2. В этой игре множество позиций игроков определяется мно­ жествами состояний LTS 1 и 2, но форма правил самой игры зависит только от отношения симуляции. Таким образом, отношение симуляции можно рассматривать как семейство игр, имеющих некоторую общую форму правил игры.

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

Каждая из игр,1,2 =,,,, 0, соответствующая извест­ ным отношениям симуляции, определяется следующими компонентами:

допустимых позиций игроков и. Таким образом, тип позиций игроков определяется парой троек 1, 2, 3 и 1, 2, 3.

2. Отношениями игровых переходов (правилами игры) и ; каждое из указанных отношений представляет собой некоторое подмножество декартового произведения 1 1 +1 2 2 +2 {0, 1}3 +3. Эти отношения могут быть заданы посредством типизированных формул логики пре­ дикатов и в некоторой фиксированной сигнатуре (одна из таких сигнатур будет приведена ниже).

3. Начальной позицией 0, зависящей только от начальных состояний LTS На основании проведённого анализа устройств игр,1,2 для провер­ ки строгой и прореженной симуляции и бисимуляции можно ввести опре­ деление шаблона игры, порождающего множество игр [1, 2 ] для всевозможных пар LTS 1 и 2.

В формулах, описывающих правила игры, могут использоваться пере­ менные 6 типов:

, — два множества переменных, значениями которых могут яв­ ляться состояния LTS 1,, — два множества переменных, значениями которых могут яв­ ляться состояния LTS 2,, — два множества булевых переменных.

Переменные из множеств, и используются для обозначения ком­ понентов позиции игрока Spoiler, а переменные из множеств, и — для обозначения компонентов позиции игрока Duplicator.

Правила игры описываются формулами логики предикатов сигнатуры = {1, 2 }, {1, 2 }, {0, 1}. Эта сигнатура состоит из двух двухместных предикатных символов 1 и 2, используемых для обозначения отношений переходов LTS, двух одноместных функциональных символов 1 и 2, исполь­ зуемых для обозначения функций разметки состояний LTS, а также из двух булевых констант. В сигнатуре правильно построенными термами считают­ качестве атомарных формул разрешается использовать булевы константы, пе­ ременные из множеств,, а также формулы вида 1 (, ), 2 (, ), 1 = 2, где, — переменные одного из четырех типов, {1, 2}, шести натуральных чисел 1, 2, 3, 1, 2, 3, определяющих тип иг­ 1,2 для формул сигнатуры. В этой интерпретации значениями перемен­ ных из множеств и служат состояния LTS, оценкой предикатных символов служит отношение переходов LTS, а оценкой функциональ­ ных символов служит функция разметки LTS.

в которой:

отношение игровых переходов (соответственно ) состоит из всех таких пар (, ) (соответственно (, )), представляющих игровые позиции и, для которых формула (соответственно ) выполняется в интерпретации 1,2 на наборе (, ) значений свободных переменных, т. е.

Описание строгой бисимуляции в рамках разработанного языка верки строгой бисимуляции. Для этого необходимо переформулировать опре­ деление игры,1,2 из раздела 2.3.1. Положим 1 = 2 = 1 = 2 = 3 = (3 ). Формула (1, 2, 3, 1, 2, 3 ) имеет следующий вид:

Формула (1, 2, 3, 1, 2, 3 ) имеет следующий вид:

Описание прореженной симуляции в рамках разработанного языка верки прореженной симуляции Для этого необходимо переформулировать определение игры,1,2 из раздела 2.3.1. Положим 1 = 2 = 2 = 1, 2 = (3 ). Формула (1, 2, 3, 1, 2, 3 ) имеет следующий вид:

Формула (1, 2, 3, 1, 2, 3 ) имеет следующий вид:

Прочие отношения, которые можно описать в рамках разработанного языка Кроме описанных выше шаблонов игр проверки строгой бисимуляции и прореженной симуляции, в рамках разработанного языка мы описали следу­ ющие отношения:

строгую симуляцию и прореженную бисимуляцию, в соответствии с пра­ вилами, описанными в работах [44] и [17], симуляцию для = 2 [43], устройство игры непосредственно вытека­ ло из определения симуляции, слабую симуляцию [105], при определении которой в множество допусти­ мых предикатов пришлось добавить предикаты 1 (1, 2 ) и 2 (1, 2 ), предикат (1, 2 ) истинен, если существует невидимое вычисление из 2.4. Универсальный символьный алгоритм проверки симуляций Символьные алгоритмы верификации работают со сложными структу­ рами данных (формулами, уравнениями, логическим схемами и др.), позво­ ляющими компактно описывать конечные множества. В данной главе для удобства записи будет использоваться формульное представление множеств.

Приведём символьный алгоритм, который по шаблону игры и по двум LTS 1 и 2 проверяет, является ли игра = [1, 2 ] выиг­ рышной для игрока Spoiler. Для того, чтобы сократить пространство поиска выигрышной стратегии, наш алгоритм строит редукцию игры, т. е. удаляет из неё все недостижимые игровые состояния и переходы. Алгоритм является модификацией алгоритма Эделькампа (Edelkamp), описанного в работе [39], и состоит из следующих трёх процедур:

1. Построение отношения игрового перехода.

2. Построение множества достижимых игровых состояний и удаление недостижимых переходов.

3. Решение игры:

а. разбиение достижимых игровых состояний на выигрышные и про­ игрышные состояния игрока Spoiler, б. проверка принадлежности начального игрового состояния множе­ ству выигрышных состояний игрока Spoiler.

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

При описании алгоритма мы не будем детализировать, каким образом реализованы операции над формулами. Нам лишь достаточно, чтобы библио­ тека работы с формулами поддерживала все логические операции (¬,, ), квантификацию (, ) и проверку на эквивалентность (). После описания алгоритма мы остановимся на особенностях его реализации при помощи упо­ рядоченных двоичных разрешающих диаграмм (OBDD).

2.4.1. Построение отношения игрового перехода 1 = 2 =. Будем считать, что множества состояний 1 и 2 конечны. То­ гда и множества переходов 1 и 2 конечны и, следовательно, они представи­ мы формулами 1 и 2 логики предикатов с равенством над сигнатурами,, 1 и,, 2 соответственно. Подставив эти формулы вместо преди­ катов 1 и 2 в формулах и, мы получаем формулы логики предикатов с равенством и над сигнатурой, {1, 2 }, {0, 1} 1 2.

Как было сказано выше в разделе 2.3.2, в формулах и функцио­ нальные символы не могут быть вложены в другие фунциональные символы и предикаты. Поэтому функции в этих формулах могут встречаться толь­ ко в подформулах вида () = () (где, {1, 2}). Очевидно, что такие подформулы можно заменить на формулы логики предикатов с равенством над сигнатурой,, 1 2. После этой замены из формул и мы получаем формулы и над сигнатурой,, 1 2.

Формулы и зависят от переменных и и характеризуют множества допустимых ходов в игре [1, 2 ].

Зададим также формулу 0, характеризующую начальное состояние иг­ ры:

2.4.2. Построение множества достижимых игровых состояний и удаление недостижимых переходов Формулы (, ) и (, ) описывают отношения переходов нередуцированной игры, в которой могут присутствовать недостижимые пе­ реходы. Наша задача — построить символьное представление редуцирован­ ной игры. Алгоритм, изображённый на рисунке 2.5, последовательно строит множества достижимых состояний, а затем оставляет только достижимые игровые переходы.

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

Корректность алгоритма BuildReachable доказывает следующая теоре­ procedure BuildRechable Рисунок 2.5. Алгоритм построения редуцированной игры ма.

Теорема 2.4. После завершения работы процедуры BuildReachable формулы ( ) и ( ) характеризуют множества достижимых состояний игроков и соответственно.

Доказательство. Докажем справедливость утверждения только для состоя­ ний игрока, для состояний игрока оно доказывается аналогично. Пусть ( ) — значение формулы ( ) на -ой итерации цикла. Легко видеть, что формула ( ) характеризует все те состояния, которые достижимы из начального состояния максимум за 2 шагов. Поскольку формула ( ) эквивалентна ( ) (где — номер последней итерации цикла), то ( ) характеризует множество игровых состояний, достижимых из на­ чального за любое конечное число шагов, что и требовалось доказать.

function SymbSolve Рисунок 2.6. Алгоритм нахождения выигрышных состояний игрока Spoiler 2.4.3. Решение игры После завершения процедуры BuildReachable мы имеем символьное пред­ ставлением каждого компонента редуцированной игры. Теперь наша задача — разбить все игровые состояния на выигрышные и проигрышные для игрока Spoiler.

На рисунке 2.6 приведена модификация описанного ранее алгоритма Solve, в которой используются формульные представления множеств. Проце­ дура SymbSolve итеративно строит формулы ( ) и ( ). На каждой итерации формула ( ) ( ) характеризует некоторое подмноже­ ство множества выигрышных для Spoiler состояний, а после выхода из цикла эта формула характеризует множество всех такие состояний. Завершимость и корректность алгоритма SymbSolve следует из доказанных выше заверши­ мости и корректности алгоритма Solve.

В конце процедуры SymbSolve происходит проверка принадлежности начального состояния множеству выигрышных состояний Spoiler. Если ( ) 0 ( ), то выигрывает Duplicator. Это свидетельству­ ет о том, что симуляция выполняется. В противном случае симуляция не выполняется.

2.4.4. Особенности реализации алгоритма при помощи двоичных разрешающих диаграмм При описании алгоритма мы не детализировали, каким образом прово­ дятся операции над формулами. Одним из широко распространённых спосо­ бов представления формул являются упорядоченные двоичные разрешающие диаграммы (OBDD) [16]. OBDD — это каноническая форма представления булевых функций : {0, 1} {0, 1}. Часто представление функций в виде OBDD оказывается значительно более компактным, чем традиционные нор­ мальные формы, такие как дизъюнктивная нормальная форма и коньюнктив­ ная нормальная форма. Упорядоченные двоичные разрешающие диаграммы нашли широкое применение во многих задачах верификации моделей про­ грамм.

Как показал Бриант (Bryant) в 1986 году в своей основополагающей рабо­ те [16], операции над функциями, заданных в виде OBDD, имеют следующую сложность:

OBDD функции, заданной булевой формулой от переменных, в худ­ шем случае имеет размер (занимает память) (2 /);

построение конъюнкции и дизъюнкции функций 1 и 2 отнимает время проверка двух функций на эквивалентность и построение дополнения функции может быть произведено за линейное время.

В формулах, используемых в нашем алгоритме, все переменные прини­ мают значение из конечных множеств 1, 2 или {0, 1}. Элементы каждого конечного множества можно закодировать при помощи булева вектора длины 2 ||. Это позволяет перейти от каждой используемой формулы, не содержащей функциональные символы, к булевой формуле такой, что формула истинна на наборе тогда и только тогда, когда формула истинна на наборе, где — булево представление набора.

Таким образом, все операции над формулами, используемые в приведён­ ном алгоритме проверки симуляций, можно реализовать при помощи опера­ ций над OBDD.

В равной мере для символьного представления моделей и игры могут быть использованы и другие математические конструкции: регулярные выра­ жения, прямое формульное представление и др. OBDD были выбраны ввиду широкой распространённости библиотек для манипуляции с ними.

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

В качестве языка описания моделей мы использовали язык верифика­ тора NuSMV [77] потому, что исходные коды NuSMV предоставляются под лицензией GPL, и его разработчики заявляют что NuSMV может использо­ ваться в качестве платформы для разработки сторонних средств, использу­ емых в верификации моделей. Кроме того, средство NuSMV может исполь­ зоваться для проверки свойств ветвящегося времени, выполнимость которых сохраняют отношения симуляции.

Работа средства проверки симуляций состоит из следующих этапов. Вна­ чале проводится разбор правил игры проверки симуляции, заданных в виде шаблона игры. Далее при помощи изменённой версии NuSMV конструиру­ ются OBDD представлений двух моделей. После этого запускается алгоритм проверки симуляций, и в случае, если симуляция не выполняется, пользова­ телю выдаётся контрпример. Этот контрпример фактически является выиг­ рышным подграфом (стратегией) игрока Spoiler. Для представления контр­ примеров используется формат Graphviz [49].

Разработанное средство написано на языке Python и работает в опера­ ционной среде Linux. В качестве библиотеки работы с OBDD используется библиотека Cudd [32]. Сама библиотека Cudd реализована на языке C++, работа с ней из Python осуществлялась с помощью враппера PyCudd [87].

2.6. Применение средства проверки симуляции для инкрементального построения модели В этом разделе рассматривается пример применения разработанной сре­ ды проверки симуляции.

Зачастую при построении модели допускаются ошибки, которые не могут быть выявлены на этапе автоматической верификации [24]. Существует ме­ тод инкрементального построения моделей программ, который в некоторых случаях поможет избежать таких ошибок [21]. В этом методе последователь­ но строятся модели программ 1,..., так, что каждая следующая модель является уточнением предыдущей модели и содержит больше подробностей о конструируемой программе. Разумно предположить, что между моделями +1 и (где 1 < ) выполняется некоторое отношение симуляции (которое выбирается исходя из характера отличий между +1 и ). Если же это отношение симуляции не выполняется, то контрпример, выданный средством проверки симуляций, поможет найти ошибку в модели +1.

Рассмотрим пример построения модели, описывающей одно из решений задачи обедающих философов [115]. На примере этой задачи часто рассмат­ ривают более общую задачу распределения ресурсов, возникающую при про­ ектировании распределённых программ. Напомним, что в задаче обедающих философов имеется философов, сидящих за круглым столом, перед каж­ дым философом находится тарелка, и кроме того между каждыми двумя философами лежит одна вилка (т. е. всего имеется вилок). Каждый фило­ соф может начать есть только когда он взял вилки слева и справа от себя, а положить вилки он может только после того, как закончил есть. Задача заключается в организации взаимодействия между философами так, чтобы исключить возможность тупика (deadlock), т. е. ситуации, когда каждый фи­ лософ держит вилку в левой руке, и ни один философ не может взять вилку справа от себя и приступить к еде.

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

В модели появляется маркер; каждый философ может получить мар­ кер только когда вилки слева и справа от него лежат на столе. После того, как философ получил маркер, он может взять вилки и начать есть; после того как он поел, он освобождает маркер. В 1971 году Дейсктрой было до­ казано, что в этой модели тупик не достижим [37], кроме того это свойство можно можно проверить автоматически при помощи NuSMV.

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

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

При исследовании моделей оказалось, что между моделями и выпол­ няется не только отношение прореженной симуляции, но и отношение строгой симуляции. Причина этого заключается в том, что из-за особенностей языка NuSMV в модели в каждом состоянии есть переход в это же состояние, и эти переходы соответствуют невидимым переходам в модели.

В таблице 2.7 приведены результаты проверки и для различных количеств обедающих философов. Среда проверки симуля­ ций запускалась на компьютере с процессором AMD Athlon 5200+. Стоит отметить, что большое число состояний в моделях и обусловлено так называемым экспоненциальным ростом числа состояний (в зависимости от количества параллельных процессов, составляющих модель), а описание са­ мих моделей занимает меньше 100 строчек кода на языке NuSMV. Число состояний модели и размер игры для нахождения симуляции между и растёт линейно в зависимости от числа процессов, однако размер модели растёт экспоненциально, и для её построения требуется больше времени, чем для решения игры.

— количество процессов (обедающих философов) в модели, ( ) — количество состояний в модели, ( ) — количество переходов в модели, — количество достижимых состояний в игре для проверки симуляции, — суммарный размер OBDD, описывающих множества достижимых игровых состояний первого и второго игроков, — занятое время при выполнении на процессоре AMD Athlon 5200+.

Рисунок 2.7. Результаты исследований на моделях универсального средства проверки си­ муляций, реализованного в рамках данной работы Стоит отметить, что время работы разработанного средства для данного примера оказалось существенно меньшим теоретических оценок сложности задач проверки симуляций, приведённых в таблице 2.2. Так, теоретико-игро­ вой алгоритм проверки симуляции имеет временную сложность (), где — суммарное количество переходов, а — суммарное количество состояний в моделях. Из таблицы 2.7 видно, что при увеличении количества философов на 1 количество переходов в моделях возрастает в среднем 6.8 раз, а суммар­ ное количество состояний — в 5.9 раз. Поэтому теоретическая верхняя оценка сложности проверки строгой симуляции между и растёт экспоненциаль­ но в зависимости от числа философов, и основание степенной функции при­ мерно равно 40. Однако, время работы алгоритма растёт экспоненциально с основанием степени, примерно равным 6. Такая разница между реальным временем работы алгоритма и его теоретической наихудшей оценкой является следствием того, что в приведённом алгоритме проводится решение редуци­ рованной игры, т. е. игры, содержащей только достижимые состояния (это описано в разделе 2.4.2). В то же время, при выводе теоретических оценок сложности теореко-игрового алгоритма считалось, что все состояния игры являются достижимыми.

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

Показано, что разработанный формальный язык достаточно богат для описания строгой симуляции, строгой бисимуляции, прореженной симуляции, прореженной бисимуляции, 2 симуляции, слабой и блочной симуляций. В то же время этот язык не подходит для описания т. н. справедливых симу­ ляций [44], т. е. симуляций, определённых на множестве структур Крипке с ограничениями справедливости [118]. В справедливых структурах Крипке считаются допустимыми только те вычисления, которые бесконечно часто проходят через так называемые принимающие состояния. Эта особенность справедливых структур Крипке позволяет их использовать, например, для за­ дания модели системы параллельных процессов, в которой каждый процесс рано или поздно будет поставлен на выполнение. К сожалению сложность нахождения справедливых симуляций слишком высока [44], поэтому в наше средство мы не стали добавлять возможность нахождения справедливых от­ ношений симуляции.

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

2.8. Заключение В данной главе был описан формальный язык, позволяющий задавать различные отношения подобия (симуляции) между моделями программ по­ средством правил антогонистической игры двух игроков. В терминах пред­ ложенного языка мы привели полное описание ряда отношений (строгой си­ муляции, строгой бисимуляции, прореженной симуляции, прореженной биси­ муляции). Кроме того, были выявлены общие приёмы, при помощи которых на разработанном нами языке можно описать и другие отношения симуляции (2 симуляция, слабая и блочная симуляции). Это показывает, что предложен­ ный язык описания симуляций имеет хорошие выразительные возможности.

Также разработано программно-инструментальное средство, которое позволяет по описанию симуляции на теоретико-игровом языке и описанию двух моделей на языке NuSMV, проверять выполняется ли данная симуля­ ция между двумя данными моделями. Для эффективности работы данного средства были использованы символьные представления моделей и игры про­ верки симуляции.

Проведено экспериментальное исследование разработанного средства при инкрементальной разработке моделей программ на примере различных вариантов задачи обедающих философов.

Проверка отношений подобия между Во второй главе были рассмотрены отношения подобия (симуляции) меж­ ду моделями программ, заданными структурами Крипке.

Структуры Крипке хорошо подходят для описания моделей программ, работающих в дискретном времени. Однако, часто возникает необходимость в анализе программ, работающих в реальном времени. Такие программы мо­ гут содержать переменные-таймеры, значениями которых могут быть веще­ ственные числа. При написании таких программ приходится учитывать и проверять течение реального времени. Для описания моделей программ с таймерами хорошо подходят временные автоматы, введённые Алюром (Alur) и Диллом (Dill) в 1994 году [5]. По существу, временные автоматы — это ко­ нечные автоматы, снабжённые конечным множеством таймеров и ограниче­ ниями на значения таймеров, при которых допустимы те или иные переходы.

Пока автомат находится в одном состоянии, значения всех таймеров растут с одинаковой скоростью, при переходе из состояния в состояние значения некоторых таймеров могут сбрасываться в 0. В работах [4, 5] было показано, что для временных автоматов являются разрешимыми многие задачи анали­ за, включая задачу проверки достижимости выбранного состояния и задачу проверки выполнимости формул темпоральной логики Timed CTL(TCTL).

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

Временные автоматы также используются в качестве удобной математи­ ческой модели при решении задачи синтеза систем автоматического управ­ ления. Эта задача синтеза состоит в построении такого алгоритма работы устройства управления (контроллера), что объект управления будет коррект­ но функционировать в независимости от действий среды (такие системы на­ зываются системами автоматического управления). При решении этой задачи система автоматического управления может быть представлена автоматом, множество переходов которого состоит из переходов двух типов, контроли­ руемых и неконтролируемых устройством управления. Такой автомат фак­ тически представляет собой описание игры двух участников — контроллера и внешней среды. И действительно, в работе [71] было показано, что задача синтеза работы контроллера сводится к задаче нахождения его выигрышной стратегии в этой игре. В этой же работе было установлено, что задача син­ теза разрешима для случая, когда цель контроллера — перевести систему за определённое время из начального состояния в заданное состояние, избегая при этом попадания в некоторые выделенные (аварийные) состояния (такие свойства можно задавать формулами логики ATCTL).

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

К сожалению, за счёт наличия таймеров временные автоматы как прави­ ло имеют бесконечное число состояний. Это обстоятельство составляет глав­ ную трудность при разработке алгоритмов проверки симуляций на времен­ ных автоматах. В частности, в литературе не было определено отношение симуляци, заданное на важном классе игровых временных автоматов.

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

3.1. Постановка задачи 3.1.1. Условные обозначения Будем обозначать R0 множество всех неотрицательных вещественных чисел, а Z0 — множество всех неотрицательных целых чисел. Пусть и — некоторые множества. Будем использовать запись для обозначения мно­ жества всех отображений из в. Это расходится с привычным в теории множеств обозначением, но такая запись представляется нам в дальней­ шем более удобной.

3.1.2. Временной автомат Пусть — конечное множество вещественных переменных. Будем ис­ пользовать запись () для обозначения множества формул, удовлетворяю­ щих грамматике:

Ниже будет введён ряд определений, необходимых для описания времен­ ного автомата и его семантики (эти определения в том или ином варианте присутствуют в большинстве работ по временным автоматам).

Оценка (valuation) переменных из — это отображение из в R0, т. е. элемент R. В терминологии, используемой в теории схем программ, оценка переменных из является интерпретацией множества переменных в области интерпретации R0 [120].

Будем обозначать оценку, сопоставляющую 0 каждой переменной.

Пусть — некоторое подмножество ; тогда будем использовать за­ пись [ ] для обозначения оценки переменных из, сопоставляющей 0 всем, и () всем. Запись [ ] будет использоваться для обо­ значения того, что таймеры из были сброшены в 0. В качестве примера рассмотрим множество переменных = {2 } и оценку = {1 1, 2 2}, для которых верно [ ] = {1 1, 2 0}.

Будем использовать запись | для обозначения оценки переменных из, для которой верно () = | () для всех. Эта запись будет ис­ пользоваться для выделения значений некоторых таймеров. Например, если Пусть даны два непересекающихся множества вещественных перемен­ ных 1 и 2, и две оценки 1 R1 и 2 R2. Будем использовать запись 1 2 для обозначения такой оценки переменных из 1 2, что (1 2 )() равно 1 (), если 1, и 2 () — иначе. Иными словами, эта запись обозна­ чает то, что две оценки непересекающихся множеств таймеров объединяются в одну. В качестве примера можно рассмотреть оценки 1 = {1 1} и 2 = {2 2}, для которых верно 1 2 = {1 1, 2 2}.

Пусть R0, тогда будем обозначать + такую оценку, что для всех выполняется (+)() = ()+. Эта запись будет использоваться в том случае, когда все переменные оценки увеличиываются на одно и то же число. Например, для оценки = {1 1, 2 2} верно ( + 1) = { 2, 2 3}.

Если () и R, то будем считать, что выполняется |=, если удовлетворяет формуле. Запись |= обозначает то, что формула выполняется на оценке. В качестве примера рассмотрим оценку = { 1, 2 2}, для которой выполняется |= (1 1) и не выполняется |= (2 1).

Будем обозначать [[, ]] множество { R | |= }. Если ясно из контекста, то для простоты будем использовать запись [[]].

Кроме приведённых определений мы будем использовать следующее свойство, являющееся аналогом свойства выпуклости для линейных про­ странств. Для каждой формулы и для любой оценки и любого R0, Определение 3.1 ([5]). Временной автомат (timed automata, TA) — это ше­ стёрка, 0,,,, Inv, где — конечное множество, элементы которого называются дискретными состояниями, 0 — начальное дискретное состояние, — конечное множество вещественных переменных (таймеров), — множество пометок переходов (действий), включающее в себя так называемое невидимое действие, — множество всех подмножеств ), Inv : () — функция, сопоставляющая дискретным состояниям формулы (такие формулы будем называть инвариантами).

Определим размеченную систему переходов (, 0, ), описывающую операционную семантику временного автомата. Множество состояний = R — это множество пар, включающих в себя некоторое дискретное состояние и некоторую оценку переменных из. Начальным состоянием ав­ томата является пара 0 = (0, Определим теперь отношение, определённое на множестве состояний автомата. Будем называть предохранителем перехода (,,,, ) формулу. Если множество содержит переход (,,,, ), то это означает, что временной автомат может совершить переход по действию из дискретного состояния в дискретное состояние при условии, что значения таймеров удовлетворяют предохранителю ; после совершения этого перехода таймеры из множества сбросятся в ноль. Это можно формализовать следующим образом: будем считать, что выполняется (, ) (, ), если существует нам важно, что был задействован именно переход, то будем использовать запись (, ) (, ). Будем считать, что функция () возвращает пометку перехода, т. е. () =, если = (,,,, ).

Автомат может оставаться в дискретном состоянии в течении некоторого времени при условии, что инвариант этого дискретного состояния не будет нарушен. Это можно формализовать следующим образом: для некоторого Вычислением временного автомата будем называть такую конечную или бесконечную последовательность (1, 1, 2, 1, 3, 2, 4, 2, 5,... ), что для Будем также использовать запись 1 2 3... для обозначения вычисления.

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

Длительностью конечного вычисления (1, 1, 2, 1, 3,..., 2+1 ) назовём значение суммы =1, множеством видимых действий этого вычисления назовём {1,..., } { }, и последним действием —.

3.1.3. Временной игровой автомат Временные автоматы могут применяться для решения задачи синтеза контроллера (устройства управления), т. е. построения такого алгоритма его работы, что поведение объекта управления будет корректным независимо от действий среды. Для описания моделей таких систем необходимо выделить среди множества переходов автомата те переходы, которые не контролируют­ ся устройством управления.

Определение 3.2 ([71]). Временной игровой автомат (timed game automata, TGA) — это временной автомат, в котором множество переходов разби­ то на множество контролируемых ( ) и множество неконтролируемых ( ) переходов.

Будем использовать нижние индексы и для обозначения контролиру­ емых и неконтролируемых переходов, т. е. переход контролируем, а переход неконтролируем.

Будем считать что неконтролируемые и контролируемые переходы нико­ гда не помечены одной и той же видимой пометкой, т. е. не существует таких Стратегия Определение 3.3 ([71]). Стратегия контроллера (соответственно, среды) в TGA, 0,,,, Inv — это функция, определённая на множестве конеч­ ных вычислений, и возвращающая некоторый элемент множества (R0 ) (соответственно, (R0 )).

Определение 3.4. Будем называть стратегию стратегией с нулевой памя­ тью, если для любых двух вычислений 1 и 2, у которых одинаковое послед­ нее состояние, справедливо (1 ) = (2 ).

Поскольку значение стратегии с нулевой памятью зависит только от по­ следнего состояния вычисления, то её можно считать определённой на мно­ жестве состояний.

В дальнейшем, если не оговорено иначе, под стратегией будем понимать стратегию с нулевой памятью.

Значение функции () определяет действия игрока в состоянии. Если () = (, ), то это означает, что игрок планирует оставаться в текущем дискретном состоянии на протяжении периода времени, а затем совершить переход.

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

Разумно потребовать, что если согласно стратегии необходимо оставать­ ся в текущем дискретном состоянии единиц времени, а затем совершить переход, то во-первых, при ожидании не нарушится инвариант текущего дискретного состояния, а во-вторых, стратегия “не поменяет своего решения” во время задержки. Таким образом, будем рассматривать только такие стра­ тегии (, ), что для любого состояния, для любого () существует Определение 3.5. Пусть дан TGA, 0,,,, Inv, и пусть (, ) и (, ) — некоторые стратегии контроллера и среды соответственно. Вычис­ ление (1, 1, 2, 1, 3,... ) будем называть порождённым стратегиями (, ) Аналогично определяется вычисление, порождённое стратегиями с нену­ левой памятью.

Отметим, что по определению 3.5, если стратегии контроллера и среды требуют совершить некоторый переход одновременно (т. е. () = ()), то переход совершает среда.

Пусть — некоторая стратегия контроллера в TGA. Обозначим [, ] множество всех вычислений в, начинающихся в состоянии и порождённых и некоторой стратегией среды.

Задача верификации состоит в том, чтобы проверить, верно ли, что су­ ществует некоторая стратегия, для которой все вычисления из [, ] удовлетворяют заданной спецификаций. Для этого необходимо определить формальный язык задания спецификаций, что будет сделано в следующем разделе.

3.1.4. Логика ATCTL Для задания спецификаций будем использоваться логику ATCTL, кото­ рая является одним из универсальных фрагментов логики Timed CTL [4].

Определение 3.6. Логика ATCTL состоит из всех формул вида 1 2 и 1 2, где Z0 {+}, а 1 и 2 — некоторые множества видимых действий.

Для того, чтобы определить выполнимость формул логики ATCTL, опре­ делим сначала выполнимость их подформул вида 1 2 и 1 2.

Будем говорить, что вычисление временного автомата удовлетворя­ ет формуле 1 2, если существует такой префикс этого вычисления, что выполняются следующие условия:

1. все видимые действия лежат в множестве 1, и 2. последнее действие лежит в 2, и 3. длительность не превышает.

Вычисление временного автомата удовлетворяет формуле 1 2, если это вычисление удовлетворяет формуле 1 2, или все видимые дей­ ствия принадлежат множеству 1.

Будем говорить, что формула логики ATCTL выполняется на TGA в состоянии (обозначается, |= ), если существует такая стратегия контроллера, что все вычисления из множества [, ] удовлетворяют формуле. Если формула выполняется в начальном состоянии, то бу­ дем обозначать это записью |=. Стратегию, использование которой контроллером приводит к выполнимости формулы на, будем называть выигрышной в игре (, ).

В работе [71] показано, что классы стратегий с нулевой и с ненулевой памятью имеют одинаковую выразительную мощность в случае, когда специ­ фикации задаются формулами ATCTL. Это означает, что для любого TGA и для любой формулы ATCTL справедливо: в игре (, ) у контроллера существует выигрышная стратегия с нулевой памятью тогда и только тогда, когда в этой игре у него существует стратегия с ненулевой памятью. В общем случае это не так, т. е. можно привести такое свойство (невыразимое форму­ лой ATCTL) и такой TGA, что в игре (, ) у контроллера существует выигрышная стратегия с ненулевой памятью, но не существует выигрышной стратегии с нулевой памятью.

Для проверки выполнимости формул ATCTL на временных игровых ав­ томатов может использоваться средство UPPAAL Tiga[103], в котором реали­ зован алгоритм, описанный в работе [41].

3.1.5. Постановка задачи Будем говорить, что бинарное отношение на множестве TGA сохраня­ ет выполнимость формул логики, если для любой формулы и любых двух TGA 1 и 2 таких, что 1 2, из 2 |= следует 1 |=.

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

Данным свойством, несомненно, обладает отношение изоморфизма, т. е.

отношение, в котором находятся те и только те пары TGA 1 и 2, что изоморфен 2 с учётом переименования переменных-таймеров. Однако нам хотелось бы, чтобы искомое отношение позволяло сравнивать существенно различные по устройству и размеру модели.

Среди отношений, сохраняющих выполнимость формул логики ATCTL, наибольший интерес представляют отношения, для которых существуют эф­ фективные алгоритмы их проверки. Будем искать именно такое отношение.

3.2. Обзор существующих подходов 3.2.1. Языковое включение Поскольку в формулах логики ATCTL не допускается использовать вло­ женные кванторы по вычислениям, то эта логика описывает свойства линей­ ного времени. Для неигровых автоматов самым общим отношением, сохра­ няющим свойства линейного времени, является отношение языкового вклю­ чения. Это отношение определяется следующим образом: два автомата 1 и 2 находятся в отношении языкового включения, если каждое слово, прини­ маемое автоматом 2, принимается и автоматом 1.

Обобщим отношение языкового включения на случай игровых времен­ ных автоматов, как это было сделано в работе [3]. Назовём видимой про­ екцией вычисления 0 1 2 3 4... последовательность (1, 1, 2, 2,... ). Будем говорить, что два игровых автомата 1 и 2 нахо­ дятся в отношении языкового включения, если для любой стратегии контрол­ лера 2 в 2 существует такая стратегия контроллера 1 в 1, что для лю­ бого вычисления 2 2 [2, 0 ] существует такое вычисление 1 1 [1, 0 ], что видимые проекции вычислений 1 и 2 совпадают. Легко видеть, что отношение языкового включения сохраняет выполнимость формул логики ATCTL. К сожалению, задача проверки языкового включения временных неигровых автоматов является алгоритмически неразрешимой [5]. Поскольку временные игровые автоматы являются частным случаем временных неигро­ вых автоматов, то и задача проверки языкового включения игровых времен­ ных автоматов является алгоритмически неразрешимой.

3.2.2. Отношения симуляции Отношения симуляции, являются более строгими, чем отношение язы­ кового включения, посколько сохраняют не только линейные свойства, но и структуру дерева вычислений в недетерменированных вычислительных си­ стемах. Для всех известных нам формализмов задания моделей задача про­ верки симуляции является алгоритмически более простой, чем задача про­ верки языкового включения. Существует большое разнообразие отношений симуляций.

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

Рассмотрим существующие определения временных, альтернирующих и ослабленных симуляций.

Временные симуляции Разрешимость (би)симуляции между временными автоматами была до­ казана в работе [22] при помощи построения декартова произведения вре­ менных зон. Этот алгоритм был реализован в средстве Epsilon[23]. В работе [109] был предложен более эффективный подход для нахождения (слабой) временной бисимуляции, который был основан на операциях над временны­ ми зонами (а не декартовыми произведениями), но он не был реализован на практике.

В работе [58] для проверки временной симуляции между полностью на­ блюдаемыми и детерменированными временными автоматами 1 и 2 пред­ лагается построить автомат, каждое выполнение которого соответствует параллельному выполнению 1 и 2. Тогда задача проверки симуляции сво­ дится к поиску такого достижимого состояния, из которого нельзя про­ должить параллельное выполнение 1 и 2.

Временная симуляция сохраняет выполнимость формул логики TCTL [4]. Поскольку логика ATCTL является фрагментом TCTL, то временная симуляция сохраняет и выполнимость формул логики ATCTL на временных неигровых автоматах.

Альтернирующие симуляции Альтернирующие автоматы Бюхи (их также называют игровыми автома­ тами) используются как вспомогательный инструмент во многих алгоритмах верификации моделей программ [107].

Кроме того, игровые автоматы могут использоваться и как формализм задания моделей мультиагентных систем [68, 88]. В этом случае для описа­ ния спецификаций удобно использовать логику альтернирующего времени ATL [6].

В работе [3] введено понятие игровой (или альтернирующей) симуляции, сохраняющей выполнимость формул универсального фрагмента логики ATL.

Также в работе [3] приводится теоретико-игровой алгоритм проверки такой симуляции.

Если не рассматривать временные ограничения, то логика ATCTL явля­ ется фрагментом логики ATL, поэтому альтернирующая симуляция сохраня­ ет выполнимость формул логики ATCTL на (невременных) игровых автома­ тах.

Ослабленные симуляции Как было указано в разделе 2.1.3, ослабленными отношеними симуляции называются отношения, в которых, в отличие от строгой симуляции, види­ мые и невидимые действия учитываются по-разному. Обзор различных видов ослабленных отношений дан в работе [105]. Все приведённые в данном обзоре симуляции имеют эффективные алгоритмы проверки.

3.2.3. Вывод На основании приведённого выше обзора можно сделать вывод о том, что для определения искомого отношения, сохраняющего выполнимость формул логики ATCTL, можно использовать “комбинацию” определений временной, игровой и ослабленной отношений симуляции. Поскольку задачи проверки этих отношений являются разрешимыми, то можно предположить, что раз­ решимой будет и задача проверки выполнимости искомого отношения. Это предположение будет обосновано ниже в разделе 3.4.

3.3. Определение слабой альтернирующей временной R — множества состояний этих автоматов ( = 1, 2). Наша задача — дать такое определение отношения симуляции, что если справедливо 1 2, то выполнимость формул логики ATCTL на 2 неизбежно влечёт их выполнимость и на 1.

Определим такое отношение 1 2 между парами состояний и 2, что если (1, 2 ), то все формулы ATCTL, выполнимые в состоянии 2, выполнимы и в состоянии 1. Тогда выполнимость отношения будет эквивалентна тому, что начальные состояния TGA 1 и 2 находятся в отношении.

Дадим определения требуемого отношения симуляции при помощи нескольких рекурсивных правил, которым должны удовлетворять пары со­ стояний (1, 2 ), находящихся в отношении.

3.3.1. Видимые дискретные переходы Представим, что в TGA 1 и 2 недопустимы задержки по времени, т. е. недопустимы переходы вида 1 2, где > 0. Такому ограничению будут удовлетворять, в частности, такие автоматы, в которых все инварианты состояний имеют вид ( = 0), где — некоторый таймер из 1 2.

Тогда в 1 и 2 разрешены только дискретные переходы, и поведение этих автоматов полностью описывается поведением схожих по структуре иг­ ровых (невременных) автоматов. Отношение симуляции между игровыми ав­ томатами называется альтернирующей симуляцией и рассматривалось в ра­ боте [3].

В определении альтернирующей симуляции учитывается тот факт, что добавление контролируемых переходов может увеличить множество свойств, выполнимых (контролируемых) на модели, а добавление неконтролируемых переходов — уменьшить это множество. Поэтому контролируемым переходам в 2 должны соответствовать контролируемые переходы в 1, а неконтро­ лируемым переходам в 1 — неконтролируемые переходы в 2.

Пусть (1, 2 ). Потребуем, что каждому контролируемому видимому переходу 2 2 в TGA 2 должен соответствовать такой контролируемый переход 1 1 в TGA 1, что выполняется (1, 2 ). Кроме того, каждому неконтролируемому переходу 1 1 в TGA 1 должен соответ­ ствовать такой неконтролируемый переход 2 2 в 2, что выполняется 3.3.2. Невидимые дискретные переходы Пусть (1, 2 ). Как и в определении слабой симуляции [105], мы не будем требовать, что каждому невидимому переходу в одной из моделей дол­ жен соответствовать невидимый переход в другой модели. Однако потребуем, что если существует невидимый переход 2 2 в TGA 2, то пара (1, 2 ) должна находится в отношении симуляции. Аналогично, если в 1 есть невидимый переход 1 1, то должно выполняться (1, 2 ).

Кроме того, если в моделях присутствуют невидимые переходы, то мож­ но ослабить требования, приведённые в разделе 3.3.1. Так, каждому некон­ тролируемому видимому переходу 1 1 в TGA 1 может соответствовать некоторая последовательность переходов 2 2,1... 2, 2, такая, что (1, 2 ).

Аналогично, каждому контролируемому переходу 2 2 в TGA 2 мо­ жет соответствовать некоторая последовательность переходов 1 1,... 1, 1, такая, что (1, 2 ). Поскольку среда имеет приоритет, если стратегии и среды и контроллер требуют совершить некоторый пере­ ход одновременно, то в промежуточном состоянии 1, среда может помешать контроллеру сделать переход в состояние 1,+1, поэтому дополнительно по­ требуем, что должно выполнятся (1,, 2 ) для каждого = 1...

3.3.3. Временные задержки Представим, что в TGA 2 существует задержка 2 2, и что для любого промежуточного состояния 2 (т. е. 2 2, где 0 < ), из не разрешён ни один дискретный переход. Тогда, если формула 1 2 (или 1 2 ) выполнима в состоянии 2, то в состоянии 2 выполнима формула 1 + 2 (соответственно, 1 + 2 ). Для того, чтобы та же формула выпол­ нялась и в TGA 1 в состоянии 1, достаточно потребовать, чтобы в существовал переход 1 1, и выполнялось (1, 2 ).

3.3.4. Определение искомого отношения Определение 3.7. Пусть даны два TGA 1 и 2 с множествами состояний ется отношением слабой альтернирующей временной (timed weak alternating, twa) симуляции между 1 и 2, если для любой пары (1, 2 ) и для 1. если (2 2 ), то существует такое 1 и такая последовательность 2. если (1 1 ), то существует такое 1 и такая последовательность Отношение twa-симуляции замкнуто по объединению, т. е. если 1 и — отношения twa-симуляции, то 1 2 — тоже отношение twa-симуляции.

Поэтому существует максимальное по включению отношение twa-симуляции, то есть такое отношение, что для любого другого отношения twa-симу­ ляции выполняется.

Будем говорить, что TGA 1 и 2 находятся в отношении twa-симуля­ ции (обозначается 1 2 ), если существует такое отношение twa-симу­ начальные состояния 1 и 2 соответственно.

Будем говорить, что в существует цикл по невидимым переходам, если в существует такое достижимое состояние и такая последовательность состояний 1, 2,..., что = 1 =, и для любого = 1.. 1 выполняется +1. На практике отсутствие циклов по невидимым переходам означает отсутствие так называемых “живых блокировок” (livelocks), т. е. бесконечного поведения, в котором с точки зрения наблюдателя ничего не происходит.

Теорема 3.1. Пусть даны два TGA 1 и 2, в которых нет циклов по невидимым переходам, и такая формула логики ATCTL, что справедливо 1 2 и 2 |=. Тогда справедливо и 1 |=.

Доказательство. Пусть =, 0,,,, Inv, — множество состо­ яний, 0 — его начальное состояние, где = 1, 2. Предположим, что — выигрышная стратегия контроллера в игре (2, ). Покажем, как постро­ ить выигрышную стратегию с ненулевой памятью контроллера 1 в игре (1, ), используя стратегию 2 и отношение.

Для начала рассмотрим случай, когда 1 и 2 не содержат невидимых переходов. Тогда для любой пары (1, 2 ) и для любых и R выполняется:

если 2 2, то существует такое состояние 1 1, что справедливо если 1 1, то существует такое состояние 2 2, что справедливо если 2 2, то существует такое состояние 1 1, что справедливо Напомним, что стратегия контроллера с ненулевой памятью — это функ­ ция, заданная на множестве вычислений. Будем определять стратегию кон­ троллера 1 индукцией по длине вычисления 1 автомата 1. Допустим, уже построен префикс вычисления 1. Зафиксируем значение стратегии контрол­ лера 1 (1 ), а затем выберем произвольное допустимое значение стратегии среды 1 (1 ) и продолжим префикс 1, используя значения 1 (1 ) и 1 (1 ).

Одновременно будем строить некоторое вычисление 2 2 [2, 20 ] так, что если 1 и 2 — последние состояния уже построенных префиксов вычислений 1 и 2, то (1, 2 ). По определению симуляции (10, 20 ), таким образом, это условие будет выполняться и в самом начале, когда вычисления 1 и 2 не содержат ни одного перехода.

— последние состояния этих вычислений, и пусть 2 (2 ) = (, ), где ( ) =. Поскольку существует переход 2 2, то по определению симуляции существует переход 1 1, и (1, 2 ). Поскольку существует переход 2 2, то по определению симуляции существует и так же помеченный положить равным (, ).

Выберем теперь произвольное допустимое значение стратегии среды Если >, то вычисление 1 продолжится задержкой 1 1 и пе­ реходом контроллера 1 1. Вычисление 2 в этом случае продолжим переходами 2 2 и 2 2.

Если, то вычисление 1 продолжится задержкой 1 1 и пере­ ходом среды 1 1. Как было показано выше в разделе 3.1.2, инварианты состояний задаются выпуклыми функциями. Поэтому в 2 допустима за­ держка 2 2, и по определению симуляции выполняется (1, 2 ). Сле­ довательно по определению симуляции существует такие 2 и 2 2, что справедливо (2 ) =, 2 2 и (1, 2 ). Продолжим вычисление 2 переходами 2 2 и 2 2.

В обоих описанных выше случаях выполняется (1, 2 ), где 1 и — последние состояния построенных префиксов вычислений 1 и 2.

Назовём проекцией вычисления = (0, 1, 1, 1, 2, 2,... ) последова­ тельность (1, 1, 2,... ). По стратегии контроллера 2 в TGA 2 и отноше­ нию мы построили такую стратегию с ненулевой памятью 1 контроллера в 1, что для любого вычисления 1 1 [1, 10 ] существует некоторое та­ кое вычисление 2 2 [2, 20 ], что проекции вычислений 1 и 2 совпадают.

Пусть =, где — это либо 1 2, либо 1 2. Поскольку стратегия является выигрышной в игре (2, ), то на вычислении 2 выполняется фор­ мула. Тогда формула выполняется и на 1 (поскольку проекции вычисле­ ний 1 и 2 совпадают). Следовательно, в силу произвольности выбора стра­ тегии среды 1, формула выполняется на любом вычислении из 1 [1, 10 ], и поэтому стратегия (с ненулевой памятью) 1 является выигрышной в игре (1, ). Поскольку для случая, когда цель игры задаётся формулой ATCTL, стратегии с нулевой памятью и с ненулевой памятью имеют одинаковую выра­ зительную мощность [71], то в игре (1, ) имеется и выигрышная стратегия с нулевой памятью. Следовательно, справедливо 1 |=.

Мы рассмотрели упрощённый случай, в котором невидимые переходы отсутствовали в моделях. Перейдём теперь к рассмотрению общего случая моделей 1 и 2.

Опишем теперь, как обобщить приведённое выше доказательство на слу­ чай, когда в 1 и 2 есть невидимые переходы. Допустим, что мы постро­ или вычисления 1 и 2, 1 и 2 — последние состояния этих вычислений и Рассмотрим сначала случай, когда в 2 есть контролируемые невидимые переходы. Предположим, что 2 (2 ) = (1, ), где ( ) =. Пусть 2,1 2,2 и 2 (2,2 ) = (2, ), где ( ) =. Предположим, что =.

Пусть 2,2 2,3 2,4. Из пунктов 3 и 5 определения симуляции видно, что в 1 существует задержка 1 1,2, и существует такой переход 1,2 1,3, что справедливо ( ) = и (1,3, 2,4 ). Выберем в качестве значения стратегии 1 (1 ) = (1 + 2, ).

Если =, то надо применять стратегию контроллера в 2 до тех пор, пока не встретится видимый переход. Рано или поздно такой видимый переход встретится, поскольку по условию теоремы в 2 нет циклов по неви­ димым переходам.

Аналогично рассматривается случай, когда в 1 присутствуют некон­ тролируемые невидимые переходы.

Рассмотрим случай, когда в 1 есть контролируемые невидимые пере­ ходы. Пусть 2 (2 ) = (, ), где ( ) =. Тогда последовательности пере­ ходов 2 2 2 может соответствовать последовательность переходов = 1..) и (1, 2 ). Среда имеет приоритет над контроллером при выбо­ ре следующего состояния вычисления, поэтому данная последовательность переходов может прерваться переходом 1, 1. По определению симуля­ ции указанному переходу будет соответствовать такой переход 2 2, что Аналогично рассматривается случай, когда в 2 присутствуют некон­ тролируемые невидимые переходы.

Назовём видимой проекцией вычисления = (0, 1, 1, 1, 2, 2,... ) по­ следовательность, получаемую из (1, 1, 2,... ) удалением -пометок и за­ меной нескольких подряд идущих длительностей задержек их суммой. Легко видеть, что построенная описанным выше образом стратегия 1 обладает сле­ дующим свойством: для любого вычисления 1 1 [1, 10 ] существует такое вычисление 2 2 [2, 20 ], что видимые проекции 1 и 2 совпадают. Повто­ рив рассуждения из конца первой части доказательства, мы получаем, что 1 |=.