Exploiting partitioned transition relations for efficient symbolic model checking in CTL

We present an efficient tool for symbolic state space traversal of finite state machines. Both algorithms for searching reachable states and for model checking in CTL owe their efficiency primarily to the use of partitioned transition relations. Partitioning of the relations is fully automatic.