МОДИФИКАЦИЯ ОПЕРАТОРОВ CTL ЛОГИКИ И ИХ АЛГОРИТМЫ ПРОВЕРКИ НА СТРУКТУРЕ КРИПКЕ
Аннотация
В настоящей статье предложено расширение некоторых темпоральных операторов CTL логики, позволяющее явно указывать количество состояний системы или количество путей, в которых выполняется заданное свойство системы. Дается семантика, формальная грамматика, а так же соответствующие алгоритмы проверки выполнимости на структуре Крипке,расширенных темпоральных операторов.
Список литературы
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.
Рецензия
Просмотров:
61
Послать статью по эл. почте 