Главная » Все файлы » Просмотр файлов из архивов » PDF-файлы » 5. Principles of Model Checking. Baier_ Joost (2008)

5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 8

PDF-файл 5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 8 Математические методы верификации схем и программ (63287): Книга - 10 семестр (2 семестр магистратуры)5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf) - PDF, страница 8 (63287) - СтудИзба2020-08-25СтудИзба

Описание файла

PDF-файл из архива "5. Principles of Model Checking. Baier_ Joost (2008).pdf", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 8 страницы из PDF

A state describes some information about a system at acertain moment of its behavior. For instance, a state of a traffic light indicates the currentcolor of the light. Similarly, a state of a sequential computer program indicates the currentvalues of all program variables together with the current value of the program counter thatindicates the next program statement to be executed. In a synchronous hardware circuit,a state typically represents the current value of the registers together with the values ofthe input bits.

Transitions specify how the system can evolve from one state to another.In the case of the traffic light a transition may indicate a switch from one color to another,whereas for the sequential program a transition typically corresponds to the execution of astatement and may involve the change of some variables and the program counter. In thecase of the synchronous hardware circuit, a transition models the change of the registersand output bits on a new set of inputs.1920Modelling Concurrent SystemsIn the literature, many different types of transition systems have been proposed. Weuse transition systems with action names for the transitions (state changes) and atomicpropositions for the states.

Action names will be used for describing communicationmechanisms between processes. We use letters at the beginning of the Greek alphabet(such as α, β, and so on) to denote actions. Atomic propositions are used to formalizetemporal characteristics. Atomic propositions intuitively express simple known facts aboutthe states of the system under consideration. They are denoted by arabic letters from thebeginning of the alphabet, such as a, b, c, and so on. Examples of atomic propositions are“x equals 0”, or “x is smaller than 200” for some given integer variable x.

Other examplesare “there is more than a liter of fluid in the tank” or “there are no customers in theshop”.Definition 2.1.Transition System (TS)A transition system TS is a tuple (S, Act, →, I, AP, L) where• S is a set of states,• Act is a set of actions,• −→ ⊆ S × Act × S is a transition relation,• I ⊆ S is a set of initial states,• AP is a set of atomic propositions, and• L : S → 2AP is a labeling function.TS is called finite if S, Act, and AP are finite.αFor convenience, we write s −−→ s instead of (s, α, s ) ∈ −→. The intuitive behavior of atransition system can be described as follows. The transition system starts in some initialstate s0 ∈ I and evolves according to the transition relation −→.

That is, if s is theα→ s originating from s is selected nondeterministicallycurrent state, then a transition s −−and taken, i.e., the action α is performed and the transition system evolves from states into the state s . This selection procedure is repeated in state s and finishes once astate is encountered that has no outgoing transitions. (Note that I may be empty; in thatcase, the transition system has no behavior at all as no initial state can be selected.) Itis important to realize that in case a state has more than one outgoing transition, the“next” transition is chosen in a purely nondeterministic fashion.

That is, the outcome ofthis selection process is not known a priori, and, hence, no statement can be made aboutTransition Systems21the likelihood with which a certain transition is selected. Similarly, when the set of initialstates consists of more than one state, the start state is selected nondeterministically.The labeling function L relates a set L(s) ∈ 2AP of atomic propositions to any state s.1L(s) intuitively stands for exactly those atomic propositions a ∈ AP which are satisfiedby state s.

Given that Φ is a propositional logic formula, then s satisfies the formula Φ ifthe evaluation induced by L(s) makes the formula Φ true; that is:s |= ΦL(s) |= Φ.iff(Basic principles of propositional logic are explained in Appendix A.3, see page 915 ff.)Example 2.2.Beverage Vending MachineWe consider an (somewhat foolish) example, which has been established as standard in thefield of process calculi. The transition system in Figure 2.1 models a preliminary designof a beverage vending machine. The machine can either deliver beer or soda. States arerepresented by ovals and transitions by labeled edges.

State names are depicted inside theovals. Initial states are indicated by having an incoming arrow without source.payget sodaget beerinsert coinsodaτselectτbeerFigure 2.1: A transition system of a simple beverage vending machine.The state space is S = { pay , select, soda , beer }.

The set of initial states consists ofonly one state, i.e., I = { pay }. The (user) action insert coin denotes the insertion of acoin, while the (machine) actions get soda and get beer denote the delivery of soda andbeer, respectively. Transitions of which the action label is not of further interest here,e.g., as it denotes some internal activity of the beverage machine, are all denoted by thedistinguished action symbol τ . We have:Act = { insert coin, get soda, get beer , τ }.Some example transitions are:insert coin−−−−−−→ selectpay −−1Recall that 2AP denotes the power set of AP.andget beerbeer −−−−−−→ pay .22Modelling Concurrent SystemsIt is worthwhile to note that after the insertion of a coin, the vending machine nondeterministically can choose to provide either beer or soda.The atomic propositions in the transition system depend on the properties under consideration.

A simple choice is to let the state names act as atomic propositions, i.e.,L(s) = { s } for any state s. If, however, the only relevant properties do not refer to theselected beverage, as in the property“The vending machine only delivers a drink after providing a coin”,it suffices to use the two-element set of propositions AP = { paid , drink } with labelingfunction:L(pay) = ∅, L(soda) = L(beer ) = { paid , drink }, L(select) = { paid }.Here, the proposition paid characterizes exactly those states in which the user has alreadypaid but not yet obtained a beverage.The previous example illustrates a certain arbitrariness concerning the choice of atomicpropositions and action names.

Even if the formal definition of a transition system requiresdetermining the set of actions Act and the set of propositions AP, the components Actand AP are casually dealt with in the following. Actions are only necessary for modelingcommunication mechanisms as we will see later on. In cases where action names areirrelevant, e.g., because the transition stands for an internal process activity, we use aspecial symbol τ or, in cases where action names are not relevant, even omit the actionlabel. The set of propositions AP is always chosen depending on the characteristics ofinterest. In depicting transition systems, the set of propositions AP often is not explicitlyindicated and it is assumed that AP ⊆ S with labeling function L(s) = { s } ∩ AP.Crucial for modeling hard- or software systems by transition systems is the nondeterminism, which in this context is by far more than a theoretical concept.

Later in this chapter(Section 2.2), we will explain in detail how transition systems can serve as a formal modelfor parallel systems. We mention here only that nondeterministic choices serve to modelthe parallel execution of independent activities by interleaving and to model the conflictsituations that arise, e.g., if two processes aim to access a shared resource. Essentially,interleaving means the nondeterministic choice of the order in which order the actions ofthe processes that run in parallel are executed.

Besides parallelism, the nondeterminismis also important for abstraction purposes, for underspecification, and to model the interface with an unknown or unpredictable environment (e.g., a human user). An example ofthe last is provided by the beverage vending machine where the user resolves the nondeterministic choice between the two τ -transitions in state ”select” by choosing one of thetwo available drinks. The notion “underspecification” refers to early design phases whereTransition Systems23a coarse model for a system is provided that represents several options for the possiblebehaviors by nondeterminism. The rough idea is that in further refinement steps the designer realizes one of the nondeterministic alternatives, but skips the others.

In this sense,nondeterminism in a transition system can represent implementation freedom.Definition 2.3.Direct Predecessors and SuccessorsLet TS = (S, Act, →, I, AP, L) be a transition system. For s ∈ S and α ∈ Act, the set ofdirect α-successors of s is defined as:α→ s ,Post(s, α).Post(s) =Post(s, α) =s ∈ S | s −−α∈ActThe set of α-predecessors of s is defined by:α→s ,Pre(s, α) =s ∈ S | s −−Pre(s) =Pre(s, α).α∈ActEach state s ∈ Post(s, α) is called a direct α-successor of s.

Accordingly, each states ∈ Post(s) is called a direct successor of s. The notations for the sets of direct successorsare expanded to subsets of S in the obvious way (i.e., pointwise extension): for C ⊆ S, letPost(s, α), Post(C) =Post(s).Post(C, α) =s∈Cs∈CThe notations Pre(C, α) and Pre(C) are defined in an analogous way:Pre(s, α), Pre(C) =Pre(s).Pre(C, α) =s∈Cs∈CTerminal states of a transition system TS are states without any outgoing transitions.Once the system described by TS reaches a terminal state, the complete system comes toa halt.Definition 2.4.Terminal StateState s in transition system TS is called terminal if and only if Post(s) = ∅.For a transition system modeling a sequential computer program, terminal states occuras a natural phenomenon representing the termination of the program.

Later on, we will24Modelling Concurrent Systemssee that for transition systems modeling parallel systems, such terminal states are usuallyconsidered to be undesired (see Section 3.1, page 89 ff.).We mentioned above that nondeterminism is crucial for modeling computer systems. However, it is often useful to consider transition systems where the ”observable” behavior isdeterministic, according to some notion of observables. There are two general approachesto formalize the visible behavior of a transition system: one relies on the actions, theother on the labels of the states. While the action-based approach assumes that onlythe executed actions are observable from outside, the state-based approach ignores theactions and relies on the atomic propositions that hold in the current state to be visible.Transition systems that are deterministic in the action-based view have at most one outgoing transition labeled with action α per state, while determinism from the view of statelabels means that for any state label A ∈ 2AP and any state there is at most one outgoingtransition leading to a state with label A.

Свежие статьи
Популярно сейчас
Как Вы думаете, сколько людей до Вас делали точно такое же задание? 99% студентов выполняют точно такие же задания, как и их предшественники год назад. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Нашёл ошибку?
Или хочешь предложить что-то улучшить на этой странице? Напиши об этом и получи бонус!
Бонус рассчитывается индивидуально в каждом случае и может быть в виде баллов или бесплатной услуги от студизбы.
Предложить исправление
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5057
Авторов
на СтудИзбе
456
Средний доход
с одного платного файла
Обучение Подробнее