{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T23:35:34Z","timestamp":1790811334596,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,3,13]]},"DOI":"10.1145\/1066677.1066777","type":"proceedings-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:31:47Z","timestamp":1123057907000},"page":"428-435","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Formal modeling and quantitative analysis of KLAIM-based mobile systems"],"prefix":"10.1145","author":[{"given":"Rocco","family":"De Nicola","sequence":"first","affiliation":[{"name":"Univ. di Firenze Lombroso, Firenze, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Diego","family":"Latella","sequence":"additional","affiliation":[{"name":"C.N.R.-I.S.T.I. -A. Faedo, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mieke","family":"Massink","sequence":"additional","affiliation":[{"name":"C.N.R., I.S.T.I.-A. Faedo, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2005,3,13]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"261","volume-title":"Computer Performance Evaluation","author":"Baier C.","year":"2002","unstructured":"C. Baier , B. Haverkort , H. Hermanns , and J. Katoen . Automated Performance and Dependability Evaluation Using Model Checking . In Computer Performance Evaluation , pages 261 -- 289 . Springer-Verlag , 2002 .]] C. Baier, B. Haverkort, H. Hermanns, and J. Katoen. Automated Performance and Dependability Evaluation Using Model Checking. In Computer Performance Evaluation, pages 261--289. Springer-Verlag, 2002.]]"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"C.\n      Baier J.\n      Katoen and \n      H.\n      Hermanns\n  . \n  Approximate Symbolic Model Checking of Continuous-Time Markov Chains\n  . In J. Baeten and S. Mauw editors Concur'99 volume \n  1664\n   of \n  LNCS pages \n  146\n  --\n  162\n  . \n  Springer-Verlag 1999\n  .]]   C. Baier J. Katoen and H. Hermanns. Approximate Symbolic Model Checking of Continuous-Time Markov Chains. In J. Baeten and S. Mauw editors Concur'99 volume 1664 of LNCS pages 146--162. Springer-Verlag 1999.]]","DOI":"10.1007\/3-540-48320-9_12"},{"key":"e_1_3_2_1_3_1","volume-title":"Formulae meet Programs over the Net: a Framework for Reliable Network Aware Programming","author":"Bettini L.","year":"2003","unstructured":"L. Bettini , R. De Nicola , and M. Loreti . Formulae meet Programs over the Net: a Framework for Reliable Network Aware Programming , 2003 . (submitted for publication. Available at: http: \/\/music. dsi.unif.it).]] L. Bettini, R. De Nicola, and M. Loreti. Formulae meet Programs over the Net: a Framework for Reliable Network Aware Programming, 2003. (submitted for publication. Available at: http: \/\/music. dsi.unif.it).]]"},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/978-3-540-40042-4_4","volume-title":"Global Computing: Programming Environments, Languages, Security and Analysis of Systems","author":"Bettini L.","year":"2003","unstructured":"L. Bettini , V. Non , R. De Nicola , G. Ferrari , D. Gorla , M. Loreti , E. Moggi , R. Pugliese , E. Tuosto , and B. Venneri . The Klaim Project: Theory and Practice . In C. Priami, editor, Global Computing: Programming Environments, Languages, Security and Analysis of Systems , volume 2874 of LNCS , pages 88 -- 150 . Springer-Verlag , 2003 .]] L. Bettini, V. Non, R. De Nicola, G. Ferrari, D. Gorla, M. Loreti, E. Moggi, R. Pugliese, E. Tuosto, and B. Venneri. The Klaim Project: Theory and Practice. In C. Priami, editor, Global Computing: Programming Environments, Languages, Security and Analysis of Systems, volume 2874 of LNCS, pages 88--150. Springer-Verlag, 2003.]]"},{"key":"e_1_3_2_1_5_1","first-page":"99","volume-title":"Proceedings of the 7th workshop on process algebras and performance modeling","author":"Bradley J.","year":"1999","unstructured":"J. Bradley and N. Davies . Reliable Performance Modeling with Approximate Synchronisations. In J. Hillston and M. Silva, editors , Proceedings of the 7th workshop on process algebras and performance modeling , pages 99 -- 118 . Prensas Universitarias de Zaragoza , September 1999 .]] J. Bradley and N. Davies. Reliable Performance Modeling with Approximate Synchronisations. In J. Hillston and M. Silva, editors, Proceedings of the 7th workshop on process algebras and performance modeling, pages 99--118. Prensas Universitarias de Zaragoza, September 1999.]]"},{"key":"e_1_3_2_1_6_1","volume-title":"Model-checking Large Structured Markov Chains. The Journal of Logic and Algebraic Programming","author":"Buchholz P.","year":"2003","unstructured":"P. Buchholz , J.-P Katoen , P. Kemper , and C. Tepper . Model-checking Large Structured Markov Chains. The Journal of Logic and Algebraic Programming . Elsevier , 56(1--2):69--96, 2003 .]] P. Buchholz, J.-P Katoen, P. Kemper, and C. Tepper. Model-checking Large Structured Markov Chains. The Journal of Logic and Algebraic Programming. Elsevier, 56(1--2):69--96, 2003.]]"},{"key":"e_1_3_2_1_7_1","volume-title":"Model Checking","author":"Clarke E.","year":"1999","unstructured":"E. Clarke , O. Grumberg , and D. Peled . Model Checking . MIT Press , 1999 . ISBN 0-262-03270-8.]] E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999. ISBN 0-262-03270-8.]]"},{"key":"e_1_3_2_1_8_1","first-page":"338","volume-title":"Verifying Temporal Properties of Finite State Probabilistic Programs. In 29th Annual Symposium on Foundations of Computer Science","author":"Courcoubetis C.","year":"1988","unstructured":"C. Courcoubetis and M. Yannakakis . Verifying Temporal Properties of Finite State Probabilistic Programs. In 29th Annual Symposium on Foundations of Computer Science , pages 338 -- 345 . IEEE Computer Society Press , 1988 .]] C. Courcoubetis and M. Yannakakis. Verifying Temporal Properties of Finite State Probabilistic Programs. In 29th Annual Symposium on Foundations of Computer Science, pages 338--345. IEEE Computer Society Press, 1988.]]"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.685256"},{"key":"e_1_3_2_1_11_1","series-title":"LNCS","volume-title":"R. De Nicola","author":"Di Pierro A.","year":"2004","unstructured":"A. Di Pierro , C. Hankin , and H. Wiklicky . Probabilistic KLAIM . In R. De Nicola , G. Ferrari, and G. Meredith, editors, Coordination Models and Languages, volume 2949 of LNCS . Springer-Verlag , 2004 .]] A. Di Pierro, C. Hankin, and H. Wiklicky. Probabilistic KLAIM. In R. De Nicola, G. Ferrari, and G. Meredith, editors, Coordination Models and Languages, volume 2949 of LNCS. Springer-Verlag, 2004.]]"},{"key":"e_1_3_2_1_12_1","volume-title":"How Much Expressive Are LOTOS Expressions? In J","author":"Fantechi A.","year":"1991","unstructured":"A. Fantechi , S. Gnesi , and G. Mazzarini . How Much Expressive Are LOTOS Expressions? In J . Quemada, J. Manas, and M. Thomas, editors, Formal Description Techniques --- III. North-Holland Publishing Company , 1991 .]] A. Fantechi, S. Gnesi, and G. Mazzarini. How Much Expressive Are LOTOS Expressions? In J. Quemada, J. Manas, and M. Thomas, editors, Formal Description Techniques --- III. North-Holland Publishing Company, 1991.]]"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2363.2433"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-5316(03)00069-5"},{"key":"e_1_3_2_1_15_1","volume-title":"A Semantic Theory for Global Computing Systems","author":"Gorla D.","year":"2004","unstructured":"D. Gorla and R. Pugliese . A Semantic Theory for Global Computing Systems , 2004 . ( Submitted for publication. Available at http:\/\/www.dsi.uniromal.it\/~gorla\/papers\/bis4k-full.pdf).]] D. Gorla and R. Pugliese. A Semantic Theory for Global Computing Systems, 2004. (Submitted for publication. Available at http:\/\/www.dsi.uniromal.it\/~gorla\/papers\/bis4k-full.pdf).]]"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/800057.808660"},{"key":"e_1_3_2_1_17_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/3-540-44667-2_2","volume-title":"Lectures on Formal Methods and Performance Analysis","author":"Haverkort B.","year":"2001","unstructured":"B. Haverkort . Markovian Models for Performance and Dependability Evaluation . In E. Brinksma, H. Hermanns, and J. Katoen, editors, Lectures on Formal Methods and Performance Analysis , volume 2090 of LNCS , pages 38 -- 83 . Springer-Verlag , 2001 .]] B. Haverkort. Markovian Models for Performance and Dependability Evaluation. In E. Brinksma, H. Hermanns, and J. Katoen, editors, Lectures on Formal Methods and Performance Analysis, volume 2090 of LNCS, pages 38--83. Springer-Verlag, 2001.]]"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"O.\n      Herescu\n     and \n      C.\n      Palamidessi\n  . \n  Probabilistic Asynchronous π-Calculus\n  . In J. Tiuryn editor FoSSaCS \n  2000 volume \n  1784\n   of \n  LNCS pages \n  146\n  --\n  160\n  . \n  Springer-Verlag 2000.]]   O. Herescu and C. Palamidessi. Probabilistic Asynchronous π-Calculus. In J. Tiuryn editor FoSSaCS 2000 volume 1784 of LNCS pages 146--160. Springer-Verlag 2000.]]","DOI":"10.1007\/3-540-46432-8_10"},{"key":"e_1_3_2_1_19_1","series-title":"LNGS pages 420--439","volume-title":"Integrated Formal Methods-IFM","author":"Hermanns H.","year":"2000","unstructured":"H. Hermanns , J. Katoen , J. Meyer-Kayser , and M. Siegle . Towards Model Checking Stochastic Process Algebra . In W. Grieskamp, T. Santen, and B. Stoddart, editors, Integrated Formal Methods-IFM 2000 , volume 1945 of LNGS pages 420--439 . Springer-Verlag , 2000.]] H. Hermanns, J. Katoen, J. Meyer-Kayser, and M. Siegle. Towards Model Checking Stochastic Process Algebra. In W. Grieskamp, T. Santen, and B. Stoddart, editors, Integrated Formal Methods-IFM 2000, volume 1945 of LNGS pages 420--439. Springer-Verlag, 2000.]]"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023985029398"},{"key":"e_1_3_2_1_21_1","volume-title":"Modeling and Analysis of Stochastic Systems","author":"Kulkami V.","year":"1995","unstructured":"V. Kulkami . Modeling and Analysis of Stochastic Systems . Chapman & Hall , 1995 .]] V. Kulkami. Modeling and Analysis of Stochastic Systems. Chapman & Hall, 1995.]]"},{"key":"e_1_3_2_1_22_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Kwiatkowska M.","year":"2002","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach . In J. P. Katoen and P. Stevens, editors, Tools and Algorithms for the Construction and Analysis of Systems , volume 2280 of LNCS , pages 52 -- 66 . Springer-Verlag , 2002 .]] M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In J. P. Katoen and P. Stevens, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 2280 of LNCS, pages 52--66. Springer-Verlag, 2002.]]"},{"key":"e_1_3_2_1_23_1","volume-title":"Stochastic π-Calculus. The Computer Journal","author":"Priami C.","year":"1995","unstructured":"C. Priami . Stochastic π-Calculus. The Computer Journal . Oxford University Press ., 38(7):578--589, 1995 .]] C. Priami. Stochastic π-Calculus. The Computer Journal. Oxford University Press., 38(7):578--589, 1995.]]"},{"key":"e_1_3_2_1_24_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"Younes H.","year":"2002","unstructured":"H. Younes and R. Simmons . Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling . In E. Brinksma and K. Larsen, editors, Computer Aided Verification , volume 2404 of LNCS , pages 223 -- 235 . Springer-Verlag , 2002 .]] H. Younes and R. Simmons. Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling. In E. Brinksma and K. Larsen, editors, Computer Aided Verification, volume 2404 of LNCS, pages 223--235. Springer-Verlag, 2002.]]"}],"event":{"name":"SAC05: The 2005 ACM Symposium on Applied Computing","location":"Santa Fe New Mexico","acronym":"SAC05","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"]},"container-title":["Proceedings of the 2005 ACM symposium on Applied computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1066677.1066777","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T19:22:13Z","timestamp":1673119333000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1066677.1066777"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,3,13]]},"references-count":23,"alternative-id":["10.1145\/1066677.1066777","10.1145\/1066677"],"URL":"https:\/\/doi.org\/10.1145\/1066677.1066777","relation":{},"subject":[],"published":{"date-parts":[[2005,3,13]]},"assertion":[{"value":"2005-03-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}