Model Checking of RegCTL
Keywords:
Finite state system, regular expression, tree automaton, temporal logic, model checkingAbstract
The paper is devoted to the problem of extending the temporal logic CTL so that it is more expressive and complicated properties can be expressed in a more readable form. The specification language RegCTL, an extension of CTL, is proposed. In RegCTL every CTL temporal operator is augmented with a regular expression, thus restricting moments when the validity is required. We propose a local distributed model checking algorithm for RegCTL.
Downloads
Download data is not yet available.
Downloads
Published
2012-01-30
How to Cite
Brázdil, T., & Černá, I. (2012). Model Checking of RegCTL. Computing and Informatics, 25(1), 81–97. Retrieved from http://147.213.75.17/ojs/index.php/cai/article/view/334
Issue
Section
Articles