2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 25
Текст из файла (страница 25)
трольным автоматом В тоже. Например, любая цепочка, которая допускается синхронной композициай основного устройства и контрольного автомата рнс. 42, является ошибочной для этого основного устройства. Определим в примере 42 любую цепочку, которая состоит из а н Ь, но заквнчнвжтся а, как "ошибочную". Автомат В на рис. 4.5 определяет как раз все такие "ошибочные" цепочки, Поставим вопрос: существует ли среди всех цепочек, допускаемых автоматом А, хотя бы одна "ошибочная" г Дяя отвею на этот вопрос мохгно не анализировать все возможные пути, велущие в допускающие состояния автомата А.
Досщточно построить синхронную композицию автоматов А и В и проверять пусвюту языка Еяпа. Если допускаемый автоматом А 4З В язык Е„ея непуст, то среди бесконечного множества цепочек, которые попускает А, есть и ошибочные цепочкм. Более тою, мы можем указать н путь, коитрпрнмер. показывающий, через какие состояния автомата А проходит "ошибочная" цепочка. Для автомата А примера на рнс. 4 5 одним из контрпрнмеров явящзся путь 1-+2-ь3.
Действительно, путь 1-+ 2-+3 выполняется в А под воздействием входной цепочки Ьа, копзрал является ошибочной — она заканчивается символом а . Таким образом, анализируя конечные модели (конечные автоматы), мы получаем ответ на вопрос о том, включает ли бескоиечлое мншкество слов (язык Ея) какие-нибудь слова нз лругого бешкшечпого мнгскесгва (языка Ея) "ошибочных" слов. Алгоритм проверки моделей для Е Ч формул рвботает полностью аналогично, хотя оперирует несколько более слшкн ими формальнымн моделямн.
4.3. Теоретико-автоматный метод проверки выполнимости ~Т1.-формулы Для реализации этой идеи в области верифииьцин реагирующих систем, моделью которых валяется структура Кринке, требуется уметь конечным абразом задавать язык Ем — все цепочки, возможные в произжшьной структуре Крнлке М, уметь конечным образом задавать юык Š— все цепочки, не удовлетворяющие заданной формуле р логики ЕТ1„а также уметь строить пересечение этих языков н проверять, явлается ли оио пустым. Прн этом мы не только сможем доказать, что Мер, но и найдем контрпрммер — те вычисления М, которые удовлетвораюг формуле Как уже говорилось выше, цепочки, харакшризующие вычисления реагнрующях систем, являются бесконечнымн, они называются е-словами.
Мно- Гласе е плещи и ккгыслесаг амгьгь и коне кается !томата но, мы гояння ера на 'ельно, 1 полу- ~ (язык а 6л) логич- .'И обраг игу)м кн, нс рента >ы мы ге вы- , ноэакак раэ зи всех опыта е в дою ком- лопус- омест- мества е -слов называются е -яэьпщмн. Оказывается, чю некоторые и-языки макно эеэщть конечной моделью, которая назыммтся автоматом Бюхи. Теоретико. автоматный подход к верификации реагирующих систем состоит в том, что строится автомат Бюхи, задающий все траектории анализируемой системы, другой автомат Бюхи, задмощий все неправильные траектории„и анализируется синхроннав композиция этих автоматов.
Более точно, алгоритм проверки выполнимости формулы О ПЧ. на струатурс Крипке М состоит нз следующих шагов (рнс. 4.6): 1. По струкгуре М строится автомат Бюхи Вм . Зтот автомат допускает все возможные траектории (и -слова) структуры Кринка М . Е НЕ вьаюлняегся нв М э выпмгнявгся нв М юглрлщеямэ Ьк. 4ль Пселедощтельнасть нагов мнор пма исг)е1 сйесй(пй дяя 1.Т1 формулы Глава 4 2. По формуле и строится ее отрицание - ~р н затем по формуле -яр сгроиз.- са автомат Бюхи В, допусяающий множество ы-слов, которые удовлетворяют -яр.
Этот автомат будет "контрольным" автоматом, допускающим асе ошнбочнме траектории. 3. Строиюя автомат Вм Э — синхронная композиция автомата Вн и "контрольного" автомата В . Этот автомат допусюют пересечение языков, допускаемых компонентными автоматами, т. е. все цепочки, допускаемые как автоматом Ви, так и автоматом В 4. Проверяется пустота язьжа Вв а . Формула й выполняеюя для М, если н только если этот язык пуст. Если этот язык непуст, то формула й не выполнштся для М, структура Кринке имеет ошибочную траекторюо поведения, которая удовлепоряст у, и можно построить коыириример (ошибочный путь), т.
е. путь в М, нарушающий свойство й. Все введенные понятия формально определаются в следующем разделе. Мы начнем с обоснованна необходимости введения нового типа формальных моделей — автомата Бюхн, рассмотрим свойства таких автоматов, правила построения их синхронной композиции. Далее обсудим связь формул БТБ н автоматов Бюхи как моделей для задания конечным образом свойств бесконечных вычислений, Ъпем рассмотрим алгоритм построения синхронной композиции двух автоматов Бехи и алгоритм определения того, что автомат Бюхи допускает пустой язык. В конце главы рассмотрим правила построения автомата Бюхи, допускающего все такие цепочки, на которых заданная БТ(~формула выполняется. 4.4. Автоматы Бюхи —, МОД®ЛИ ДЛЯ ЗВДЗНИЯ б) ЯЗЫКОВ Классическая теория формальных азыков и конечных автоматов построена лля шшлиза цепочек символов, которые мозуг иметь КОНЕЧНУ)0, хотя и проювольную длину.
Формальные языки являются формальными моделями естественных и искусственных юыков, все слова которых конечны (например, скаль бы длинную фразу а ии начал, я когда-нибудь замолчу, какой бы длинный роман ни был, он когда-нибудь закончится, программист ьюжст написать тольжз конечную программу, асс сообщения имеют только конечную длину н т. п.). Теория формальных языков и конечных автоматов имеет разнообразные применения в трансляции пыжов программирования, анализе текстов и многих других областях. Есе зги приложения имеют дело только с г Сую ° гзн ватт жьту Шь ° лапу о ать тэг с конечнымн непочквмн символов, поогроеннымн нз снмвощж конечного словаря.
Еше рш подчеркнем, что число такнх конечных цепочек мщкет быль бесконечным. Вм н е язы- копус- ~я яг, ула ц торню Иизмр ~е. Мы ых моща ло. ЕТЬ н бескоюнной втомат роения данная ив е.з аешоышн Ешли) Автомат Бюхн — это щперка (о, Х, Яс, Ь, гт), где: ° Š— конечное множество символов (алфавнт); ° Я вЂ” мнояиство состояннй; ° $>СЯ вЂ” множество начальных состояний (содерлщшее только один элемент для детермнннроввнного случая); е Ь: Я х Е -ь Эз — отношение переходов (длв детерминированного автомата б МХЕ-+Я); ° Р С 8 — мпоплство дсмупзжщцнх (фпнщцнык) состояний, .
:троена хотя н дел ямн ,'наприкой бы жет нанечную жт раз- только ш-языки и поведение реагирующих систем Цепочкн, порслщаемью вычислениями реагирующих систем, являются бег конечными, поскольку зтн системы после запуска должны функцноннровать БЕСКОНЕЧНО долго. Формальные моделн, нспользуемые прн вернфнкацнн таких систем, должнм иметь дело с бесконечнымн цепочками — м -словвмн, н нх множествамн — мчщыкамн. Поэтому первой нашей задачей является следующая: как с помощью автомата описать ы -языку Конечные автоматы явлжотся удобным формалнзмом, который конечным образом залает обычные формальные взыкн — бесконечные множества цело. чек конечной данны.
Нвм нужен новый тнп автомата, вещающего оз-взыкн— бесконечнме множесща бесконечных цепочек. Можно лн звдщь хотя бы некоторые м-языкн конечными моделями, аналогичными конечным автоматам".г Существует несколько возможных путей обобщения моделн конечного автомата таким образом, чтобы он мог допусюпь бесконечные цепочки. Мы рассьютрнм два таких формалнзма, которые были созданы в середнне прошлого ° ока: автоматы Бюхн н обобщенные автоматы Бюхн. Автомат Бюхн можно счнтать недегермнннрованным конечным автоматом, пслучающнм на вход бесконечные слова. В отянчне от конечного автомата, усяовне допустимости входной цепочкн в автомкш Бюхн изменено так, чтобы можно было определять некоторые бесконечнью цепочкн (е слова) явк допустн мыс. 132 Любое и-слово и юа алфавгпом Е можно счиппь функцией иМ-чЕ (где дl — натуральные числа), понимая под и(!) гчо букву слова и.
Аналогично, если к: М -+ 8 — бесконечная последовательность состояний автомата А, то к(П вЂ” 1-е состояние в цепочке и. Обозначим гнУ(я) множество элементов из Я, которые встречмотся в цепочке к бесконечно много раз. е -слово и над алфавитом Е допускается автоматом Бюхи А =(8, Е, Вс, б, Р'), если существует такое е -слово к нал множеством состояний В (бесконечная цепочка состояний автоматаА), по: °, х(0) е Яе — цепочка состояний начинается одним из начальных состоаннй; ° тгк 0: х(г+ 1) и б(к(1) м(1)) — переход в очередное состояние вызван очередной буквой ы -слова и; ° !лу(к) г! В и И вЂ” среди бесконечно повторюощихся щютсвний цепочки к существует хотя бы одно допускающее. Таким образом, автомат Бюхи допусюмт (распознает, принимает) а.слово, если при чтении этого бесконечного слова автомат бесконечно много раз проходит хотя бы одно допускаквцее состояние.
Множество и -слов, допускаемых автоматом Бюхи А, называетсв м-языком, допускаемым А. в-язык Е ~ Е" называется Бюхи-допусююмым (нли и-ре!улярнымй если существует автомат Бюхи, допускающий Е. Автоматы Бюхи эквивалентны, если допускаемые нми языки совпадмот. Поскольку автоматы Бюхн используются для жвания в -языков, их тыаке нюы вист и -автомвтами. Прмыпр 4.3 Два автомата, А и В, приведенные на рис. 4.7, можно считать как конечнымн автоматамн, так н автоматами Бюхи. Автомат А, рассматриваимый как автомат Бюхи, допускает любую цепочку из символов а н Ь, содераашую бесконечное число вхоященнй Ь.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
