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