Model Checking of RegCTL

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ČERNÁ Ivana BRÁZDIL Tomáš

Year of publication 2006
Type Article in Periodical
Magazine / Source Computing and Informatics
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords model checking; RegCTL temporal logic
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.