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.
Speaker bio
John McCabe-Dansted is a Post-Doc working with Mark Reynolds at the University of Western Australia. His masters thesis from Auckland University in New Zealand was on the approximability and computational properties of a voting rule suggested by Lewis Carrol. His PhD thesis at UWA proposed an extension RoCTL* of the Full Computation Tree Logic (CTL*), and studied the expressiveness, succinctness and decision procedures for RoCTL*. Since then he has studied model checking procedures for General linear flows of time and the Real Temporal Logic (RTL), and is interested in Metric Temporal Logics and tools for verification of software.Share this:
