{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:36:54Z","timestamp":1725550614701},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291053"},{"type":"electronic","value":"9783540320302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_7","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"50-64","source":"Crossref","is-referenced-by-count":21,"title":["Verifying Quantitative Properties Using Bound Functions"],"prefix":"10.1007","author":[{"given":"Arindam","family":"Chakrabarti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM\u00a049, 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0890-5401(03)00038-5","volume":"182","author":"P. Bouyer","year":"2003","unstructured":"Bouyer, P., Petit, A., Th\u00e9rien, D.: An algebraic approach to data languages and timed languages. Information & Computation\u00a0182, 137\u2013162 (2003)","journal-title":"Information & Computation"},{"key":"7_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information & Computation\u00a098, 142\u2013170 (1992)","journal-title":"Information & Computation"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-540-45212-6_9","volume-title":"Embedded Software","author":"A. Chakrabarti","year":"2003","unstructured":"Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol.\u00a02855, pp. 117\u2013133. Springer, Heidelberg (2003)"},{"key":"7_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"Dam, M.: CTL* and ECTL* as fragments of the modal \u03bc-calculus. Theoretical Computer Science\u00a0126, 77\u201396 (1994)","journal-title":"Theoretical Computer Science"},{"key":"7_CR9","first-page":"279","volume-title":"LICS","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: Dynamic programs for \u03c9-regular objectives. In: LICS, pp. 279\u2013290. IEEE, Los Alamitos (2001)"},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1016\/j.jcss.2003.07.009","volume":"68","author":"L. Alfaro de","year":"2004","unstructured":"de Alfaro, L., Majumdar, R.: Quantitative solution of concurrent games. J. Computer & Systems Sciences\u00a068, 374\u2013397 (2004)","journal-title":"J. Computer & Systems Sciences"},{"key":"7_CR11","first-page":"267","volume-title":"LICS","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Lei, C.: Efficient model checking in fragments of the propositional \u03bc-calculus. In: LICS, pp. 267\u2013278. IEEE, Los Alamitos (1986)"},{"key":"7_CR12","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"key":"7_CR13","first-page":"111","volume-title":"LICS","author":"M. Huth","year":"1997","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: LICS, pp. 111\u2013122. IEEE, Los Alamitos (1997)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44612-5_38","volume-title":"Mathematical Foundations of Computer Science 2000","author":"O.H. Ibarra","year":"2000","unstructured":"Ibarra, O.H., Su, J., Dang, Z., Bultan, T., Kemmerer, R.A.: Counter machines: Decidable properties and applications to verification problems. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.\u00a01893, pp. 426\u2013435. Springer, Heidelberg (2000)"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"7_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-36078-6_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. McIver","year":"2002","unstructured":"McIver, A., Morgan, C.: Games, probability, and the quantitative \u03bc-calculus. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 292\u2013310. Springer, Heidelberg (2002)"},{"key":"7_CR17","first-page":"250","volume-title":"POPL","author":"M.Y. Vardi","year":"1988","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: POPL, pp. 250\u2013259. ACM, New York (1988)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-45069-6_8","volume-title":"Computer Aided Verification","author":"G. Xie","year":"2003","unstructured":"Xie, G., Dang, Z., Ibarra, O.H., Pietro, P.S.: Dense counter machines and verification problems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 93\u2013105. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:13:14Z","timestamp":1619507594000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11560548_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}