Local Distributed Model Checking of RegCTL

Investor logo

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ČERNÁ Ivana BRÁZDIL Tomáš

Year of publication 2002
Type Article in Proceedings
Conference PDMC 2002 Parallel and Distributed Model Checking
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords model checking
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 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.
Related projects:

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

More info