A branching time temporal framework for quantitative reasoning

Chatterjee, Krishnendu ; Dasgupta, Pallab ; Chakrabarti, P. P. (2003) A branching time temporal framework for quantitative reasoning Journal of Automated Reasoning, 30 (2). pp. 205-232. ISSN 0168-7433

Full text not available from this repository.

Official URL: http://www.springerlink.com/content/k0561177376106...

Related URL: http://dx.doi.org/10.1023/A:1023217515688


Temporal logics such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) have become popular for specifying temporal properties over a wide variety of planning and verification problems. In this paper we work towards building a generalized framework for automated reasoning based on temporal logics. We present a powerful extension of CTL with first-order quantification over the set of reachable states for reasoning about extremal properties of weighted labeled transition systems in general. The proposed logic, which we call Weighted Quantified Computation Tree Logic (WQCTL), captures the essential elements common to the domain of planning and verification problems and can thereby be used as an effective specification language in both domains. We show that in spite of the rich, expressive power of the logic, we are able to evaluate WQCTL formulas in time polynomial in the size of the state space times the length of the formula. Wepresent experimental results on the WQCTL verifier.

Item Type:Article
Source:Copyright of this article belongs to Springer-Verlag.
Keywords:Computation Tree Logic; Temporal Logics; Quantitative Reasoning
ID Code:6013
Deposited On:19 Oct 2010 09:51
Last Modified:20 May 2011 09:33

Repository Staff Only: item control page