{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:08Z","timestamp":1761611108495,"version":"3.41.0"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2003,2]]},"DOI":"10.1023\/a:1023217515688","type":"journal-article","created":{"date-parts":[[2003,6,6]],"date-time":"2003-06-06T17:39:54Z","timestamp":1054921194000},"page":"205-232","source":"Crossref","is-referenced-by-count":1,"title":["A Branching Time Temporal Framework for Quantitative Reasoning"],"prefix":"10.1007","volume":"30","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. P.","family":"Chakrabarti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"5118854_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R. and Henzinger, T.: Real time logics: Complexity and expressiveness, Inform. and Comput.\n104(1) (1993), 35-77.","journal-title":"Inform. and Comput."},{"key":"5118854_CR2","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1018985923441","volume":"22","author":"F. Bacchus","year":"1998","unstructured":"Bacchus, F. and Kabanza, F.: Planning for temporally extended goals, Ann. Math. Artificial Intelligence\n22 (1998), 5-27.","journal-title":"Ann. Math. Artificial Intelligence"},{"key":"5118854_CR3","unstructured":"Baier, C. and Clarke, E. M.: The algebraic \u00b5-calculus and MTBDDs, in Proc. 5th Workshop on Logic, Language, Information and Computation (WoLLIC\u2019 98), 1998, pp. 27-38."},{"issue":"2","key":"5118854_CR4","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E. A. and Sistla, A. P.: Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. on Program. Lang. and Systems\n8(2) (1986), 244-263.","journal-title":"ACM Trans. on Program. Lang. and Systems"},{"key":"5118854_CR5","volume-title":"Model Checking","author":"E. M. Clarke","year":"2000","unstructured":"Clarke, E. M., Grumberg, O. and Peled, D. A.: Model Checking, MIT Press, Cambridge, MA, 2000."},{"key":"5118854_CR6","volume-title":"Introduction to Algorithms","author":"T. H. Cormen","year":"1990","unstructured":"Cormen, T. H., Leiserson, C. E. and Rivest, R. L.: Introduction to Algorithms, MIT Press, Cambridge, MA, and McGraw-Hill, 1990."},{"key":"5118854_CR7","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0004-3702(01)00059-5","volume":"127","author":"P. Dasgupta","year":"2001","unstructured":"Dasgupta, P., Chakrabarti, P. P., Deka, J. K. and Sriram, S.: Min-max computation tree logic, Artificial Intelligence\n127 (2001), 137-162.","journal-title":"Artificial Intelligence"},{"key":"5118854_CR8","unstructured":"Emerson, E. A., Mok, A. K., Sistla, A. P. and Srinivasan, J.: Quantitative temporal reasoning, in First Annual Workshop on Computer-Aided Verification, France, 1989."},{"key":"5118854_CR9","unstructured":"Giacomo, G. D. and Vardi, M. Y.: Automata-theoretic approach to planning for temporally extended goals, in Proc. of ECP, 1999."},{"key":"5118854_CR10","unstructured":"Mandal, C. R., Cadouri, E., Chakrabarti, P. P., Chatterjee, B. and Majumder, J.: Netlist database reference manual 3.0, National Semiconductor Corp and IIT Kharagpur, 2001 (mail to: bijoy@nsc.com, ppchak@cse.iitkgp.ernet.in)."},{"key":"5118854_CR11","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0020-0190(01)00260-5","volume":"82","author":"A. C. Patthak","year":"2002","unstructured":"Patthak, A. C., Bhattacharya, I., Dasgupta, A., Dasgupta, P. and Chakrabarti, P. P.: Quantified computation tree logic, Inform. Process. Lett.\n82 (2002), 123-129.","journal-title":"Inform. Process. Lett."},{"key":"5118854_CR12","doi-asserted-by":"crossref","unstructured":"Penfield, P. and Rubenstein, J.: Signal delay in RC tree networks, in Proc. of 19th Design Automation Conference, 1981.","DOI":"10.1109\/DAC.1981.1585417"},{"key":"5118854_CR13","doi-asserted-by":"crossref","unstructured":"Pillage, L. T. and Rohrer, R. A.: Asymptotic waveform evaluation for timing analysis, IEEE Transactions on Computer Aided Design\n9(4) (1990).","DOI":"10.1109\/43.45867"},{"key":"5118854_CR14","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs, in Proc. of FOCS\u201977, 1977, pp. 46-57.","DOI":"10.1109\/SFCS.1977.32"},{"key":"5118854_CR15","unstructured":"Sarkar, S., Chakrabarti, P. P., Niyogi, R. and Dasgupta, P.: Specification of planning goals in branching time logics in stochastic systems, in Proc. of KBCS 2000: Int. Conf. on Knowledge Based Computer Systems, Mumbai, India, 2000."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1023217515688.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1023217515688\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1023217515688.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:45:05Z","timestamp":1749123905000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1023217515688"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["5118854"],"URL":"https:\/\/doi.org\/10.1023\/a:1023217515688","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2003,2]]}}}