Local Distributed Model Checking of RegCTL
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F02%3A00006437" target="_blank" >RIV/00216224:14330/02:00006437 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Local Distributed Model Checking of RegCTL
Original language 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 themodel checking algorithm is well distributable.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GA201%2F00%2F1023" target="_blank" >GA201/00/1023: Algorithms and tools for practical verification of concurrent systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2002
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
PDMC 2002 Parallel and Distributed Model Checking
ISBN
0444512918
ISSN
—
e-ISSN
—
Number of pages
14
Pages from-to
1
Publisher name
Elsevier Science Publishers
Place of publication
The Netherlands
Event location
19.8.2002, Brno, Czech Republic
Event date
Jan 1, 2002
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—