Логика вычислений с ветвлением времени (CTL) и ее применение в верификации
Computation tree logic
Логика вычислений CTL: проверка безопасности и живости программного и аппаратного обеспечения. Ветвление времени, моделирование, формальная верификация.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Вычислительная древесная логика (CTL) — это логика ветвящегося времени, что означает, что её модель времени имеет древовидную структуру, в которой будущее не предопределено; существует множество возможных путей развития событий, и любой из них может быть реализован. Она используется для формальной верификации программных или аппаратных средств, как правило, с помощью программных приложений, известных как модели-проверщики, которые определяют, обладает ли данное средство свойствами безопасности или живости. Например, CTL может задавать, что если выполняется некоторое начальное условие (например, все переменные программы положительны или на шоссе нет машин, занимающих одновременно две полосы), то все возможные сценарии выполнения программы избегают нежелательного состояния (например, деления на ноль или столкновения двух машин на шоссе). В этом примере свойство безопасности может быть проверено модели-проверщиком, который исследует все возможные переходы из состояний программы, удовлетворяющих начальному условию, и удостоверяется, что все такие сценарии удовлетворяют свойству. Вычислительная древесная логика относится к классу темпоральных логик, в который также входит линейная темпоральная логика (LTL). Хотя существуют свойства, которые можно выразить только в CTL и свойства, которые можно выразить только в LTL, все свойства, выразимые в любой из этих логик, также могут быть выражены в CTL*.
Computation tree logic (CTL) is a branching time logic, meaning that its model of time is a tree like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers, which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied (e. g., all program variables are positive or no cars on a highway straddle two lanes), then all possible executions of a program avoid some undesirable condition (e. g., dividing a number by zero or two cars colliding on a highway). In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic belongs to a class of temporal logics that includes linear temporal logic (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in CTL*.
История
CTL был впервые предложен Эдмундом М. Кларком и Э. Алленом Эмерсоном в 1981 году, которые использовали его для синтеза так называемых скелетов синхронизации, то есть абстракций параллельных программ. С момента появления CTL ведутся споры о сравнительных преимуществах CTL и LTL. Благодаря более высокой вычислительной эффективности при проверке моделей, CTL получила более широкое распространение в промышленности, и многие из наиболее успешных инструментов проверки моделей используют CTL как язык спецификаций.
CTL was first proposed by Edmund M. Clarke and E. Allen Emerson in 1981, who used it to synthesize so called synchronisation skeletons, i. e abstractions of concurrent programs. Since the introduction of CTL, there has been debate about the relative merits of CTL and LTL. Because it is more computationally efficient to model check, CTL has become more common in industrial use, and many of the most successful model checking tools use CTL as a specification language.
Логические операторы
Логические операторы стандартные: ¬, ∨, ∧, ⇒ и ⇔. Наряду с этими операторами, формулы CTL также могут использовать булевы константы true и false.
The logical operators are the usual ones: ¬, ∨, ∧, ⇒ and ⇔. Along with these operators CTL formulas can also make use of the boolean constants true and false.
Отношения с другими логиками
Вычислительная древесная логика (CTL) является подмножеством CTL* и модальной μ-логики. CTL также является фрагментом альтернативной временной логики Алура, Хензингера и Купфермана (ATL). Вычислительная древесная логика (CTL) и линейная временная логика (LTL) являются подмножествами CTL*. CTL и LTL не эквивалентны, и у них есть общее подмножество, которое является собственным подмножеством как CTL, так и LTL. FG. P существует в LTL, но не в CTL. AG(P⇒((EX Q)∧(EX¬Q))) и AG EF P существуют в CTL, но не в LTL.
Computation tree logic (CTL) is a subset of CTL* as well as of the modal μ calculus. CTL is also a fragment of Alur, Henzinger and Kupferman's alternating time temporal logic (ATL). Computation tree logic (CTL) and linear temporal logic (LTL) are both a subset of CTL*. CTL and LTL are not equivalent and they have a common subset, which is a proper subset of both CTL and LTL. FG. P exists in LTL but not in CTL. AG(P⇒((EX. Q)∧(EX¬Q))) and AG. EF. P exist in CTL but not in LTL.
Расширения
CTL был расширен квантификацией второго порядка и превращен в квантифицированную вычислительную древесную логику (QCTL). Существуют две семантики:
CTL has been extended with second order quantification and to quantified computational tree logic (QCTL). There are two semantics:
семантика дерева. Мы помечаем узлы дерева вычислений. QCTL* = QCTL = MSO над деревьями. Проверка моделей и задача выполнимости являются башнево-полными. семантика структуры. Мы помечаем состояния. QCTL* = QCTL = MSO над графами. Проверка моделей является PSPACE-полной, но задача выполнимости неразрешима. Предложено сведение задачи проверки моделей QCTL с семантикой структуры к TQBF (истинно квантифицированным булевым формулам) для использования преимуществ решателей QBF.
the tree semantics. We label nodes of the computation tree. QCTL* = QCTL = MSO over trees. Model checking and satisfiability are tower complete. the structure semantics. We label states. QCTL* = QCTL = MSO over graphs. Model checking is PSPACE complete but satisfiability is undecidable. A reduction from the model checking problem of QCTL with the structure semantics, to TQBF (true quantified Boolean formulae) has been proposed, in order to take advantage of the QBF solvers.