{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T14:48:52Z","timestamp":1725806932869},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319120959"},{"type":"electronic","value":"9783319120966"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12096-6_25","type":"book-chapter","created":{"date-parts":[[2014,10,10]],"date-time":"2014-10-10T10:04:21Z","timestamp":1412935461000},"page":"278-289","source":"Crossref","is-referenced-by-count":0,"title":["Model Checking (k, d)-Markov Chain with ipLTL"],"prefix":"10.1007","author":[{"given":"Lianyi","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Qingdi","family":"Meng","sequence":"additional","affiliation":[]},{"given":"Guiming","family":"Luo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Prism: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-540-30482-1_21","volume-title":"Formal Methods and Software Engineering","author":"Y. Kwon","year":"2004","unstructured":"Kwon, Y., Agha, G.: Linear inequality ltl (iltl): A model checker for discrete time markov chains. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 194\u2013208. Springer, Heidelberg (2004)"},{"issue":"1","key":"25_CR5","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1109\/TSE.2010.80","volume":"37","author":"Y. Kwon","year":"2011","unstructured":"Kwon, Y., Agha, G.: Verifying the evolution of probability distributions governed by a dtmc. IEEE Transactions on Software Engineering\u00a037(1), 126\u2013141 (2011)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"25_CR6","unstructured":"Papoulis, A., Pillai, S.U.: Probability, random variables, and stochastic processes. Tata McGraw-Hill Education (2002)"},{"issue":"23","key":"25_CR7","doi-asserted-by":"publisher","first-page":"4636","DOI":"10.1093\/nar\/27.23.4636","volume":"27","author":"A.L. Delcher","year":"1999","unstructured":"Delcher, A.L., Harmon, D., Kasif, S., White, O., Salzberg, S.L.: Improved microbial gene identification with glimmer. Nucleic Acids Research\u00a027(23), 4636\u20134641 (1999)","journal-title":"Nucleic Acids Research"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Pinsky, M., Karlin, S.: An introduction to stochastic modeling. Academic press (2010)","DOI":"10.1016\/B978-0-12-381416-6.00001-0"},{"issue":"2","key":"25_CR9","doi-asserted-by":"publisher","first-page":"876","DOI":"10.1214\/aoms\/1177703591","volume":"35","author":"R. Sinkhorn","year":"1964","unstructured":"Sinkhorn, R.: A relationship between arbitrary positive matrices and doubly stochastic matrices. The Annals of Mathematical Statistics\u00a035(2), 876\u2013879 (1964)","journal-title":"The Annals of Mathematical Statistics"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of the Fifteenth IFIP WG6. 1 International Symposium on Protocol Specification, Testing and Verification. IFIP (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Strang, G.: Introduction to linear algebra. SIAM (2003)","DOI":"10.1007\/978-3-642-55631-9"},{"key":"25_CR12","unstructured":"Lay, D.C.: Linear algebra and its applications. Univ. of Maryland-College Park (2003)"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: The Collected Works of J. Richard B\u00fcchi, pp. 425\u2013435. Springer (1990)","DOI":"10.1007\/978-1-4613-8928-6_23"},{"key":"25_CR14","unstructured":"Luenberger, D.G.: Linear and nonlinear programming. Springer (2003)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/3-540-63166-6_34","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1997","unstructured":"Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 340\u2013351. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Knowledge Science, Engineering and Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12096-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,19]],"date-time":"2022-04-19T19:38:43Z","timestamp":1650397123000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12096-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319120959","9783319120966"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12096-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}