{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:29:57Z","timestamp":1743038997700,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540344544"},{"type":"electronic","value":"9783540344551"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11759744_3","type":"book-chapter","created":{"date-parts":[[2006,6,2]],"date-time":"2006-06-02T08:27:50Z","timestamp":1149236870000},"page":"32-46","source":"Crossref","is-referenced-by-count":20,"title":["Play to Test"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Blass","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuri","family":"Gurevich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lev","family":"Nachmanson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Spec Explorer. (released January 2005), URL: http:\/\/research.microsoft.com\/specexplorer"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Yannakakis, M.: Distinguishing tests for nondeterministic and probabilistic machines. In: Proc. 27th Ann. ACM Symp. Theory of Computing, pp. 363\u2013372 (1995)","DOI":"10.1145\/225058.225161"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR \u201998 Concurrency Theory","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 163\u2013178. Springer, Heidelberg (1998)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-36498-6_5","volume-title":"Abstract State Machines 2003. Advances in Theory and Practice","author":"C. Artho","year":"2003","unstructured":"Artho, C., Drusinsky, D., Goldberg, A., Havelund, K., Lowry, M., Pasareanu, C., Rosu, G., Visser, W.: Experiments with test case generation and runtime analysis. In: B\u00f6rger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol.\u00a02589, pp. 87\u2013107. Springer, Heidelberg (2003)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-540-24617-6_18","volume-title":"Formal Approaches to Software Testing","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., Veanes, M.: Towards a tool environment for model-based testing with AsmL. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol.\u00a02931, pp. 264\u2013280. Springer, Heidelberg (2004)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, R., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"3_CR7","unstructured":"Blass, A., Gurevich, Y., Nachmanson, L., Veanes, M.: Play to test. Technical Report MSR-TR-2005-04, Microsoft Research (January 2005) (Revised April 5, 2005)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Campbell, C., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., Veanes, M.: Model-based testing of object-oriented reactive systems with Spec Explorer. Technical Report MSR-TR-2005-59, Microsoft Research (2005)","DOI":"10.1007\/11526841_38"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-45220-1_11","volume-title":"Computer Science Logic","author":"K. Chatterjee","year":"2003","unstructured":"Chatterjee, K., Jurdzi\u0144ski, M., Henzinger, T.: Simple stochastic parity games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol.\u00a02803, pp. 100\u2013113. Springer, Heidelberg (2003)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"CONCUR\u201999. Concurrency Theory","author":"L. Alfaro de","year":"1999","unstructured":"de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 66\u201381. Springer, Heidelberg (1999)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-39910-0_12","volume-title":"Verification: Theory and Practice","author":"L. Alfaro de","year":"2004","unstructured":"de Alfaro, L.: Game models for open systems. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 269\u2013289. Springer, Heidelberg (2004)"},{"key":"3_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4054-9","volume-title":"Competitive Markov decision processes","author":"J. Filar","year":"1996","unstructured":"Filar, J., Vrieze, K.: Competitive Markov decision processes. Springer, New York (1996)"},{"key":"3_CR13","series-title":"Software Engineering Notes","first-page":"112","volume-title":"ISSTA 2002","author":"W. Grieskamp","year":"2002","unstructured":"Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. In: ISSTA 2002. Software Engineering Notes, vol.\u00a027, pp. 112\u2013122. ACM, New York (2002)"},{"key":"3_CR14","unstructured":"Gujiwara, S., Bochman, G.V.: Testing non-deterministic state machines with fault-coverage. In: Kroon, J., Heijunk, R., Brinksma, E. (eds.) Protocol Test Systems, pp. 363\u2013372 (1992)"},{"key":"3_CR15","first-page":"9","volume-title":"Specification and Validation Methods","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: B\u00f6rger, E. (ed.) Specification and Validation Methods, pp. 9\u201336. Oxford University Press, Oxford (1995)"},{"key":"3_CR16","unstructured":"Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of AsmL. In: Theoretical Computer Science (2005), special issue dedicated to FMCO 2003, preliminary version available as Microsoft Research Technical Report MSR-TR-2004-27 (to appear)"},{"key":"3_CR17","unstructured":"Hartman, A., Nagin, K.: Model driven testing - AGEDIS architecture interfaces and tools. In: 1st European Conference on Model Driven Software Engineering, Nuremberg, Germany, pp. 1\u201311 (December 2003)"},{"key":"3_CR18","unstructured":"Jard, C., J\u00e9ron, T.: TGV: theory, principles and algorithms. In: The Sixth World Conference on Integrated Design and Process Technology, IDPT 2002, Pasadena, California (June 2002)"},{"key":"3_CR19","unstructured":"Kuliamin, V.V., Petrenko, A.K., Kossatchev, A.S., Bourdonov, I.B.: UniTesK: Model based testing in industrial practice. In: 1st European Conference on Model Driven Software Engineering, Nuremberg, Germany, pp. 55\u201363 (December 2003)"},{"key":"3_CR20","series-title":"Software Engineering Notes","first-page":"55","volume-title":"ISSTA 2004","author":"L. Nachmanson","year":"2004","unstructured":"Nachmanson, L., Veanes, M., Schulte, W., Tillmann, N., Grieskamp, W.: Optimal strategies for testing nondeterministic systems. In: ISSTA 2004. Software Engineering Notes, vol.\u00a029, pp. 55\u201364. ACM, New York (2004)"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-0-387-35062-2_10","volume-title":"IFIP TC6 9th International Workshop on Testing of Communicating Systems","author":"A. Petrenko","year":"1996","unstructured":"Petrenko, A., Yevtushenko, N., Bochmann, G.v.: Testing deterministic implementations from nondeterministic FSM specifications. In: Baumgarten, B., Burkhardt, H.-J., Giessler, A. (eds.) IFIP TC6 9th International Workshop on Testing of Communicating Systems, pp. 125\u2013140. Chapman & Hall, Boca Raton (1996)"},{"key":"3_CR22","series-title":"Wiley Series in Probability and Mathematical Statistics","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M.L. Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Mathematical Statistics. A Wiley-Interscience, New York (1994)"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Tasiran, S., Qadeer, S.: Runtime refinement checking of concurrent data structures. Electronic Notes in Theoretical Computer Science\u00a0113, 163\u2013179 (January 2005), Proceedings of the Fourth Workshop on Runtime Verification (RV 2004)","DOI":"10.1016\/j.entcs.2004.01.028"},{"key":"3_CR24","unstructured":"Tretmans, J., Brinksma, E.: TorX: Automated model based testing. In: 1st European Conference on Model Driven Software Engineering, Nuremberg, Germany, pp. 31\u201343 (December 2003)"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: ESEC\/FSE 2005 (2005)","DOI":"10.1145\/1081706.1081751"},{"key":"3_CR26","volume-title":"Theory of Games and Economic Behavior","author":"J. Neumann von","year":"1944","unstructured":"von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior. Princeton University Press, Princeton (1944)"},{"key":"3_CR27","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1109\/LICS.2004.1319602","volume-title":"Proceedings of the Nineteenth Annual IEEE Symposium on Logic In Computer Science, LICS 2004","author":"M. Yannakakis","year":"2004","unstructured":"Yannakakis, M.: Testing, optimization, and games. In: Proceedings of the Nineteenth Annual IEEE Symposium on Logic In Computer Science, LICS 2004, pp. 78\u201388. IEEE, Los Alamitos (2004)"},{"key":"3_CR28","first-page":"347","volume-title":"Testing and Verification XII","author":"W. Yi","year":"1992","unstructured":"Yi, W., Larsen, K.G.: Testing probabilistic and nondeterministic processes. In: Testing and Verification XII, pp. 347\u2013361. North Holland, Amsterdam (1992)"}],"container-title":["Lecture Notes in Computer Science","Formal Approaches to Software Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11759744_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T00:28:01Z","timestamp":1555633681000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11759744_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540344544","9783540344551"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/11759744_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}