A Tableau for the Combination of CTL and BCTL*
John McCabe-Dansted ( University of Western Australia )
- 11:30 26th September 2012051
It is known that there is an exponential decision procedure for CTL. Given that important properties cannot be expressed in CTL, we seek a pure tableau based decision procedure (that does not rely on translations into automata) that is exponential for formulas that have only a bounded number of non-CTL properties. In this paper we present such a tableau for a combination of CTL and a bundled variant (BCTL*) of CTL* that is singly exponential for formulae with a bounded number of path-subformulae. The existing pure tableau for CTL* built upon the pure tableau for BCTL*, so this paper is also a natural first step towards a pure tableau technique for CTL* that is singly exponential when similarly restricted.