A branching time temporal framework for quantitative reasoning

K. Chatterjee, P. Dasgupta, P. Chakrabarti, Journal of Automated Reasoning 30 (2003) 205–232.

Download
No fulltext has been uploaded. References only!

Journal Article | Published
Author
; ;
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.
Publishing Year
Date Published
2003-02-01
Journal Title
Journal of Automated Reasoning
Volume
30
Issue
2
Page
205 - 232
IST-REx-ID

Cite this

Chatterjee K, Dasgupta P, Chakrabarti P. A branching time temporal framework for quantitative reasoning. Journal of Automated Reasoning. 2003;30(2):205-232. doi:10.1023/A:1023217515688
Chatterjee, K., Dasgupta, P., & Chakrabarti, P. (2003). A branching time temporal framework for quantitative reasoning. Journal of Automated Reasoning, 30(2), 205–232. https://doi.org/10.1023/A:1023217515688
Chatterjee, Krishnendu, Pallab Dasgupta, and Partha Chakrabarti. “A Branching Time Temporal Framework for Quantitative Reasoning.” Journal of Automated Reasoning 30, no. 2 (2003): 205–32. https://doi.org/10.1023/A:1023217515688.
K. Chatterjee, P. Dasgupta, and P. Chakrabarti, “A branching time temporal framework for quantitative reasoning,” Journal of Automated Reasoning, vol. 30, no. 2, pp. 205–232, 2003.
Chatterjee K, Dasgupta P, Chakrabarti P. 2003. A branching time temporal framework for quantitative reasoning. Journal of Automated Reasoning. 30(2), 205–232.
Chatterjee, Krishnendu, et al. “A Branching Time Temporal Framework for Quantitative Reasoning.” Journal of Automated Reasoning, vol. 30, no. 2, Springer, 2003, pp. 205–32, doi:10.1023/A:1023217515688.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar