UPDATING OF CTL OPERATORS AND THEIR CHECK ALGORITHMS ON KRIPKE STRUCTURE
Abstract
In this article, extension of some temporal CTL logics operators is proposed,
which enables explicit indication of the number of system states or the number of ways
wherein the preset feature of the system is realized. Semantics, formal grammar, as well
as relevant Kripke structure and extended temporal operators based feasibility check algorithms
are given.
which enables explicit indication of the number of system states or the number of ways
wherein the preset feature of the system is realized. Semantics, formal grammar, as well
as relevant Kripke structure and extended temporal operators based feasibility check algorithms
are given.
References
1. Pnueli, A.. The temporal logic of programs [Text]. //Proc. of 18-th IEEE Symposium on Foundations of Computer Science, pp. 46-57, 1977.
2. Clarke, J.E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic [Text]. //A Series of Lecture Notes in Computer Science. - V. 131, pp.52-71, Springer, 1981.
3. Кларк, Э., Грамберг, О., Пелед, Д. Верификация моделей программ: Model Checking [Текст]. - М.: МЦНМО, 2002, с. 56-61.
4. Карпов, Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем[Текст]. - СПб.: БХВ-Петербург, 2010, с. 41-73.
Review
Views:
62
Email this article 