Reducing the extensions of CTL with actions and real time

Share/Save/Bookmark

Jansen, David N. and Wieringa, Roel J. (2000) Reducing the extensions of CTL with actions and real time. [Report]

[img]
Preview
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