Title
A Tableau for Bundled CTL
Abstract
We present a sound, complete and relatively straightforward tableau method for deciding valid formulas in the propositional version of the bundled (or suffix and fusion closed) computation tree logic BCTL*. This proves that BCTL* is decidable. It is also moderately useful to have a tableau available for a reasonably expressive branching-time temporal logic. However, the main interest in this shoul...
Year
DOI
Venue
2007
10.1093/logcom/exl033
Journal of Logic and Computation
Keywords
Field
DocType
Temporal logic,branching-time logic,tableau,full computation tree logic,theorem proving
Discrete mathematics,Algebra,CTL*,Mathematics
Journal
Volume
Issue
ISSN
17
1
0955-792X
Citations 
PageRank 
References 
15
0.82
0
Authors
1
Name
Order
Citations
PageRank
Mark Reynolds19315.44