Model Checking of RegCTL
| Authors | |
|---|---|
| Year of publication | 2006 |
| Type | Article in Periodical |
| Magazine / Source | Computing and Informatics |
| MU Faculty or unit | |
| 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: |