{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:09:13Z","timestamp":1776373753266,"version":"3.51.2"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319471655","type":"print"},{"value":"9783319471662","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-47166-2_46","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T18:07:34Z","timestamp":1475604454000},"page":"657-673","source":"Crossref","is-referenced-by-count":41,"title":["A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems"],"prefix":"10.1007","author":[{"given":"Vincenzo","family":"Ciancia","sequence":"first","affiliation":[]},{"given":"Diego","family":"Latella","sequence":"additional","affiliation":[]},{"given":"Mieke","family":"Massink","sequence":"additional","affiliation":[]},{"given":"Rytis","family":"Pa\u0161kauskas","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Vandin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"46_CR1","first-page":"213","volume":"153","author":"G Agha","year":"2005","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite- based specification language for probabilistic object systems. ENTCS 153, 213\u2013239 (2005)","journal-title":"ENTCS"},{"key":"46_CR2","volume-title":"Handbook of Spatial Logics","year":"2007","unstructured":"Aiello, M., Pratt-Hartmann, I., van Benthem, J. (eds.): Handbook of Spatial Logics. Springer, Heidelberg (2007)"},{"key":"46_CR3","doi-asserted-by":"crossref","unstructured":"Arora, S., Rathor, A., Rao, M.V.P.: Statistical model checking of opportunistic network protocols. In: Proceedings of the Asian Internet Engineering Conference, pp. 62\u201368. AINTEC 2015. ACM (2015)","DOI":"10.1145\/2837030.2837039"},{"key":"46_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-319-28934-2_5","volume-title":"Formal Aspects of Component Software","author":"M Bartoletti","year":"2016","unstructured":"Bartoletti, M., Cimoli, T., Murgia, M., Podda, A.S., Pompianu, L.: A contract-oriented middleware. In: Braga, C., et al. (eds.) FACS 2015. LNCS, vol. 9539, pp. 86\u2013104. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-28934-2_5"},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Legay, A., Lluch-Lafuente, A., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: 19th International Conference on Software Product Line, pp. 11\u201315. ACM (2015)","DOI":"10.1145\/2791060.2791087"},{"key":"46_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-642-54624-2_10","volume-title":"Specification, Algebra, and Software","author":"L Belzner","year":"2014","unstructured":"Belzner, L., De Nicola, R., Vandin, A., Wirsing, M.: Reasoning (on) service component ensembles in rewriting logic. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 188\u2013211. Springer, Heidelberg (2014)"},{"key":"46_CR7","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/978-1-4020-5587-4_5","volume-title":"Handbook of Spatial Logics","author":"J Benthem van","year":"2007","unstructured":"van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Aiello, M., Pratt-Hartmann, I., Van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 217\u2013298. Springer, Heidelberg (2007)"},{"issue":"4","key":"46_CR8","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1109\/69.404033","volume":"7","author":"AD Bimbo","year":"1995","unstructured":"Bimbo, A.D., Vicario, E., Zingoni, D.: Symbolic description and visual querying of image sequences using spatio-temporal logic. IEEE Trans. Knowl. Data Eng. 7(4), 609\u2013622 (1995)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"46_CR9","volume-title":"Introduction to Stochastic Processes","author":"E \u00c7inlar","year":"1975","unstructured":"\u00c7inlar, E.: Introduction to Stochastic Processes. Prentice-Hall, Upper Saddle River (1975)"},{"key":"46_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-3-662-44602-7_18","volume-title":"Theoretical Computer Science","author":"V Ciancia","year":"2014","unstructured":"Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 222\u2013235. Springer, Heidelberg (2014)"},{"key":"46_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-34096-8_6","volume-title":"Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems","author":"V Ciancia","year":"2016","unstructured":"Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 156\u2013201. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-34096-8_6"},{"key":"46_CR12","doi-asserted-by":"crossref","unstructured":"Ciancia, V., Gilmore, S., Latella, D., Loreti, M., Massink, M.: Data verification for collective adaptive systems: spatial model-checking of vehicle location data. In: IEEE International Conference on Self-Adaptive and Self-Organizing Systems, 2nd FoCAS Workshop (2014)","DOI":"10.1109\/SASOW.2014.16"},{"key":"46_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-662-49224-6_24","volume-title":"Software Engineering and Formal Methods","author":"V Ciancia","year":"2015","unstructured":"Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Bianculli, D., et al. (eds.) SEFM 2015 Workshops. LNCS, vol. 9509, pp. 297\u2013311. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-49224-6_24"},{"key":"46_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-319-39519-7_5","volume-title":"Coordination Models and Languages","author":"V Ciancia","year":"2016","unstructured":"Ciancia, V., Latella, D., Massink, M.: On-the-fly mean-field model-checking for attribute-based coordination. In: Lluch Lafuente, A., Proen\u00e7a, J. (eds.) COORDINATION 2016. LNCS, vol. 9686, pp. 67\u201383. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-39519-7_5"},{"key":"46_CR15","doi-asserted-by":"crossref","unstructured":"Ciancia, V., Latella, D., Massink, M., Pa\u0161kauskas, R.: Exploring spatio-temporal properties of bike-sharing systems. In: SASO Workshops, pp. 74\u201379. IEEE Computer Society (2015)","DOI":"10.1109\/SASOW.2015.17"},{"key":"46_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/978-3-540-69850-0_12","volume-title":"25 Years of Model Checking","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 196\u2013215. Springer, Heidelberg (2008)"},{"issue":"4","key":"46_CR17","doi-asserted-by":"crossref","first-page":"41","DOI":"10.5038\/2375-0901.12.4.3","volume":"12","author":"P Maio","year":"2009","unstructured":"Maio, P.: Bike-sharing: its history, impacts, models of provision, and future. J. Publ. Transp. 12(4), 41\u201356 (2009)","journal-title":"J. Publ. Transp."},{"issue":"1","key":"46_CR18","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1016\/j.tcs.2007.05.008","volume":"382","author":"R Nicola De","year":"2007","unstructured":"De Nicola, R., Katoen, J.P., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theor. Comput. Sci. 382(1), 42\u201370 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"46_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/3-540-48384-5_17","volume-title":"Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science","author":"A Galton","year":"1999","unstructured":"Galton, A.: The mereotopology of discrete space. In: Freksa, C., Mark, D.M. (eds.) COSIT 1999. LNCS, vol. 1661, pp. 251\u2013266. Springer, Heidelberg (1999)"},{"issue":"9","key":"46_CR20","doi-asserted-by":"crossref","first-page":"1876","DOI":"10.1021\/jp993732q","volume":"104","author":"MA Gibson","year":"2000","unstructured":"Gibson, M.A., Bruck, J.: Efficient exact stochastic simulation of chemical systems with many species and many channels. J. Phys. Chem. A 104(9), 1876\u20131889 (2000)","journal-title":"J. Phys. Chem. A"},{"key":"46_CR21","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1146\/annurev.physchem.58.032806.104637","volume":"58","author":"DT Gillespie","year":"2007","unstructured":"Gillespie, D.T.: Stochastic simulation of chemical kinetics. Ann. Rev. Phys. Chem. 58, 35\u201355 (2007)","journal-title":"Ann. Rev. Phys. Chem."},{"key":"46_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/978-3-319-10181-1_5","volume-title":"Integrated Formal Methods","author":"S Gilmore","year":"2014","unstructured":"Gilmore, S., Tribastone, M., Vandin, A.: An analysis pathway for the quantitative evaluation of public transport systems. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 71\u201386. Springer, Heidelberg (2014)"},{"issue":"3","key":"46_CR23","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/1467247.1467271","volume":"52","author":"R Grosu","year":"2009","unstructured":"Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97\u2013105 (2009)","journal-title":"Commun. ACM"},{"key":"46_CR24","doi-asserted-by":"crossref","unstructured":"Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Gros, R., Belta, C.: Spatel: A novel spatial-temporal logic and its applications to networked systems. In: 18th International Conference on Hybrid Systems: Computation and Control, pp. 189\u2013198. ACM (2015)","DOI":"10.1145\/2728606.2728633"},{"key":"46_CR25","unstructured":"Hauskrecht, M.: Monte-Carlo approximations to continuous-time semi-Markov processes. Technical report CS-03-02, University of Pittsburgh (2002)"},{"key":"46_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1007\/978-3-642-39799-8_38","volume-title":"Computer Aided Verification","author":"C Jegourel","year":"2013","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576\u2013591. Springer, Heidelberg (2013)"},{"key":"46_CR27","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/978-1-4020-5587-4_9","volume-title":"Handbook of Spatial Logics","author":"R Kontchakov","year":"2007","unstructured":"Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: Spatial logic + temporal logic = ? In: Aiello, M., Pratt-Hartmann, I., Van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 497\u2013564. Springer, Heidelberg (2007)"},{"key":"46_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-662-45231-8_10","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"KG Larsen","year":"2014","unstructured":"Larsen, K.G., Legay, A.: Statistical model checking past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 135\u2013142. Springer, Heidelberg (2014)"},{"key":"46_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010)"},{"key":"46_CR30","doi-asserted-by":"crossref","unstructured":"Massink, M., Pa\u0161kauskas, R.: Model-based assessment of aspects of user-satisfaction in bicycle sharing systems. In: 18th International Conference on Intelligent Transportation Systems, pp. 1363\u20131370. IEEE (2015)","DOI":"10.1109\/ITSC.2015.224"},{"key":"46_CR31","unstructured":"Midgley, P.: Bicycle-sharing schemes: enhancing sustainable mobility in urban areas. In: 19th session of the Commission on Sustainable Development. CSD19\/2011\/BP8, United Nations (2011)"},{"key":"46_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-23820-3_2","volume-title":"Runtime Verification","author":"L Nenzi","year":"2015","unstructured":"Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 21\u201337. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-23820-3_2"},{"key":"46_CR33","doi-asserted-by":"crossref","unstructured":"Pianini, D., Sebastio, S., Vandin, A.: Distributed statistical analysis of complex systems modeled through a chemical metaphor. In: International Conference on High Performance Computing & Simulation, pp. 416\u2013423. IEEE (2014)","DOI":"10.1109\/HPCSim.2014.6903715"},{"key":"46_CR34","doi-asserted-by":"crossref","unstructured":"Sebastio, S., Amoretti, M., Lluch Lafuente, A.: A computational field framework for collaborative task execution in volunteer clouds. In: ICSE workshop SEAMS, pp. 105\u2013114. ACM (2014)","DOI":"10.1145\/2593929.2593943"},{"key":"46_CR35","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: ValueTools, pp. 310\u2013315. ACM (2013)"},{"key":"46_CR36","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316481","volume-title":"Approximation Theorems of Mathematical Statistics, Probability and Statistics","author":"RJ Serfling","year":"1980","unstructured":"Serfling, R.J.: Approximation Theorems of Mathematical Statistics, Probability and Statistics, vol. 162. Wiley, Hoboken (1980)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47166-2_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:22:07Z","timestamp":1498335727000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47166-2_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471655","9783319471662"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47166-2_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}