Model Checking of RegCTL

keywords: Finite state system, regular expression, tree automaton, temporal logic, model checking
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 and exactly state the complexity of model checking RegCTL formulas.
reference: Vol. 25, 2006, No. 1, pp. 81–97