Model Checking of RegCTL
Tomáš Brázdil ; Ivana Černá
Computing and Informatics, Tome 28 (2012) no. 1, / Harvested from Computing and Informatics
Text on Computing and Informatics
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.
Publié le : 2012-01-26
Classification:  Finite state system; regular expression; tree automaton; temporal logic; model checking 
@article{cai334,
     author = {Tom\'a\v s Br\'azdil and Ivana \v Cern\'a},
     title = {Model Checking of RegCTL},
     journal = {Computing and Informatics},
     volume = {28},
     number = {1},
     year = {2012},
     language = {en},
     url = {http://dml.mathdoc.fr/item/cai334}
}

Tomáš Brázdil; Ivana Černá. Model Checking of RegCTL. Computing and Informatics, Tome 28 (2012) no. 1, . http://gdmltest.u-ga.fr/item/cai334/