2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 87
Текст из файла (страница 87)
Одной нз форм эквивалентности поведений систем переходов является 6иси- муляция. Бнснмуляция основана на идее моделирования одной системы пе- реходов другой системой переколов. Более формально это определение зву- 4и (об Таз бис "ви нщ чит так. Как обычно, значком -ь' будем сбознвчшь транзитнвное рефлек. сивное замыкание бинарного отношения -+, т. е. р-+ «у обозначает р = ге -+ г, -ь ...-+ г„= а прн любом конечном и-"О,Е2,....
Пусть М и М' — две временных системы перекодов с одним н тем же алфавитом действий Е. Обозначим а ю бинарное отношение на мноместае состояний системы переходов так: р = а =ь а, если существует такое состояние г, что; р-т-+ьз и з-а-ьа, где а и Е, а т — внугренний переход системы по времени. о ив тйЛР гбпси лапал) Бисимуляцня — это отношение эквивалентности на мнакестве пер со. стояний ЯхГ систем М и М' и алфшите действий Е, определяющееся как симметричное бинарное отношение, удовлетворяющее еле. дующим условиам для всех пар (г,г') бнсимуляционно эквиваленпщх состояний: ° если а М существует переход г аюа длл иекоюрых а вЕ и а, то в М' существует переход г'=аюа' н состояния а, 'а' бисимуляционно эквивалентны; и ° если в М' сулысщует переход г'-а-ад' для некоторых пи Ен1?,+ н а', то в М существует переход з -а-+ р и состояния а, р' бисимуляционно эквивалентны. Дае временных системы переходов М и М' биснмуляциоино эквивалшпны (обозначщтся М «М'), сели начальные состояния этих систем бисимуляциоино эквивалентны.
Таким образом, две системы переходов находятся в отношении "невременной бнсимуляции" тогда и тонька тогда, когда они выполняют одни и те яш "видимые" извне переходы, и прн этом переходат в эквнвалензные состоя- ТЕОРЕМА 12.2 Система псршг~дое Т(а) и автомат регионов й(А) любого временного автомата д бнсимуляционно эквивалентны при бненмулацнн и. гласа 12 Иными словами, каждое состояние э системы переходов Т(А) бнснмуляцнонно эквивалентно состоянию [з] графа регионов Гт(А), т.е.
если две интерпретации часов, «и «', находятса в одном временном регионе, И=И, и в графе переходов Т(А) сушествует любая цепочка переходов: (!Ос «е) 4 ~'(!Осб«1) Г(2 +(!ОГ2 «2) Аз +-' л +(! «2я) то в графе регионов Р((А) найдется соотвстствующва папочка переходов: (!Ос; [«])-т-е()сс1; [)])-т-ь ...-а-«(!Ос„; [«„]) и наоборот. Как результат, любая цепочка действий долуакаатся во временном графе переходов тогда и только тогда, когда оиа будет допустима и в графе регионов. Поэтому биснмуляционную эквивалентность двух временных автоматов А и В макло проверить, анализируя бнсимулационную зквюмлентносп их графов регионге, Н(А) и И(В).
ДОСТИжиМОСТЬ Проблема доспскимости для временных автометов являсюя одной из вмкнейших проблем верифнкацим. Неформально, зта проблема звучит твк: достижимо ли некоторое (лпюрректлое) сосюяние (!Ос; «) временного автомата нз его начального (или некоторого промежуточного) состояния (т. е. Оправедлизолн (!Ос;«)-««(!Ос',«'.)7 Для состояний (!Ос; «) н (!Ос', «') временного автомата А = (ь, !Осс, ~ Х, ул«, Е) будем писать: ((ос; «) -+(!ос', «'), если либо ((ос; «) — а -+ (!Ос", «') дла некоторого дейспшя а и Е, либо (!Ос; «) — А -+ (!Ос', «') лля некоторого Л и К~.
с' 12А1 достнжимостль пусть дан временной автомат А =()„!осе, х., х, йпг,е) и некоторое его состояние (!Ос; «). Проблема достюкимостн состоит в проверке того, может ли зго состояние (!ос; 1) быть достигнуто из начального сосюяиия (!Осз; «е), т. е. справедливо ли (!Осе;«з)-е«(!Ос;«), (где «е(х) =О для всех локальных часов л нз Х ). ТЕО% Во вр в Тра~ Такил ТОЛЬК ЭТОГО ТОМЗ1 Прин Из н по ТГЗ = в Аз (' (~ Про( (нли ннче чиш нов. вр раз( ГОПТ анм опм рим Одь Оин том Справедлива слелуюшвя теорема. ТЕОРЕМА 12З Во временном автомате А ((асс; ге)-+е(йа;т) тогда и толью тогда, югдв а графе регионов Й(А) этого автомата (1ссэ1 [гс])-+ (гсс [т]), Таким образом, во временном автомате любое сасгоянне достюкимо тогда и только тогда, когда соотвеютвующее состояние достимнмо в грвфе регношю этого автомата. Следовательно, проблема достимимости для временных ав- томвтоа разрешима.
Пример 12.19 Нз начального сосгояния (з;я О,у=О) временного автомата Аз (см. рис. 12.13) достиэимо саспюшю (г;х=2.у 0.3). Эзо мошно установить по графу регионов Й(Аз), в котором доспакимо состояние Эе (г;[х=2,у=03])=(г;([х 2,0<у<1])). Одна из возможных иепочмс в Аз. (з; х 0 у=О)-1 7-о(Эх=17, у=17)-с-ь(г; я=17 ря 0)-03-+ (г;я=2, у 0.3) Проблему достижимости мошно вмразить с помощью формулы СТ1.
Ир 1илиАСр), где р — логическая комбинация атомарных предикатов и огра.- ничений ив показания локальных часов. Для ее решенна мошно строить значитазьно более ~рубая представление временного автоьгата, чвм граф репю. нов. в. и з" 12.14. Временные зоны ВРЭМЭННЫЭ РЭГИОНЫ И ВДЭМЭННЫЭ ЗОНЫ Разбиение пространства значений локальных часов на регионы, на основа которого строиюя граф регионов, является фундаментальнмм приемом длт анализа свойств временных автоматоа: все докюательства разрешимости и оценки сломности алгоритмов верификации временных автоматов, рэссмюриваемые в литературе, основываются на конструировании такого разбиения. Однако на пракщке графы региожю фактически ие применяются, поскольку онн содеряшт огромное число состояний, зкспоненцнально растущее н с ростом числа локальных часов, и с ростом "потолков" локаяьных часов.
Причина такого огромного чнсяа состовний понятна: идея регионов использует только одно свойство возможных ограничений локальных часов; то, что все констюггм в ограничениях целые. Разбиение на регионы вюбще не учитывает реальных ограничений конкретного временного автомата.
Следствием этого является то, что в графе регионов обычно присугсгвует огромное число состояний, эквивалентных относительно проверяемых свойств. Значительно более эффективное представление поведения временного автомата лмот так называемые "временные зоны", представляющие собой обьедннения таких состояний временного графа, которые эквивалентны относительно не всех возможных свойств поведения (как во временных регионах), а только тех временных смзйстп, которые выражены в ограничениях и инвариантвх временного автомата.
Очевидно, что кюкдый временной регион и их объединения могут быть предспжлены как логические формулы ивд линейными ограничениями локальных часов временного автомата. Недавно была предложена идея анализировать временной автомат, не стров временные регионы, а символически манипулируя всеми ограничениями на показания локальных часов, которые встречаютсв в этом автомате. Одна из рсалинщий этой идеи привела к компактному представлению временного автомата с помощью временных зон. Зона — зто некоторое подмножество регионов. С точки зрения проверки свойств временных автоматов, принципиавьноЯ разницы между графом регионов и графом зон нет, просто граф зон — зто эффективное представление графа регионов, в котором одна зона является объединением многих эквивалентных регионов.
Временнвв зона пнщетсв ограничением на показания часов н является классом эквиввюнтности показаний часов относительно некоторого ограничения й на показания часов: дпГ(Х), (я(=(т~т~=ф. Инымн словами, зона, определяемая ограничением д, это множество значениЯ часов, которые удовлетворяют этому ограничению. Очевидно, что отдельный регион также являсгся зоной, т.
е. зона — это просто объединение нескольких регионов. Можно подойти к построению зон, рассматривал обьединенна эквивалентных регионов, однако зоны могут быть построены и без предварительного построенив графа регионов с использованием операций наа ограничениями локальных часов, встречающиеся во временном автомате. Точно так же, как граф регионов, граф зон представляет граф переходов временного автомата, но зоны .
(клвссы эквивалентности показаний локальных часов автомвта1 на которые рюбнвается все множесщо показаний часов, являнпгл более грубыми, а построенный по этому разбиению граф эон — более компактным. Прз Нв часз рези лои нем пер~ дев Прз)мпр 12.20 На рнс. )2.22 приведен переход временного автомата с двумя локальиымн часами, х и у, из локации м с инварнантом у я? влокацию и. Запппи пе. рекола — неравенство х > 3 . Пусть исходная эона У, (мновмспю значений локальных часов, допустимых при переходе в згу локацию) определяется неравенствами Р б х Я 5, 2 К у К 3 . Если зона 2~ удовлетворяет инварианту локации м, то какое мномество значений локальных часов возможно при переходе в локацюо л ? Иннин словами, если У~ — временнаа зона при входе в локацию и, то какова будет временная зона при входе в локацию и? иоиянер вене: 2 ° () якдб) л Ркуяз) Томме цмимм в ломаем и, м)ммэиин09 энеарнвитсм ливкам: дю (зкк)ь(2яуат)ь(элхуяа) Рне.
Имэ, я-о Посэелоаатекьнсе пресбразоэаиие мы аа однем переходе временного мпемям (м) г()-я -+(л) Ееъ) укаев та Оп (Крмае~ннв (аманы) аеримде: 2, (З *) (аяуят) (-а»укэ) а г) ред П ~ Ссттсс липпыаат часом 2„(а«хяя)л(у 0) а П ~ П~ Рас Рас. 1222, г и ж Последовательное преобразование зон на одном лерехоле аремсанстс аатсмата (яклт)-л-ь(л;24) Пв пп чен Пр Оп ртш обт Ва зуе Эп Рнс. 12.22 показыеаст последоаатсльщю пресбрюоеание зон а этом фрагменте временного аатомата для нахожлення искомой зоны. Во-переых, начальная зона Ут (1<хк5)л(2лУкз) с течением вРемени нзменастса: значение всех локальных часоа одновременно растут с одним темпом. Инеарианг ул 7 локации т отраничиаает рост не толыто часов у, но н часов х, поскольку менку часами обязательно сохраняется соотношение х — у Сонет.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
