Publication details
Local Distributed Model Checking of RegCTL
| Basic information | |
|---|---|
| Original title: | Local Distributed Model Checking of RegCTL |
| Authors: | Ivana Černá, Tomáš Brázdil |
| Further information | |
|---|---|
| Citation: | ČERNÁ, Ivana and Tomáš BRÁZDIL. Local Distributed Model
Checking of RegCTL (Local Distributed Model Checking of
RegCTL). In PDMC 2002 Parallel and Distributed Model Checking.
The Netherlands: Elsevier Science Publishers, 2002. p. 1 -14.
ISBN 0444512918.Export BibTeX@inproceedings{405442, author = {Černá, Ivana and Brázdil, Tomáš}, address = {The Netherlands}, booktitle = {PDMC 2002 Parallel and Distributed Model Checking}, keywords = {model checking}, language = {eng}, location = {The Netherlands}, isbn = {0444512918}, pages = {1 -14},publisher = {Elsevier Science Publishers}, title = {Local Distributed Model Checking of RegCTL}, year = {2002} } |
| Original language: | English |
| Field: | Informatics |
| Type: | Article in Proceedings |
| Keywords: | model checking |
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:
- Algorithms and tools for practical verification of concurrent systems.
- Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
