An experimental comparison of theorem provers for CTL

Rajeev Goŕe; Jimmy Thomson; Florian Widmann

doi:10.1109/TIME.2011.16

An experimental comparison of theorem provers for CTL

Rajeev Goŕe^*, Jimmy Thomson, Florian Widmann

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

15 Citations (Scopus)

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.

Original language	English
Title of host publication	Proceedings - 18th International Symposium on Temporal Representation and Reasoning, TIME 2011
Pages	49-56
Number of pages	8
DOIs	https://doi.org/10.1109/TIME.2011.16
Publication status	Published - 2011
Event	18th International Symposium on Temporal Representation and Reasoning, TIME 2011 - Lubeck, Germany Duration: 12 Sept 2011 → 14 Sept 2011

Publication series

Name	Proceedings of the International Workshop on Temporal Representation and Reasoning

Conference

Conference	18th International Symposium on Temporal Representation and Reasoning, TIME 2011
Country/Territory	Germany
City	Lubeck
Period	12/09/11 → 14/09/11

Access to Document

10.1109/TIME.2011.16

Cite this

@inproceedings{3c7dc25b8252471da2e8e32c96b4f0df,

title = "An experimental comparison of theorem provers for CTL",

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.",

keywords = "Automated reasoning, Computation tree logic, Experimental comparison",

author = "Rajeev Go{\'r}e and Jimmy Thomson and Florian Widmann",

year = "2011",

doi = "10.1109/TIME.2011.16",

language = "English",

isbn = "9780769545080",

series = "Proceedings of the International Workshop on Temporal Representation and Reasoning",

pages = "49--56",

booktitle = "Proceedings - 18th International Symposium on Temporal Representation and Reasoning, TIME 2011",

note = "18th International Symposium on Temporal Representation and Reasoning, TIME 2011 ; Conference date: 12-09-2011 Through 14-09-2011",

}

Goŕe, R, Thomson, J & Widmann, F 2011, An experimental comparison of theorem provers for CTL. in Proceedings - 18th International Symposium on Temporal Representation and Reasoning, TIME 2011., 6065228, Proceedings of the International Workshop on Temporal Representation and Reasoning, pp. 49-56, 18th International Symposium on Temporal Representation and Reasoning, TIME 2011, Lubeck, Germany, 12/09/11. https://doi.org/10.1109/TIME.2011.16

An experimental comparison of theorem provers for CTL. / Goŕe, Rajeev; Thomson, Jimmy; Widmann, Florian.
Proceedings - 18th International Symposium on Temporal Representation and Reasoning, TIME 2011. 2011. p. 49-56 6065228 (Proceedings of the International Workshop on Temporal Representation and Reasoning).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - An experimental comparison of theorem provers for CTL

AU - Goŕe, Rajeev

AU - Thomson, Jimmy

AU - Widmann, Florian

PY - 2011

Y1 - 2011

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

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

KW - Automated reasoning

KW - Computation tree logic

KW - Experimental comparison

UR - http://www.scopus.com/inward/record.url?scp=81455132782&partnerID=8YFLogxK

U2 - 10.1109/TIME.2011.16

DO - 10.1109/TIME.2011.16

M3 - Conference contribution

SN - 9780769545080

T3 - Proceedings of the International Workshop on Temporal Representation and Reasoning

SP - 49

EP - 56

BT - Proceedings - 18th International Symposium on Temporal Representation and Reasoning, TIME 2011

T2 - 18th International Symposium on Temporal Representation and Reasoning, TIME 2011

Y2 - 12 September 2011 through 14 September 2011

ER -

An experimental comparison of theorem provers for CTL

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this