XTL

XTL (eXecutable Temporal Language) is a functional programming language interpreted over LTSs (Labelled Transition Systems) encoded in the BCG (Binary Coded Graph) file format. XTL can typically be used for implementing temporal logic operators, by describing their fixed point semantics as iterative or recursive computations over sets of states. More generally, XTL enables one to perform any computation on a BCG graph: for instance, it can compute the branching factor of a graph, print its list of labels, etc. XTL programs are compiled and evaluated on BCG graphs by using the xtl model checker.