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]

open access
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
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 119065