document: Extending CTL with actions and real time 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 -LRB- UML -RRB- . 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 -LRB- ACTL -RRB- -LRB- 1990 -RRB- and R. Alur et aL -LRB- TCTL -RRB- -LRB- 1993 -RRB- . 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
doc_bio_tags: O O O B O O O O O O O O O O B I O O O O O O O O B I I O O O O O O O O O O B I I O O O O O O O O O O B I O O O O O O O O O O O O O O O B I O O O O O O O O O O B O O O O O O O O O B O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B I I