title: Extending CTL with actions and real time
abstract: In this paper, 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 R. De Nicola and F. Vaandrager (ACTL) (1990) and R. Alur et aL (TCTL) (1993). 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
keyphrases: actions logic ATCTL model checking models Unified Modelling Language formal semantics specification language Kronos model checker real time logic computation tree logic