2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 27
Текст из файла (страница 27)
Состояния каждой копни снабжаются индексами; Я' ах!1, ..., я); 2. Яе'= бе х11) — начальным состоянием нового авюмвта являепж на швьное состояние обобщенного автомата с индексом 1. 3. В копни 1 выходные ребра пз сосгояний, принадлежащих допускмошему множеству У„направляются в состояниа слелующей по номеру копни, т. е. Ь'опредепястсв тмс ! Пусть А =!8, Е, Уш б, г), тле Р =(Уп Уз,..., Уь~ — обобщенный автомат Бюхн.
Обычный автоьшт Бюхи А' (о', Е', Яс', Ь', г"'), эквивалентный обобщенному автомату Бюхн А, строится так (рнс. 4.13, а): бпб(р, о),то(ф',Днб'((р',1~,о) иг у=г,если рир„ У = ПУщодд+1, если,опр,. зно Таким образом, в переходах автомата А' получщтся цикл, проходящий через все копии А, и ющщый цикл содержит допускакнцне соопжния нз каящого допускающего множества Я,. 'мат юя" 4. Р"=англ(1) — допускающими состоаниями нового обычного автомкщ Бюхи явлжотся только состояния копни 1 из множества У~ . Под воздействием входной цепочки и автомат А' проходит допуаающие состояния первой копии бесконечно часто тогда и тояько тогда, когда он проходит и состояния из каждого множества Я, бесконечно часто в обобщенном автомате Бюхи А.
Поэтому цепочка ж ящщстся допустимой в А' тогда н только тогда, когда сна допускветсв в А . .ви- ~ый ый яь- му зн, 6 Рис 4.И, От сбобщеняою автомата Баха к обычному жпчмазу Бюхи Пиеа в В акп ° онеч друго ° омпг абебе заннь эшм, тодьк ° се ээ ° Ь, Пример 4.7 По обобщенному автомату Бюхи АЭВ(см. рнс.4.12, б) на рис. 4.13, б по вышеприведенному алгоритму построен эквивалентный обычный автомат Бюхи. Можно видеть, что этот автомат Бюхи допускает все возможные ке- почки с бесконечным числом вхождений как а, так и Ь. рве.4.14.
а) Обсбшеинмй автомат Бюхк — сннхроввая композншм авюматов Бехи рис.4.1 1; б) эквивалентный автомат Бюхн Проверку лусшошм юмка, допускаемого автоматом Бюхи, мшкно осущест.- вить с помощью простого алгоритма: автомат Бюхи А допускает пустой язмк, если и только если в А ле султеслмуеш ни одной сильно связной компонедпы. достюкнмой изначального состояния и вкшочакипей хотя бы одно допускшошее состоюше. Иными словами, есек е аешомаше Бехи ссшь Вккг Еше ! ° спш ж~и вых ~ испо Коне юык~ его в анри тельн сими прох~ мат Б !,б по гтомат ые це. с долускаюизнм состоянием, досяэилпигмй вз начпеьлого соотаялмк вю а- томам допускает хотя бм одно и -слово.
Пример 4.6 В автомате Бюхн на рис. 4.13, б кз начального состотщя (гс, зе, 1) достюким цикл, включающий допускакпцее состояние (ги эз, 1) . Следовательно, этот автомат допускает и -слова (т. е. непустой и -язык). Пр ер4.а Автоматы Бюхи А и В с входным алфавмгом (а, Ь), допускающие цепочки с конечным числом вхождений одной буквы и бесконечнмм числом вхождений другой, представлены на рис. 4.11. Нв рис. 4.!4, а построена нх синхронная композншт — обобщенный автомат Бюхи с двумя множестаамн допускающих состояний Г=(Упрз), где У!=((гпэс)), Уэ=((ге,э!)). По этому обобщенному автомату Бюхи легко строится обычный автомат Бюхи, показанный на рис. 4.14, б.
В этом автомате нет цикла, включающего единственное допускиощее состоанне (гп ге, 1). Следовательно, язык, допускаемый этим автоматом, пуст. Лейсттггельно, пересечение языков Ел и Ьа включест только цепочки с конечным числом вхождений символов о и символов Ь, в все этн цепочки конечные, они никаким авюматом Бюхи не допускаются. Еще раз подчеркнем, что хоти и автомат Бюхи, и обобщенный автомат Бюхн используются для задания и анааиза бесконечных юмков, это конечные модели с конечным числом соопиннй и переходоа.
Они отличаются от обычных конечных автоматов только правилами, определяющими допускаемме цепочки среди множества всех возможных бесконечных входных цепочек. цестгстой комодпо еккл 4.6. Автоматы Би)хи и 1 Т1.-формулы Конечные автоматы можно считать формальными системами, зввающимн языки, т.
е. некоторое подмножество (обычно бесконечное) конечных слов в его входном алфавит. Например, автомат А на рис. 4.7, рзссматрнааеммй как конечный автомат, допускает (н, следовательно, задает) все цепочки из а н Ь, оканчивающиеся на Ь. Все такие цепочки определяются регулярным выражением (а+Ь) Ь. Кюкдмй автомат Бюхи также допускает !н, следовательно, задает) некоторое множество бесконечных цепочек, составленных нз символов его входного алфавита Е, которые определвют его циклическое прохожяение через Ьдно из допускакнцих состояний. Инммн словамн, автомат Бюхн задает и -язык. 142 Глюа 4 Формулы ЬТЬ ннюрпрстнруются иа вычислениях струатурм Кринке.
Каждое вычисление структуры Кринке — это бссконечназ послеловательвкзь состояний. Ясно, однако, что не названия соспжний хармггернзуют вычисление. Вычисление харакюризуется цепочкой подмножеств тех атомарных преднкатов структуры Кринке, которые истинны в соответствующих состояниях, т.е. траекторией. Каждая траектория структуры Крипке— эго бссконечное слово в алфавите 2'г.
Например, если ЛР (Ф г), то г"г=(В,(г),(д),(Ф )). Если а = зсз,ззгз... — вычисление структуры Крипке, то, в соотастс1внн с онрмзглелаам 2.10. Е(о) будем обозначать м -слово Е(ге) Ь(з,) Ь(зз)Ь(зз)..., индуцированное вмчислением о. Например, траектория, соотаеютвующая вычислению, предссзвлспному парис.2.3,— это бесконечная цепочка (р,яЦФ гЦ«)(г)(г) ... Все траектории структуры Кринке рнс. 4.1, а — это бесконечное множество и-слов (т.
с. м -язык), примерами которых являются: (р, б)(щг) (гЦ ),4 (р, бЦ ЦФ гЦгЦ ЦФ г) 4 (р, д) (д, г) (г) (г) ..:, м.слово к удовлетворяет ЬТЬ-формуле <р, сели ф принимает истинное значенне на к (обозначается к/= рй Например, м-слово к=(р)( ЦрЦБЦ ) удовлетворяет формуле р л( еПс) . Любую формулу ф линейной темпо- ральной логики можно считать описанием (спецификацией) е -языка, все цепочки которого удовлетворяют этой формуле. Зацадимся вопросом: можно лн конечным образом с помощью автомюа Бюхн задать все те траектории вычисления„мжорме опнсыванжся заданной Ь 1 формулой е? Во-первых, рассмотрим, какой алфавит должен быль у такого автомата Бюхи. Пусть, например, формула яг усть 1гр, т.
е. эта формула логики ЬТ1. описывает такие бесконечные траектории, в которых когда-нибудь в будущем встреппся р . Автомат Бюхи, допускмощнй все тыще траектории, не может иметь в своем алфавите ппько сними р — ведь автомат Бюхн дслхмн на казсдам,паис функционирования прннюппь какой-то входной символ. Значит, кроме символа р во входном алфыпгю Е автомата Бюхи должно быть еще что-то (например, символ, показывающий отсугствие символа р. Очевидно, что входным аафмщтом Е автомата Бюхи, допускмощвго е-слова, удои (И, На 1 рект вход сисе Антс муля црп \ ( х( йаее 4 оотвю.- ~-слово , траекуктуры к), при- врс И,( юе зна- помята данной г Бюхи. описы- ,рй щущем может жен иа ьь Зна.
ю быть >. Оче- Каждое яьность ют выпомар. ующит ипке— г), то алиня н екжм Ояя ать 143 удовлегворякнпне формуле р ИЪ с мнакеством атомарных предикатов АР, 1 явл меся 2"г. Для формулы гр такой автомат будет иметь входной алфавит 10,1р)), или, что тоже, 11),1р)) . На рис. 4.10 контролвный автомат Бюхи — иаЫкйщ, отслеживающий кор- ректность системы управления перекрестюм, в качестве одного из симжщов входного языка имеет множество 1Ф йо, 6' йо~ двух атомарных преднка- тов, которые ие домены быть истнннм одновременно ни в каком состоянии системы управления перекрестком.
Автоматы Бюхи, допускающие а-язмки, заданнмс некоторыми 1.Т1 фор- мулами, приведены на рис. 4.15. Супзествуст важный результат; впервые полученный а.1 Я5Я г. 1161 н влослед- стван нспсльюванный дяя аернфнкацнн в 1146]. ТЕОРЕМА 4В Для любой ЬТ1 формуяы р существует автомат Бюхн, допускзющнй все м -слова, на которых выполняется р, н только нх. Известно, что для некоторых автоматов Бюхн не существует 1. Ч формулы, которая ъпмат все м -алова, распознаваемые этнм автоматом. Иными слова- мн, автоматы Бюхн более выразлтельны, чем ПЧ формулы.
ТЕОРЕМА 4А Существуют автоматы Бюхя, м-языкн которых не могут бмть заданы ника- кой 1Л7 -формулой. нм аз В качестве примера прнведем вычнслення, удовлепзоряющне требованию: "р нсмнлно яа казндцн чалмам маге". Онн опнсываются м -регулярным вы- раямннем Щ р~+ 811 р~) н определиотся автоматом Бюхн (рнс. 4.16).
Ока- эываетгл, что 1 Т формулой зто свойство выразнть нельзя. Нв рн ° ге зт и Рна 4.16. Автомат Бюхн, лопусзакяанй траевторнн, в зоюрых на змквсм четном маге выпояммтся р 4.7. Структуры Крипке и автоматы Бюхи Структура Крнпке также щаает траектории — мщзкестао бесконечных цепочек над алфынпом 2"~, т. е. символами цепочек являются множества атомарных преднкатов. По заданной структуре Крнпке Аз автомат Бюхн Вн, допускающнй все траекторнн М, стронтся последующему алгоритму: О каждый переход в Вм, ведущнй нз состояния э, помечается подмножеством атомарных преднкатов, истинных в з, н ьз кюклое состоянне Вм явлщтса допускакяцнм — все траекторнн в этом автомате Бкжн явлаютсв допускаемымн м.слоаамн.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
