2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 81
Текст из файла (страница 81)
12.6. Временные регионы: один таймер Когда можно объединять в один класс эквнвамнтностн два состояния системы переходов Т(А) временного автомата А, чтобы сохранюиюь свойства системы переходов, важные для анализа ее свойсш? Пусть у временндго автомю» А только одни локальные часы. Рассмотрим два состояние; (рзя) и (у;з) системы переходов Т(А). Если р и ?в две разные локации, то объеднюпь эти состояния в один васс эквивалентности, конечно. нельзя: состояния с разными локацнямн могут иметь различные значения кгомарных предиквтов в ннх, и свойспю автомата А невозможно будет исследовать после такого обьединения.
Рассмотрим теперь два состояния автомата А с одними и теми же именами локацнй, но отличающиеся значениями локальных часов, например, 3! =(ф х !.5) и зз =(Гн х = !.б) . Можно ли утвсржаать, что 3! и зз эквивалентны относительно каких-либо свойств автомата А? Очевидно, что да, потому что в этих сооюяннях локация одна и та же, н межлу состояниями з! и зз прошло всего О.! единншя непрерывного времени. Такое изменение значения часов не повлияет ни на истинность условий перехода, ни на истинность инварнантов, определяющих нахождение автомвта в поющим.
Действзпельно, все констмггы в неравенопжх, используемых в икр н и б р О ю,в ю «рн- ния ь либо экви! лля 3 наны Пуст сов з на ОЛ изме~ та. П го— Очев ции г с точ мели Пуоп не в юрс~удст акой мтве уци- ассы нове Очевидно, что если показания (единственных) часов в одной и той же локации имеют ненулевую дробную честь н не отличакпся целыми частями. то с точки зрения поведения ЛЮБОГО временного автомата с ЛЮБЫМИ временнымн ограничениями они эквивалентны. Пусть С, — максимальная целая константа в неравенствах для локальных часов х (эту конспнпу будем называть "помазкам" часов х). Обозначим — целую часть вещественного числа 1', гг(г') — дробную часть и. О Определение т2.4 рееионелыюе отношеею эяепеишитности .
ТНО- ~ные жно Определим отношение эквивалентносш ц на мишкеспю вещественнык значений единственных лоюшьиых часов х временного ввтомш» сле- дующим образом: т(х) и «'(х),если; мми мер, квн- ° т(х)>С„Н т'(х)>С все показания лоявлынак часов х, превышшощне свой потолок, эквивалентны, ени. ° т(х)5С„~~Т(ЛЦм(т(х)) л уг(т(х))=бл й(т'(х))=0 спета в ин- целью покаяния локальных часов х, не превышающие потолок, со. стввляют отдельные классы эквиаалеитности, тым условием являются целыми чнсламн.
Поэтому все возможнью ограничения на значения часов Лпя обоих сосюяний з~ = (9; х = 1 5) и гт = (9; х = 1 6) либо истинны, либо лшкны одновременно. Следовательно, зти дяа состояния эквивалентны относительно всех свойств, которые мозшо сформулироашь для временного автомата, у которого во временных ограничениях использо. яаны только целые значения. Пусть теперь з,=(9;т=!.9995) н зз (9;х 2.0005). Хотя показания мм сОВ х В состОЯнии 3, Отлнчастса От псяззаннл чжОВ х В ссстсянин гз тОлькО на 0.001, ист гарантии, чю между этими состояниями не произошло никаких изменений в значениях условий переходов для выполнения действий автомата. Например, условие х < 2 для первого состоянна выполняется, для второ- , главе зд Оасш ° т(х)кС пэ[т(х)]=[к'(х)) л л(э(х))вО л й(г(х))иО любые показания часов х, не превышмощне потолок С„с одинаковымн целыми частями и произвольными ненулевыми дробными частями, эквивалентны.
Классы эквивалентности определенного таким обрезом отношения и называются еремслиымн регналамн (! !пмд гейюпэ), а само отношение и — регэа. иаяьясй эхяьиаяелтластью. + Оп не!ВО ан Временной регион временного автомата — это класс'эквивалентности и интерпретаций локальных чааав автомата. Очевидно, таких клаасое (регионов) всегда конечное число, поскольку потолок часов ограничен. В случае единственных локальных часов регионы описывматся как интервалы вещестмнной оси: [(х=О),(0<х<1),(х 1),(1схс2),(х 2),...,(х С„),(х>С,)]. Их количество равно 2е(С + 1) .
Пример временных регионов длв С, =2 предшаелен на рис. 12.10, а. Заметим, что отношение региональной эквивалентности определено безотносительна какому-нибудь временному автомату нли конкретному набору ограничений на эти часы. Оно зависит только ат потолка часов и определено так, чтобы любые соотношения мшкду значениами часов, имеющие в качест.- ве констант только целые, прииимаяи бы одна и то же значение истинности длл всех интерпретаций часов х из одного и того ям региона. Обозначим [г(х)1 класс эквнеалеиппкти и (регион), которому принадлемит ингерпрепщия э(х) часов х. Ясли отношение эквивалентности и очевидно, клмю эквивалентности [т(х)] будем записывать [т(х)].
Например, пусть т(х) = 03; тогда [г(х)] (О < х <!), О!ругие примеры (при Сх = 2): [х 0]=(х=О) [х =1.56] =[я =1.3] =(1 < х < 2) [х=1.4]=[х=1.3244]=[х=1.89]=(1 «я<2) [х = 2.3] в [к = 2 993] и [я = 3] [х 20355.976] (х >2) сн г а е г- н г с э, э $ $ $ с Ъ $$ $ г" к э щмменнь$ ° $$енгонс$ О Рнс. 12.16. а) йремыгные регноны, прсвспммаогнне квассы эквнввнентностн и; 6) мессы эквнаымнтных состовннн грае$в нерсхпвов автомате А1; с) рспюнакьнын автомат кав временного автомата л1 г 12 12Л'. Граф регионов временного автомата Расширим отиошеиие эквивалентности и, определенное иа бесксиечиом миожестве интерпретаций локальиых часов, па мишкестео состояиий системы переходов т(А) таю два ссстояиия т(А) попаюпог в один класс экеивалеитпости и тогда и только тогда, когда их локации совпадают, а иитерпретации часов находятся в одном и том же региоие (принадяакат одному и тому же классу эквивазеитпссти и !.
Таким обрюом, граф регионов времеююго автомата А — это граф, полученный из системм переходов Т(А) так; одно состояиие графа регионов образуют все состояииа Т(А), припадлелшшие одному и тому же классу эквивалшппости и, т. е. все состояния Т(А) с одной и той же локацпей, иитерпретации часов которых иаходатся в одном временном регионе. Формально: (1ос;т)п(1ос',т') сэ (1ас=1ос')л([т) =[т'] ) Будем обозиачать И (ияи просто И, если отношение зквпвалепппжти и очевидно) класс эквивалеипюсти и, которому прииадлюкит состояиие з графа переходов Т(А) . Пример 12.6 На рис.
12.10, б в графе переходов аатоиата Аз тем. рис. 12.5) вьщелеиы классы эквивалептиьш состояний. В этом автомате только одни часы с потолком 2. Классы зквивалеитиости и здесь образуются: 12 стдельиыми состояниями, в которых зпачеииа локальных часов в точности равны целым О, 1 и 2; О теми состояниями, у которых зиачеиия часов т заключены мюкду 0 и 1, ммклу ! и 2 пбольше 2.
Классы эквивалеитиости и иа миакестве состояиий Т(А) мшкио считать состояииями !Рафа регионов Й(А) (его таске иазыввют автоматом региоиов). Оп является фмггор-графом переходов графа Т(А) по модулю отношения региональной эквиаалептиости ц. Поскольку число регионов всегда колечко, то и состояний у любого графа региоиов тоже конечное число. Дадим форм альков определение гри)ж репюиов. Пусть А=(асс.1 .ь,Х,Зл,й) — р й, Т(А) (аре,|,г)— аисте автои мз ~з система переходов и т — новый символ, не входжпнй в алфавит действий автомата А. вчном 'иста ~внва- рпреи то- ~учен- обра:вива,рпреаены аи1, итать ЕГНО- юше1а ко- )усть — его 12Я 1 ашаногюе Граф регионов временного автомата А — это граф переходов 1ч(А) =(Д», [ЕС]ь, Ем Мв), Гдс; ° Д вЂ” множество состояний — это множество классов отношения эквивалентности и на состояниях графа переходов Т(А), Д, =([Е], ~ЕЕД]; ° [Ее) — начапьиое соспмние графа Рамонов, [Ев] =()сев' [те])» где ге(к) 0 дла часов Я е к; ° Е, = Е и [т] — новый алфавит действий, включаюшнй, кроме действий автомата А, новое действие т.
Символ т будет помечюь перекоп с течением времени, коглв локвпня не меняется 1временную эааержку); ° йе — множествопереходов, й ~Д хЕ,хая тасос, по: для любого действия о автомата А, и любых двух состояний Г, Г'Е Д„Я вЂ” О -+ Г'Е Дв ТОГДа И ТОЛЬКО ТОГДа, КОГДа СУШЕСТЕУКП два такие состояния о и О' системы перекодоа т(А), что ге[О], г а[я] и Е О ьл еК' Дав ВСЕХ Г,Г'ЕДа Г-Т-ЬГ'ЕйатОГДаитОЛЬКОтОГДа, КОГДа 3' состояния г и г' совпадают, и они представляют неограниченный регион, или Р состояния г н г' не совпадают, я ив', г (1ос; [г]).
г'=(1ос; и), и существуег такое И еГс~, что (1ос; г)-А -+ (1ос; т ) — переход в графе Т(А), и для всек А~ ей таких, что И~ ЕИ, [гь~Це[[+.~[э+А~]] (т.е. [г'] — это соседний с И регион, достюкимый из [г] прн удовлетворении ограничений на локальные часы автомата А ). Главе тг Для каждого репюна г следующий регион зпсс(г), вуда попадает граф регионов любого автомата по перехолу т гпо задержке времени), всегда определен однозначно.
Граф регионов Й(Аз) временного автомпщ Аз представлен нерпе. 12ЛО,е. В двух состояниях, (т; (х 2)) и (и; (х>2)), автомата Й(Аз) не выполняется инвариант (х < 2) локации м, поэтому в них время не может прогрессировать. Это пример состояний с остановкой времени (бюейюк зщцв). У автомата Й(Аз) этн состояния недостижимы. Ипж, состояния графа регионов временного автомата А представлают млолсестео состояний системы переходов Т(А) .
А именно, кмкдое состояние (1ос; [т)) графа регионов неявно задает (в общем случае бесконечное) множество таких состояний временного графа, интерпретации т таймеров которых эквивалентны опикительно введенной региональной эквивалентности и. По аналогии с символьным предспщленнем данных с помощью ВРР, состояния графа регионов называют "симеозьлымй состояниями. Легко видеть, что граф регионов Й(А) моделирует поведение графа переходов Т(А), поскольку любые два элемента одного н того же временного региона эквивалентны относительно любого свойства, вмраженного с помопщю условий, наложенных на локации, и ограничений на локальные часы (<1оск солгпаглм). Например, цепочка переходов в Т(Аз) на рнс.
12.10, б: (вхх=О)-01 — «(т;х 0.1)-05-«(игл=0.6)-ОА — «(т;х 1)-а-« (к -О) моделнруегся цепочкой переходов в Й(Аз) грие. 12.10, ей (т;(» 0)) — т-+(щ;(О <х<!)) -т-+(ж;(х =1)) — а-+(м;(я =0)) Каждое состояние графа регионов Й(А) является парой (локаьая пмпамама А; регволй Принадлежносп состояний любого временного автомата р и д одному и тому же региону означщт, что если из р доспокимо какое.то состояние р', то пз О достюкимо состояние о', которое находится в одном регионе с р'. Некоторые состояния графа регионов могут быть недостижимы: например, в графе регионов Й(Аз) состояния (лп(к 2)) н (лп(х>2)) недостюкимы. Далее мы будем показывать на рисунках только достижимые состояния графа регионов. Переходы по действиям будем показывать пунктирными стрелками.
е~г он- нот;о ), и. не нх )о нв н т т г и ерювеннъю реиюеы 6 т 'ь и~ ть Рне. 11.П. а) Временной ввтомвт и), 6) временные репюны и а) врв$ репюнов Й(М~ ) Главе 12 Из разных состояиий одного и того же класса эквиеалеитиости в другой класс эквивалентности переходы могут выполияться при различных зиачеииях временных задержек. Точные зиачеиия иитерваяов времеии меяглу любыми событиями во временном автомате А макно подсчитать только по вычислеииям системы переходов Т(А), которая имеет бесконечное число сосюяиий, и поэтому их невозможно аиализировать.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
