CTL Model Checker
After lots of trouble with flex and bison, we finally have a CTL Model Checker - a system that determines the vertices in a graph, at which a given CTL formula holds. For example the vertices without successors are the ones that satisfy the formula 'A X \bot'