Publication details
Model Checking of RegCTL
| Basic information | |
|---|---|
| Original title: | Model Checking of RegCTL |
| Authors: | Ivana Černá, Tomáš Brázdil |
| Further information | |
|---|---|
| Citation: | ČERNÁ, Ivana  - BRÁZDIL, Tomáš. Model Checking of RegCTL. Computing and Informatics, Slovakia. ISSN 1335-9150, 2006, vol. 25, no. 1, pp. 81-97. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Periodical |
| Keywords: | model checking; RegCTL temporal logic |
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:
- Techniques for automatic verification and validation of software nad hardware systems
- Highly Parallel and Distributed Computing Systems
- Automated software verification
