{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,17]],"date-time":"2025-04-17T13:47:30Z","timestamp":1744897650040,"version":"3.37.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642116223"},{"type":"electronic","value":"9783642116230"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11623-0_17","type":"book-chapter","created":{"date-parts":[[2010,1,25]],"date-time":"2010-01-25T01:08:29Z","timestamp":1264381709000},"page":"292-307","source":"Crossref","is-referenced-by-count":11,"title":["Bounded Rational Search for On-the-Fly Model Checking of LTL Properties"],"prefix":"10.1007","author":[{"given":"Razieh","family":"Behjati","sequence":"first","affiliation":[]},{"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[]},{"given":"Majid","family":"Nili Ahmadabadi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-74128-2_6","volume-title":"Model Checking and Artificial Intelligence","author":"T. Araragi","year":"2007","unstructured":"Araragi, T., Cho, S.M.: Checking liveness properties of concurrent systems by reinforcement learning. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol.\u00a04428, pp. 84\u201394. Springer, Heidelberg (2007)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/3-540-45793-3_21","volume-title":"Computer Science Logic","author":"D. Beauquier","year":"2002","unstructured":"Beauquier, D., Slissenko, A., Rabinovich, A.: A logic of probability with decidable model-checking. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 306\u2013321. Springer, Heidelberg (2002)"},{"key":"17_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)"},{"issue":"2","key":"17_CR4","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 and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"17_CR5","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., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08, 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1-2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des.\u00a09(1-2), 77\u2013104 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"17_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M., et al.: Formal methods: State of the art and future directions. ACM Computing Surveys\u00a028, 626\u2013643 (1996)","journal-title":"ACM Computing Surveys"},{"key":"17_CR9","first-page":"142","volume-title":"FOCS 1995","author":"P. Dagum","year":"1995","unstructured":"Dagum, P., Karp, R., Luby, M., Ross, S.: An optimal algorithm for monte carlo estimation. In: FOCS 1995, Washington, DC, USA, p. 142. IEEE Computer Society, Los Alamitos (1995)"},{"key":"17_CR10","unstructured":"Darbon, J., Lassaigne, R., Peyro, S.: Approximate probabilistic model checking for programs. In: Second IEEE International Conference on Intelligent Computer Communication and Processing, ICCP 2006 (2006)"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Allen Emerson, E.: Temporal and modal logic, pp. 995\u20131072 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"1-2","key":"17_CR12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E. Allen Emerson","year":"1996","unstructured":"Allen Emerson, E., Prasad Sistla, A.: Symmetry and model checking. Form. Methods Syst. Des.\u00a09(1-2), 105\u2013131 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71209-1_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Etessami","year":"2007","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of markov decision processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 50\u201365. Springer, Heidelberg (2007)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BFb0023731","volume-title":"Computer-Aided Verification","author":"P. Godefroid","year":"1991","unstructured":"Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 176\u2013185. Springer, Heidelberg (1991)"},{"key":"17_CR15","unstructured":"Grosu, R., Smolka, S.A.: Quantitative model checking. In: ISoLA (Preliminary proceedings). Technical Report, vol.\u00a0TR-2004-6, pp. 165\u2013174. Department of Computer Science, University of Cyprus (2004)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Grosu","year":"2005","unstructured":"Grosu, R., Smolka, S.A.: Monte carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 271\u2013286. Springer, Heidelberg (2005)"},{"key":"17_CR17","unstructured":"Haslum, P.: Model checking by random walk. In: ECSEL Workshop (1999)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Jaghoori, M.M., Movaghar, A., Sirjani, M.: Modere: The model-checking engine of Rebeca. In: ACM Symposium on Applied Computing - Software Verificatin Track, pp. 1810\u20131815 (2006)","DOI":"10.1145\/1141277.1141704"},{"issue":"3","key":"17_CR20","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1016\/0196-6774(89)90038-2","volume":"10","author":"R.M. Kapp","year":"1989","unstructured":"Kapp, R.M., Luby, M., Madras, N.: Monte-carlo approximation algorithms for enumeration problems. J. Algorithms\u00a010(3), 429\u2013448 (1989)","journal-title":"J. Algorithms"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol.\u00a04486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"17_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic, Dordrecht (1993)"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs, pp. 1\u201320 (1979)","DOI":"10.1007\/BFb0022460"},{"issue":"4","key":"17_CR24","doi-asserted-by":"crossref","first-page":"385","DOI":"10.3233\/FUN-2004-63405","volume":"63","author":"M. Sirjani","year":"2004","unstructured":"Sirjani, M., Movaghar, A., Shali, A., de Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundamenta Informaticae\u00a063(4), 385\u2013410 (2004)","journal-title":"Fundamenta Informaticae"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","first-page":"232","volume-title":"Computer Aided Verification","author":"A. Prasad Sistla","year":"1997","unstructured":"Prasad Sistla, A., Emerson, E.A.: On-the-fly model checking under fairness that exploits symmetry. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 232\u2013243. Springer, Heidelberg (1997)"},{"key":"17_CR26","series-title":"ENTCS","first-page":"2003","volume-title":"Proc. of Parallel and Distributed Model Checking (PDMC 2003)","author":"H. Sivaraj","year":"2003","unstructured":"Sivaraj, H., Sivaraj, H., Gopalakrishnan, G., Gopalakrishnan, G.: Random walk based heuristic algorithms for distributed memory model checking. In: Proc. of Parallel and Distributed Model Checking (PDMC 2003). ENTCS, vol.\u00a089, p. 2003. Elsevier, Amsterdam (2003)"},{"key":"17_CR27","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press, Cambridge"},{"key":"17_CR28","first-page":"317","volume-title":"Proc. Asia-Pacific Software Engineering Conference (APSEC 2001)","author":"E. Tronci","year":"2001","unstructured":"Tronci, E.: A probabilistic approach to automatic verification of concurrent systems. In: Proc. Asia-Pacific Software Engineering Conference (APSEC 2001), pp. 317\u2013324. IEEE Computer Society, Los Alamitos (2001)"},{"issue":"4","key":"17_CR29","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Form. Methods Syst. Des.\u00a01(4), 297\u2013322 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"17_CR30","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Symp. on Logic in Computer Science, Cambridge, June 1986, pp. 332\u2013344 (1986)"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11623-0_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,16]],"date-time":"2025-02-16T23:18:16Z","timestamp":1739747896000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11623-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642116223","9783642116230"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11623-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}