2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 49
Текст из файла (страница 49)
Графические элементы, свазывающие элементарные шаги процессов, следующие. ° — АпгУо(и — процесс нродолжаегся, если все входные действия этого блока выполнены; а — Огуо(н — процесс продолхшется, если хотя бы одно из входных действий этого блока выполнено; е — Авдбрйй — все выходные процессы этого блока заиускшотся;, Для Прн цжз сущ сон энр аум~ Тин лрог РН где ' Ю; г' Неве 8 3. Пою вк- функ- юблсэтому э всс- того 1 проэйэлц.
меют мвльэдели легко оввть кото- пвмн ввноязык :рить сэнщ1 сссы, эиру. с по- эецн1.Т1., э ме. энес:нты, ного дей- Рае.$.1. Графическое предстмтенне бизнес-процессов стрехояой компвнни о — Огбррд — по кремней мере одни нз вмхслных процессов этого блока запускается. Дла струкгурптцни процессов используетоя объединение действий в модули, графически прсдстмщяемые прямоугольниками, включаюищмн в себя элементы модуля. Модули могут быть связаны синхронной коммуникацией. Пример спецификации бизнес-процессов страховой компании с помощью графического взыка АтЬег покюви на рис. 8.1. В этой страховой компании сущестует несколько бизнес-процессов: процесс Свгвбе, описыввкнцнй деВ стеня и их связи по ремонту автомашины после тюрин, процесс Рго-уээ, моделирующий прохомдение бумаг а компании, процесс клиента, подтощего документы нв возмещение ущерба н полу тющего метину после ремонта, и др. Типичные свойстве, которые моэуг быть проверены дла этих бизнеспроцессов: Р!: Мамино рвмонтнрутлсв только восле того, «ок нртопио рвнинае сб удовлетворенно аскц нрнчем это рвнннне молсвт быть н не принято; С((-ейлиобв серо!тд)Трао!т сррюзвд) где ЧР— слабый Упэ11.
Р2: ХХск до 10 тысвч доялорэм дла клиента з'1104 всегда будни удовяентереэк С((с!шт Ьв!ом !Озэсэоготвг 108)нгрс1оют орртотг1) РЗ: Из зараз«о молото всзераикмтсв владвльлу только восле ев ратнвиа: С ((-гзвзэгг сог) Ррйотоде гвроггегз) длвеа а Ра: Если нск отвергнут, машину не будут ремонтироввзь: . С ггс1а!т ге/есть С чйвнаяе гераГгегг)) Р5: Гврюк не представит счет за ремонт, если иск отаергнуп сЦсьггт гегесгеи ю с еяьтй ьшо!се)) В.2. Проблема планирования как гпосЫ спесЫпя Проблема планированиа — зто классическая проблема искусственного интеллекта. Она состоит в поиске такого плана целесообразной деятельности в некоторой среде, шпорый приведет к заданной цели. Более точное опрединнне обычно определяет среду как дискретное мноямство состояний и перехо.
дов ыежлу ними, а проблему планироаанив — как поиск конечной последовательшкти действий, которая переводит из начального состояния е одно нз состояний, которме удовлетворяют поставленной цели. В юямснческой теории планирования приюпы следующие предположеииа: О состояния средм днскрстны, квкдое состояние полностью наблюдаемо н множество состояний конечно; О время решения и выполнения действий не учитывается; О возможные действия по изменению сосюяннй извастнм, кюкдое действие приводит к единственному новому состояяию; О начальное состояние шшностью определено: О пель определена явно как одно соеюяние нли мншкество заключительных состояний; О план — последовательность действий — строится один рнь изменение среды в процесса выполнения плана определяепж только выполняемымн действиями.
Решением проблемы планнроааниа ввлаетса пуп, от начального состояния до палевого состояния. В некоторых случаях искомый путь должен удовлетворяю некоторому набору ограничений. Часто с решением саюывают его качеспю, т, е. некоторую функцию стоимости пути. Тогда поиск решения состоит в нахождении оптимального пути, который имеет наименьшую стоимость среди всех возможных решений. Одяой из главных причин сложности этой проблемы яшгяешя огромный размер пространства возмвкных последовательностей шагов.
Дяя построения ам оригма планировании, который мог бы найти лу ппий пуп, среди огромно- го стр иия Суг чес Во ды явл. мог пел Прес цесс стоя~ дом свой мерется. Если с поь ия: ьных план Рис. 8дд Система лланироваюм ~ение яыми ия до ство. каче:тоит юсть 1 ряз- ения ~ми~ь о иикти в ;дмю'рехо- ледоло из го числа альтернативных путей, требуются методы для представления пространственного зияния: структуры среды, связей и переходов между соетовииями, а такам управления перебором в пространстве вариантов. Существуют различные методы синтеза плаца из формальной модели и логи.
ческой спецификации цели, которые реализуются в алгоритме планировщика. В общем виде процесс планирования представлен иа рис. 82. Описание среды — коиечвио множества состояний и их связей, а также описание цели являютса входом в систему плаиироваиия, которая либо не находит требуемого плашь либо находит его и выдает как путь из начального состояния в целевое состояние, Представлеииый таким образом процесс планирования очень похож па про цесс верификации (рис. 8.3): описание системы — конечное миожесшо состояний и переходов, а глюке описание проверяемого свойства являются входом в систему верификации.
Верификвтор либо заключает, что заданное свойство выполцяеюя, либо, если оно ие вмполияется, выддет коизрпример — такой путь из начального состояния, иа котором свойство ие выполняется. Если среду прелставить как структуру Крипке М, а состояния цели описать с впиицыо логического условия р, то в простейшем случае зажгчу пяаиироваиия можно переформулировать как задачу верификации — проверку вы- Глава в опимзра крима Мвр ванн нанб лект Мнр но н ков ! ти и За о, СТОН друг шаг< Кантрарммер Рнс. $.3. Сискма верификации поянения свойства, выршкениого формулой А6 ер линейной темпоральной логики (.Т(. на структуре М (на всех путях из начального состояния структуры М свойство р никогда не встретнтая).
Верифнкагор будет нокать опровержение, т. е. путь в М, удовлепюряющий отрицанию А6 р этой формулы, т. е. формуле Ер р. Если верификатор найдет опровержение, то зто н будет решением задачи шжннровання. Таким образом, система верификации не только сообщит, что существует пугь, на котором будет выполняться формула Ерр (т.е. саойспю р может выполниться когда-нибудь в будущем). но и выдаст один из жжможных путей квк конгрпример (рнс. ВВ).
Если искомый путь к цели должен удовлетворять огрвничениам, запишем этн шраничения о помощью логической формулы у, которая дол:кна выполняться ао всех состояниях на пути до цели. Вернфикатор в этом случае может быть использован для проверки условия А (цг6<р) (ле существует,такого 'лулги, но ктлорот в будущем моисею быть достигнуто состояние, удсеяетвораюи,ме р, о до этого во всех состояниях луши вылояняется свойство у ). Верификатор будет исказя путь, удовлепюрающий формуле А, (чйеф) =е(чйкр), н асан такой путь будет найден, то выдаст его в квчсствс контрпрнмарв.
Таки спец ныд торо обла без ~ проб цнн легк~ всех зада ды), вием чогь план стоя На ( прог рсш~ дов~ Леп кон( го и буде буде стоя циш ~ще 8 применения аяияияииа люде[ а ~ьнай труа ь опэтой о это )икапьса [уду т эти го а Таким образом, иден шаде[ сйесЫпй и формулы темпоральной логики дая спецификации цели и ограничений при поиске цели могут быть использованы для решении проблем планирования. Ниже мы рассмотрим пример, в котором идеи люде! сЬесЫпй применяются для решения простой проблемм этой области. В этом примере мы используем стандартный подход ля[де! сбсе[с[ой без какой-либо оптимизации и эвристики. Вместо того чтобы предсшшвпь проблему в виде структуры Кринке, будем испальювать сиатему верификанни Бртл и представлять модель проблемы нв языке Ртоше[а, На этом языке легко определяется множество жжмажных состояний среды (как множество всех возможных наборов значений переменных, описывающих среду), можно задать начальное н целевое состояния (как наборы значений параметров среды), а тишке определить правила изменения состояний.
Проверяемым условием является сведующее: "чеяееое сосяимиие среды яедостижимо иэ ее иочаяьиого состояния'. В качестве контрпримера бр[и находит и выдает план — последовательность шагов, приводящих нз начального в целевое состояние, удовлетворяющее ограничениям. Мир блоков (Ыосйя иогЫ). Мир блоков — зто искусственная среда планирования действий, катарах нэ.за своей ясности и простоты явлжтав одним из наиболее часто приводимых примеров планированив в искусспюнном интеллекте. Мир блоков состоит нз плоской поверхности (стола), на которой расцщиакено несколыю именованных блоков (АВС,...).
Взаимное располвкеиие блоков (конфигурация) яшмется состоянием среды. Задача планирования — найти план, каторый позволит перевести начальную конфщурацию в целевую. За один шаг может быть перемещен только один блок, на катаром ничего не стоит: он может быть либо поставлен иа стол, либо сразу поставлен сверху на другой блок. Оптимааьный план — это план, имеющий наименьшее число шагов. На рис. 8.4, о представлен пример такого задания. Рнс. 8.4, б показывает все лроатранство состоаннй и переходы меткду ними для трех блоков. План— решение задачи — аостонт в любой псаледовательностн допустимых переходов из начального в целевое састоание.
Легко построить программу на языке Ртоше1а, описывающую все возможные конфи[урании и допустимые их изменения для любого числа блоков и любого их расположения. Число блоков определим параметром и, кюкдый блок будет идентифицироваться уникальным номером от а до и-ц Конфигурацию будем задавать двумя массивами данны н: яр[ы определяет номер блока, стоящего над т-м, оаям[ы определяет номер блока, спвпцего под [-м. Специаяьная константа иатнпю пусть опредшщет, что над нли под блоком ничего гвв рла в не стонт. Целевая конфщурацив определяется подобнымн масснвамн т ср н то Рнс. 8.4.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
