Name
Abstract | ||
|---|---|---|
Computation tree logic (CTL) is expressive to specify those qualitative properties which focus on the temporal order of events. It, however, lacks to specify quantitative temporal requirements, which put time constraints on the occurrence of events. Thus, this paper presents a novel variant of temporal logic, RCTL (Region Computation Tree Logic), that extends CTL by incorporating the notation of time explicitly. To accomplish this aim, the paper uses hybrid automata as a model of computation. The specification language of RCTL allows us to express many properties in a concise and intuitive manner. To bring model checking within the scope of RCTL, the paper focuses on the specification of those properties that can be verified using reachability analysis, which is implemented in a previous work. |
Year | Venue | Field |
|---|---|---|
2010 | MSVVEIS 2010: MODELLING, SIMULATION, VERIFICATION AND VALIDATION OF ENTERPRISE INFORMATION SYSTEMS | Programming language,Computer science,CTL* |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ammar Mohammed | 1 | 17 | 4.72 |
| Ulrich Furbach | 2 | 639 | 88.23 |