Local Distributed Model Checking of RegCTL Tomas Brazdil and Ivana Cerna
The paper is devoted to the problem of extending the temporal logic
CTL so as it is more expressive and complicated properties can be
expressed more succinctly. The specification language RegCTL, an
extension of CTL, is proposed. In RegCTL every CTL temporal operator is
augmented with a regular expression restricting thus moments when the
validity is required. The resulting logic is more expressive than
previous extensions of CTL with regular expressions. RegCTL can be
model-checked on-the-fly and the model checking algorithm is well
distributable.
|