CTL (Computation Tree Logic) – бағдарламалық жасақтама мен аппараттық құралдарды тексеруге арналған уақыт логикасы. Қауіпсіздік пен тірілік қасиеттерін анықтайды.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы 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 формулалары сондай-ақ boolean тұрақтыларын 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-дің өзінен кіші жиынтық болып табылады. Мысалы, 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-толық, бірақ қанағаттандыру шешілмейді. QBF шешушілерін пайдалану мақсатында, құрылым семантикасымен QCTL модельді тексеру мәселесін TQBF (нағыз сандықталған Буль формулалары) түріне келтіру ұсынылды.
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.