DocumentCode :
3441447
Title :
A Tableau for the Combination of CTL and BCTL
Author :
Cabe-Dansted, John C M
Author_Institution :
Sch. of Comput. Sci. & Software Eng., Univ. of Western Australia, Perth, WA, Australia
fYear :
2012
fDate :
12-14 Sept. 2012
Firstpage :
29
Lastpage :
36
Abstract :
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 abounded number of path-sub formulae. The existing pure tableau for CTL* was 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.
Keywords :
automata theory; decision making; formal logic; trees (mathematics); BCTL*; CTL*; automata; bundled variant; computation tree logic; exponential decision procedure; path-sub formulae; tableau; Automata; Color; Gold; Semantics; Syntactics; Bundled; Exptime; Logic; Tableaux; Temporal;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Temporal Representation and Reasoning (TIME), 2012 19th International Symposium on
Conference_Location :
Leicester
ISSN :
1530-1311
Print_ISBN :
978-1-4673-2659-9
Type :
conf
DOI :
10.1109/TIME.2012.17
Filename :
6311112
Link To Document :
بازگشت