CITREELO

This is a basic ROBDD-based symbolic model checker for Computational Tree Logic.

This work is mainly an interpretation of the presentation of CTL symbolic model checking from the course of Roberto Sebastiani.

I wrote this out of curiosity and it has not been extensively tested (besides the tests in "/src/test/").

I use biodivine-lib-bdd as as a backend for the ROBDDs.

The supported CTL operators are:

• &, |, !, =>, <=>, AX, EX, AF, EF, AG, EG, AU, EU

To compute BDDs representing sets of states satisfying CTL formulae, all these operators directly correspond to operations on BDDs i.e., we do not use translation using a minimal set of operators e.g. "AX p -> !EX(!p)".