{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:29:22Z","timestamp":1761596962726},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540341451"},{"type":"electronic","value":"9783540341468"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11752707_4","type":"book-chapter","created":{"date-parts":[[2006,5,25]],"date-time":"2006-05-25T09:50:15Z","timestamp":1148550615000},"page":"39-50","source":"Crossref","is-referenced-by-count":5,"title":["Towards Model Checking Stochastic Aspects of the thinkteam User Interface"],"prefix":"10.1007","author":[{"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[]},{"given":"Mieke","family":"Massink","sequence":"additional","affiliation":[]},{"given":"Diego","family":"Latella","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. Formal Methods in System Design\u00a015, 7\u201348 (1999)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"4_CR2","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking continuous time Markov chains. ACM Transactions on Computational Logic\u00a01(1), 162\u2013170 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuoustime Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 146\u2013162. Springer, Heidelberg (1999)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-45798-4_12","volume-title":"Performance Evaluation of Complex Systems: Techniques and Tools","author":"C. Baier","year":"2002","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Automated performance and dependability evaluation using model checking. In: Calzarossa, M.C., Tucci, S. (eds.) Performance 2002. LNCS, vol.\u00a02459, pp. 261\u2013289. Springer, Heidelberg (2002)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Massink, M., Latella, D.: Towards Model Checking Stochastic Aspects of the thinkteam User Interface\u2014FULL VERSION. Technical Report 2005-TR-18, CNR\/ISTI (2005), http:\/\/fmt.isti.cnr.it\/WEBPAPER\/TRdsvis.pdf","DOI":"10.1007\/11752707_4"},{"key":"4_CR6","first-page":"179","volume-title":"Cooperative Systems Design","author":"M.H. Beek ter","year":"2004","unstructured":"ter Beek, M.H., Massink, M., Latella, D., Gnesi, S.: Model checking groupware protocols. In: Cooperative Systems Design, pp. 179\u2013194. IOS Press, Amsterdam (2004)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Massink, M., Latella, D., Gnesi, S., Forghieri, A., Sebastianis, M.: Model checking publish\/subscribe notification for thinkteam, Technical Report 2004-TR-20, CNR\/ISTI (2004), http:\/\/fmt.isti.cnr.it\/WEBPAPER\/TRTT.ps","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Massink, M., Latella, D., Gnesi, S., Forghieri, A., Sebastianis, M.: Model checking publish\/subscribe notification for thinkteam. In: Proc. FMICS 2004. ENTCS, vol.\u00a0133, pp. 275\u2013294 (2005)","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Lectures on Formal Methods and Performance Analysis","year":"2001","unstructured":"Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.): Lectures on Formal Methods and Performance Analysis. LNCS, vol.\u00a02090. Springer, Heidelberg (2001)"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S1567-8326(02)00067-X","volume":"56","author":"P. Buchholz","year":"2003","unstructured":"Buchholz, P., Katoen, J.-P., Kemper, P., Tepper, C.: Model-checking large structured Markov chains. Journal of Logic and Algebraic Programming\u00a056, 69\u201396 (2003)","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"2","key":"4_CR11","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1145\/376929.376941","volume":"8","author":"P. Cairns","year":"2001","unstructured":"Cairns, P., Jones, M., Thimbleby, H.: Reusable usability analysis with Markov models. ACM Transactions on Computer Human Interaction\u00a08(2), 99\u2013132 (2001)","journal-title":"ACM Transactions on Computer Human Interaction"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., Sistla, A.: 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"},{"key":"4_CR13","volume-title":"Model Checking","author":"E.M. Clarke Jr.","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/3-540-45522-1_9","volume-title":"Interactive Systems: Design, Specification, and Verification","author":"G. Doherty","year":"2001","unstructured":"Doherty, G., Massink, M., Faconti, G.P.: Reasoning about interactive systems with stochastic models. In: Johnson, C. (ed.) DSV-IS 2001. LNCS, vol.\u00a02220, pp. 144\u2013163. Springer, Heidelberg (2001)"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/143457.143468","volume-title":"Proc. CSCW 1992","author":"P. Dourish","year":"1992","unstructured":"Dourish, P., Bellotti, V.: Awareness and coordination in shared workspaces. In: Proc. CSCW 1992, pp. 107\u2013114. ACM Press, New York (1992)"},{"issue":"1","key":"4_CR16","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/99977.99987","volume":"34","author":"C.A. Ellis","year":"1991","unstructured":"Ellis, C.A., Gibbs, S.J., Rein, G.L.: Groupware\u2014Some issues and experiences. Communications of the ACM\u00a034(1), 38\u201358 (1991)","journal-title":"Communications of the ACM"},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF01158472","volume":"7","author":"G.I. Falin","year":"1990","unstructured":"Falin, G.I.: A survey of retrial queues. Queueing Systems\u00a07, 127\u2013168 (1990)","journal-title":"Queueing Systems"},{"key":"4_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4899-2977-8","volume-title":"Retrial Queues","author":"G.I. Falin","year":"1997","unstructured":"Falin, G.I., Templeton, J.G.C.: Retrial Queues. Chapman and Hall, Boca Raton (1997)"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Haverkort, B.: Markovianmodels for performance and dependability evaluation. In: [9], pp. 38\u201383","DOI":"10.1007\/3-540-44667-2_2"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s100090100072","volume":"4","author":"H. Hermanns","year":"2003","unstructured":"Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A tool for model-checking Markov chains. Int. Journal on Software Tools for Technology Transfer\u00a04, 153\u2013172 (2003)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. CU Press, Cambridge (1996)","DOI":"10.1017\/CBO9780511569951"},{"key":"4_CR22","volume-title":"The SPIN Model Checker","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)"},{"key":"4_CR23","volume-title":"Modeling and Analysis of Stochastic Systems","author":"V. Kulkarni","year":"1995","unstructured":"Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman and Hall, Boca Raton (1995)"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 52\u201366. Springer, Heidelberg (2002)"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-36235-5_16","volume-title":"Interactive Systems. Design, Specification, and Verification","author":"X. Lacaze","year":"2002","unstructured":"Lacaze, X., Palanque, P., Navarre, D., Bastide, R.: Performance Evaluation as a Tool for Quantitative Assessment of Complexity of Interactive Systems. In: Forbrig, P., Limbourg, Q., Urban, B., Vanderdonckt, J. (eds.) DSV-IS 2002. LNCS, vol.\u00a02545, pp. 208\u2013222. Springer, Heidelberg (2002)"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1093\/comjnl\/45.4.453","volume":"45","author":"C. Papadopoulos","year":"2002","unstructured":"Papadopoulos, C.: An extended temporal logic for CSCW. Comp. Journal\u00a045, 453\u2013472 (2002)","journal-title":"Comp. Journal"},{"key":"4_CR27","unstructured":"Urnes, T.: Efficiently Implementing Synchronous Groupware. Ph.D. thesis, Department of Computer Science, York University, Toronto (1998)"}],"container-title":["Lecture Notes in Computer Science","Interactive Systems. Design, Specification, and Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11752707_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,18]],"date-time":"2019-04-18T20:39:49Z","timestamp":1555619989000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11752707_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540341451","9783540341468"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11752707_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}