Extending CTL with actions and real time

David N Jansen, Roel J. Wieringa

    Research output: Contribution to journalArticleAcademicpeer-review

    5 Citations (Scopus)


    We present the logic ATCTL, which is intended to be used for model checking models that have been specified in a lightweight version of the Unified Modelling Language (UML). Elsewhere, we have defined a formal semantics for LUML to describe the models. This paper's goal is to give a specification language for properties that fits LUML; LUML includes states, actions and real time. ATCTL extends CTL with concurrent actions and real time. It is based on earlier extensions of CTL by De Nicola and Vaandrager (ACTL) and Alur et al. (TCTL). This makes it easier to adapt existing model checkers to ATCTL. To show that we can check properties specified in ATCTL in models specified in LUML, we give a small example using the Kronos model checker.
    Original languageEnglish
    Pages (from-to)607-621
    Number of pages15
    JournalJournal of logic and computation
    Issue number4
    Publication statusPublished - Aug 2002


    • Real-time logic
    • Model checking
    • Action modalities
    • SCS-Services
    • EWI-1666
    • IR-38418
    • METIS-210566


    Dive into the research topics of 'Extending CTL with actions and real time'. Together they form a unique fingerprint.

    Cite this