A branching time temporal framework for quantitative reasoning Journal Article


Author(s): Chatterjee, Krishnendu; Dasgupta, Pallab; Chakrabarti, Partha P
Article Title: A branching time temporal framework for quantitative reasoning
Affiliation
Abstract: 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.
Keywords: computation tree logic; temporal logics; quantitative reasoning
Journal Title: Journal of Automated Reasoning
Volume: 30
Issue 2
ISSN: 1573-0670
Publisher: Springer  
Date Published: 2003-02-01
Start Page: 205
End Page: 232
DOI: 10.1023/A:1023217515688
Open access: no
IST Austria Authors
Related IST Austria Work