Reducing the extensions of CTL with actions and real time

D.N. Jansen, Roelf J. Wieringa

    Research output: Book/ReportReportProfessional

    83 Downloads (Pure)


    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.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages20
    Publication statusPublished - Dec 2000

    Publication series

    NameCTIT technical report series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)


    • SCS-Services
    • METIS-119065
    • IR-56028
    • EWI-1667

    Cite this