Reducing the extensions of CTL with actions and real time
Jansen, David N. and Wieringa, Roel J. (2000) Reducing the extensions of CTL with actions and real time. [Report]
| PDF 279Kb |
| Abstract: | In this report, we present the logic ATCTL, which combines two known extensions of CTL, namely ACTL and TCTL. ACTL extends CTL with constructs to describe actions and TCTL extends it with constructs to specify real-time properties. ATCTL combines both extensions. We use ATCTL as a language for property specification in which we can express state properties, action properties, and real-time properties. We show that the result can be reduced to ACTL as well as to TCTL, and therefore also to CTL. This makes model-checking ATCTL possible, because CTL model checkers exist. |
| Item Type: | Report |
| Copyright: | © 2000 University of Twente, CTIT |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Research Group: | |
| Link to this item: | http://purl.utwente.nl/publications/56028 |
| Official URL: | http://eprints.eemcs.utwente.nl/1667/01/tech.rep.pdf |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Repository Staff Only: item control page
Metis ID: 119065

Show download statistics for this publication
Show download statistics for this publication