Abstract
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.
Keywords
Cite this article
@article{cai-1520,
author = {Tomáš Brázdil and Ivana Černá},
title = {Model Checking of RegCTL},
journal = {Computing and Informatics},
volume = {25},
number = {1},
pages = {81--97},
year = {2006},
issn = {1335-9150},
url = {https://cai.type.sk/content/2006/1/model-checking-of-regctl/}
}
TY - JOUR AU - Tomáš Brázdil AU - Ivana Černá TI - Model Checking of RegCTL JO - Computing and Informatics VL - 25 IS - 1 SP - 81 EP - 97 PY - 2006 SN - 1335-9150 UR - https://cai.type.sk/content/2006/1/model-checking-of-regctl/ KW - Finite state system KW - regular expression KW - tree automaton KW - temporal logic KW - model checking ER -
Brázdil, T., & Černá, I. (2006). Model Checking of RegCTL. Computing and Informatics, 25(1), 81–97. https://cai.type.sk/content/2006/1/model-checking-of-regctl/