Gore, RajeevThomson, JamesWidmann, Florian2015-12-08September9781457712425http://hdl.handle.net/1885/37632We compare implementations of five theorem provers for Computation Tree Logic (CTL) based on treetableaux, graph-tableaux, binary decision diagrams, resolution and games using formula-classes from the literature. In the process, we gather and analyse a set of test formulae which could form the basis of a suite of benchmark formulae for CTL.Keywords: Automated reasoning; Computation tree logic; Experimental comparison; Theorem provers; Automata theory; Forestry; Temporal logic; Binary decision diagrams; Algorithms; Computation; Experimentation; Forestry Automated reasoning; Computation tree logic; Experimental comparison201110.1109/TIME.2011.162016-02-24