A Faster Tableau for CTL*

A Faster Tableau for CTL*

There have been several recent suggestions for tableau systems for deciding satisfiability in the practically important branching time temporal logic known as CTL*. In this paper we present a streamlined and more traditional tableau approach built upon the author's earlier theoretical work. Sou...

Full description

Bibliographic Details
Main Author: Mark Reynolds
Format: Article
Language:English
Published: Open Publishing Association 2013-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1307.4468v1
id doaj-5fc841059fd644038c74fcdc2cb1d160
record_format Article
spelling doaj-5fc841059fd644038c74fcdc2cb1d1602020-11-24T21:03:49ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-07-01119Proc. GandALF 2013506310.4204/EPTCS.119.7A Faster Tableau for CTL*Mark ReynoldsThere have been several recent suggestions for tableau systems for deciding satisfiability in the practically important branching time temporal logic known as CTL*. In this paper we present a streamlined and more traditional tableau approach built upon the author's earlier theoretical work. Soundness and completeness results are proved. A prototype implementation demonstrates the significantly improved performance of the new approach on a range of test formulas. We also see that it compares favourably to state of the art, game and automata based decision procedures.http://arxiv.org/pdf/1307.4468v1
collection DOAJ
language English
format Article
sources DOAJ
author Mark Reynolds
spellingShingle Mark Reynolds
A Faster Tableau for CTL*
Electronic Proceedings in Theoretical Computer Science
author_facet Mark Reynolds
author_sort Mark Reynolds
title A Faster Tableau for CTL*
title_short A Faster Tableau for CTL*
title_full A Faster Tableau for CTL*
title_fullStr A Faster Tableau for CTL*
title_full_unstemmed A Faster Tableau for CTL*
title_sort faster tableau for ctl*
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2013-07-01
description There have been several recent suggestions for tableau systems for deciding satisfiability in the practically important branching time temporal logic known as CTL*. In this paper we present a streamlined and more traditional tableau approach built upon the author's earlier theoretical work. Soundness and completeness results are proved. A prototype implementation demonstrates the significantly improved performance of the new approach on a range of test formulas. We also see that it compares favourably to state of the art, game and automata based decision procedures.
url http://arxiv.org/pdf/1307.4468v1
work_keys_str_mv AT markreynolds afastertableauforctl
AT markreynolds fastertableauforctl
_version_ 1716772850777456640

Similar Items