Helsinki University of Technology
Department of Computer Science
Digital Systems Laboratory
Otaniemi, Otakaari 1
FIN>=02150 ESPOO, FINLAND

HELSINKI UNIVERSITY OF TECHNOLOGY

DIGITAL SYSTEMS LABORATORY

Series A: Research Reports ISSN 0783>=5396

No. 45; May 1997 ISBN 951>=22>=3603>=6

MODEL CHECKING THE BRANCHING TIME TEMPORAL

LOGIC CTL

Keijo Heljanko

Digital Systems Laboratory
Department of Computer Science
Helsinki University of Technology
Otaniemi, FINLAND