Главная » Просмотр файлов » 5. Principles of Model Checking. Baier_ Joost (2008)

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

Файл №811406 5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf) 64 страница5. Principles of Model Checking. Baier_ Joost (2008) (811406) страница 642020-08-25СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 64)

The foundations of this algorithm are discussed and the adaptationsneeded to incorporate fairness are detailed. This is followed by an algorithm for thegeneration of counterexamples. The chapter is concluded by presenting a model-checkingalgorithm for CTL∗ , a branching-time logic that subsumes both LTL and CTL.6.1IntroductionPnueli [337] has introduced linear temporal logic for the specification and verification ofreactive systems. LTL is called linear, because the qualitative notion of time is path-basedand viewed to be linear: at each moment of time there is only one possible successor stateand thus each time moment has a unique possible future.

Technically speaking, this followsfrom the fact that the interpretation of LTL formulae is defined in terms of paths, i.e.,sequences of states.Paths themselves, though, are obtained from a transition system that might be branching:a state may have several, distinct direct successor states, and thus several computationsmay start in a state. The interpretation of LTL-formulae in a state requires that a formulaϕ holds in state s if all possible computations that start in s satisfy ϕ. The universal313314Computation Tree Logicquantification over all computations that is implicit in the LTL semantics can also bemade explicit in the formula, e.g.:s |= ∀ϕ if and only if π |= ϕ for all paths π starting in sIn LTL, we thus can state properties over all possible computations that start in a state,but not easily about some of such computations.

To some extent this may be overcomeby exploiting the duality between universal and existential quantification. For instance, tocheck whether there exists some computation starting in s that satisfies ϕ we may checkwhether s |= ∀ ¬ ϕ; if this formula is not satisfied by s, then there must be a computationthat meets ϕ, otherwise they should all refute ϕ.For more complicated properties, like “for every computation it is always possible to returnto the initial state”, this is, however, not possible. A naive attempt would be to require ♦ start for every computation, i.e., s |= ∀ ♦ start, where the proposition start uniquelyidentifies the initial state. This is, however, too strong as it requires a computation toalways return to the initial state, not just possibly.

Other attempts to specify the intendedproperty also fail, and it even turns out to be the case that the property cannot be specifiedin LTL.To overcome these problems, in the early eighties another strand of temporal logics forspecification and verification purposes was introduced by Clarke and Emerson [86]. Thesemantics of this kind of temporal logic is not based on a linear notion of time—an infinitesequence of states—but on a branching notion of time—an infinite tree of states. Branchingtime refers to the fact that at each moment there may be several different possible futures.Each moment of time may thus split into several possible futures.

Due to this branchingnotion of time, this class of temporal logic is known as branching temporal logic. Thesemantics of a branching temporal logic is defined in terms of an infinite, directed treeof states rather than an infinite sequence. Each traversal of the tree starting in its rootrepresents a single path. The tree itself thus represents all possible paths, and is directlyobtained from a transition system by “unfolding” at the state of interest. The tree rootedat state s thus represents all possible infinite computations in the transition system thatstart in s.

Figure 6.1 depicts a transition system and its unfolding. (For convenience, eachnode in the tree consists of a pair indicating the state and the level of the node in thetree.)The temporal operators in branching temporal logic allow the expression of properties ofsome or all computations that start in a state.

To that end, it supports an existentialpath quantifier (denoted ∃) and a universal path quantifier (denoted ∀). For instance, theproperty ∃♦ Φ denotes that there exists a computation along which ♦ Φ holds. That is,it states that there is at least one possible computation in which a state that satisfies ΦIntroduction315(s0 , 0)(s1 , 1)s1 { x = 0 }s0{ x = 0 }(s2 , 2)s2 { x = 0 }s3{ x = 1, x = 0 }(a)(s3 , 3)(s2 , 4)(s3 , 2)(s2 , 3)(s3 , 3)(s3 , 4) (s3 , 4)(s2 , 4)(s3 , 4)(b)Figure 6.1: (a) A transition system and (b) a prefix of its infinite computation treeis eventually reached. This does not, however, exclude the fact that there can also becomputations for which this property does not hold, for instance, computations for whichΦ is always refuted. The property ∀♦ Φ, in contrast, states that all computations satisfythe property ♦ Φ.

More complicated properties can be expressed by nesting universaland existential path quantifiers. For instance, the aforementioned property “for everycomputation it is always possible to return to the initial state” can be faithfully expressedby ∀ ∃♦ start: in any state () of any possible computation (∀), there is a possibility (∃)to eventually return to the start state (♦ start).This chapter considers Computation Tree Logic (CTL), a temporal logic based on propositional logic with a discrete notion of time, and only future modalities. CTL is an importantbranching temporal logic that is sufficiently expressive for the formulation of an important set of system properties.

It was originally used by Clarke and Emerson [86] and (ina slightly different form) by Queille and Sifakis [347] for model checking. More importantly, it is a logic for which efficient and—as we will see—rather simple model-checkingalgorithms do exist.Anticipatory to the results presented in this chapter, we summarize the major aspects ofthe linear-vs-branching-time debate and provide arguments that justify the treatment ofmodel checking based on linear or branching time logics:• The expressiveness of many linear and branching temporal logics is incomparable.This means that some properties that are expressible in a linear temporal logiccannot be expressed in certain branching temporal logics, and vice versa.316Computation Tree LogicAspectLinear timeBranching time“behavior”in a state spath-based:trace(s)state-based:computation tree of stemporallogicLTL: path formulae ϕs |= ϕ iff∀π ∈ Paths(s).

π |= ϕCTL: state formulaeexistential path quantification ∃ϕuniversal path quantification: ∀ϕcomplexity of themodel checkingproblemsPSPACE–completePTIMEO (|TS| · exp(|ϕ|))O(|TS| · |Φ|)implementationrelationtrace inclusion and the like(proof is PSPACE-complete)simulation and bisimulation(proof in polynomial time)fairnessno special techniques neededspecial techniques neededTable 6.1: Linear-time vs.

branching-time in a nutshell.• The model-checking algorithms for linear and branching temporal logics are quitedifferent. This results, for instance, in significantly different time and space complexity results.• The notion of fairness can be treated in linear temporal logic without the need forany additional machinery since fairness assumptions can be expressed in the logic.For various branching temporal logics this is not the case.• The equivalences and preorders between transition systems that “correspond” tolinear temporal logic are based on traces, i.e., trace inclusion and equality, whereasfor branching temporal logic such relations are based on simulation and bisimulationrelations (see Chapter 7).Table 6.1 summarizes the main differences between the linear-time and branching-timeperspective in a succinct way.Computation Tree Logic6.2317Computation Tree LogicThis section presents the syntax and the semantics of CTL.

The following sections willdiscuss the relation and differences between CTL and LTL, present a model-checkingalgorithm for CTL, and introduce some extensions of CTL.6.2.1SyntaxCTL has a two-stage syntax where formulae in CTL are classified into state and pathformulae. The former are assertions about the atomic propositions in the states and theirbranching structure, while path formulae express temporal properties of paths. Comparedto LTL formulae, path formulae in CTL are simpler: as in LTL they are built by thenext-step and until operators, but they must not be combined with Boolean connectivesand no nesting of temporal modalities is allowed.Definition 6.1.Syntax of CTLCTL state formulae over the set AP of atomic proposition are formed according to thefollowing grammar:Φ ::= trueaΦ1 ∧ Φ2¬Φ∃ϕ∀ϕwhere a ∈ AP and ϕ is a path formula.

CTL path formulae are formed according to thefollowing grammar:ϕ ::= ΦΦ1 U Φ2where Φ, Φ1 and Φ2 are state formulae.Greek capital letters will denote CTL state formulae (CTL formulae, for short), whereaslowercase Greek letters will denote CTL path formulae.CTL distinguishes between state formulae and path formulae. Intuitively, state formulaeexpress a property of a state, while path formulae express a property of a path, i.e., aninfinite sequence of states. The temporal operators and U have the same meaning asin LTL and are path operators.

Formula Φ holds for a path if Φ holds at the nextstate in the path, and Φ U Ψ holds for a path if there is some state along the path forwhich Ψ holds, and Φ holds in all states prior to that state. Path formulae can be turnedinto state formulae by prefixing them with either the path quantifier ∃ (pronounced “forsome path”) or the path quantifier ∀ (pronounced “for all paths”). Note that the linear318Computation Tree Logictemporal operators and U are required to be immediately preceded by ∃ or ∀ to obtaina legal state formula. Formula ∃ϕ holds in a state if there exists some path satisfying ϕthat starts in that state.

Характеристики

Тип файла
PDF-файл
Размер
5,5 Mb
Тип материала
Высшее учебное заведение

Список файлов книги

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