An Experimental Comparison of Theorem Provers for CTL

Date

2011

Authors

Gore, Rajeev
Thomson, James
Widmann, Florian

Journal Title

Journal ISSN

Volume Title

Publisher

IEEE Computer Society

Abstract

We 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.

Description

Keywords

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 comparison

Citation

Source

Proceedings of TIME 2011

Type

Conference paper

Book Title

Entity type

Access Statement

License Rights

Restricted until

2037-12-31