{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T05:42:45Z","timestamp":1781588565460,"version":"3.54.5"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,1,24]],"date-time":"2018-01-24T00:00:00Z","timestamp":1516752000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10009-018-0483-8","type":"journal-article","created":{"date-parts":[[2018,1,24]],"date-time":"2018-01-24T14:48:22Z","timestamp":1516805302000},"page":"289-311","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":49,"title":["Spatio-temporal model checking of vehicular movement in public transport systems"],"prefix":"10.1007","volume":"20","author":[{"given":"Vincenzo","family":"Ciancia","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephen","family":"Gilmore","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gianluca","family":"Grilletti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Diego","family":"Latella","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mieke","family":"Massink","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,1,24]]},"reference":[{"key":"483_CR1","unstructured":"Aiello, M.: Spatial reasoning: theory and practice. Ph.D. thesis, ILLC, University of Amsterdam (2002)"},{"key":"483_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"483_CR3","first-page":"1","volume":"PP","author":"E Bartocci","year":"2016","unstructured":"Bartocci, E., Gol, E.A., Haghighi, I., Belta, C.: A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Trans. Control Netw. Syst. PP, 1\u201312 (2016)","journal-title":"IEEE Trans. Control Netw. Syst."},{"key":"483_CR4","doi-asserted-by":"crossref","unstructured":"Belmonte, G., Ciancia, V., Latella, D., Massink, M.: From collective adaptive systems to human centric computation and back: spatial model checking for medical imaging. In: Proceedings of the Workshop on FORmal Methods for the Quantitative Evaluation of Collective Adaptive SysTems, FORECAST@STAF 2016, Vienna, Austria, 8 July 2016, volume 217 of EPTCS, pp. 81\u201392 (2016)","DOI":"10.4204\/EPTCS.217.10"},{"issue":"3","key":"483_CR5","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M Ben-Ari","year":"1983","unstructured":"Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Inform. 20(3), 207\u2013226 (1983)","journal-title":"Acta Inform."},{"key":"483_CR6","unstructured":"Bortolussi, L., Nenzi, L.: Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In: VALUETOOLS (2014)"},{"issue":"3","key":"483_CR7","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1006\/jcss.2000.1734","volume":"62","author":"F Buccafurri","year":"2001","unstructured":"Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: On ACTL formulas having linear counterexamples. J. Comput. Syst. Sci. 62(3), 463\u2013515 (2001)","journal-title":"J. Comput. Syst. Sci."},{"key":"483_CR8","doi-asserted-by":"crossref","unstructured":"Caires, L.: Behavioral and spatial observations in a logic for the $$\\pi $$ \u03c0 -calculus. In: Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures (FOSSACS\u201904), volume 2987 of LNCS, pp. 72\u201387. Springer (2004)","DOI":"10.1007\/978-3-540-24727-2_7"},{"issue":"0","key":"483_CR9","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1016\/j.tcs.2011.12.051","volume":"431","author":"L Cardelli","year":"2012","unstructured":"Cardelli, L., Gardner, P.: Processes in space. Theor. Comput. Sci. 431(0), 40\u201355 (2012). Modelling and Analysis of Biological Systems Based on papers presented at the Workshop on Membrane Computing and Bio-logically Inspired Process Calculi (MeCBIC) held in 2008 (Iasi), 2009 (Bologna) and 2010 (Jena)","journal-title":"Theor. Comput. Sci."},{"key":"483_CR10","doi-asserted-by":"crossref","unstructured":"Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: Proceedings of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201900), pp. 365\u2013377 (2000)","DOI":"10.1145\/325694.325742"},{"key":"483_CR11","doi-asserted-by":"crossref","unstructured":"Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Software Engineering and Formal Methods\u2014SEFM 2015 Collocated Workshops, volume 9509 of Lecture Notes in Computer Science, pp. 297\u2013311. Springer (2015)","DOI":"10.1007\/978-3-662-49224-6_24"},{"key":"483_CR12","doi-asserted-by":"crossref","unstructured":"Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Springer (ed.) The 8th IFIP International Conference on Theoretical Computer Science, TCS 2014, Track B, volume 8705 of Lecture Notes in Computer Science, pp. 222\u2013235 (2014)","DOI":"10.1007\/978-3-662-44602-7_18"},{"key":"483_CR13","unstructured":"Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model checking spatial logics for closure spaces. Log. Methods Comput. Sci. 12(4), 1\u201351 (2016)"},{"key":"483_CR14","doi-asserted-by":"crossref","unstructured":"Ciancia, V., Latella, D., Massink, M., Paskauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques\u20147th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, 10\u201314 October 2016, Proceedings, Part I, volume 9952 of Lecture Notes in Computer Science, pp. 657\u2013673 (2016)","DOI":"10.1007\/978-3-319-47166-2_46"},{"key":"483_CR15","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Logic of Programs, volume 131 of Lecture Notes in Computer Science, pp. 53\u201371. Springer (1986)"},{"key":"483_CR16","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-540-39910-0_9","volume-title":"Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, volume 2772 of Lecture Notes in Computer Science","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Veith, H.: Counterexamples revisited: principles, algorithms, applications. In: Dershowitz, N. (ed.) Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, volume 2772 of Lecture Notes in Computer Science, pp. 208\u2013224. Springer, Berlin (2003)"},{"issue":"10","key":"483_CR17","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1016\/j.trb.2009.04.002","volume":"43","author":"CF Daganzo","year":"2009","unstructured":"Daganzo, C.F.: A headway-based approach to eliminate bus bunching: systematic analysis and comparisons. Transp. Res. Part B Methodol. 43(10), 913\u2013921 (2009)","journal-title":"Transp. Res. Part B Methodol."},{"issue":"1","key":"483_CR18","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/j.trb.2010.06.005","volume":"45","author":"CF Daganzo","year":"2011","unstructured":"Daganzo, C.F., Pilachowski, J.: Reducing bunching with bus-to-bus cooperation. Transp. Res. Part B Methodol. 45(1), 267\u2013277 (2011)","journal-title":"Transp. Res. Part B Methodol."},{"key":"483_CR19","doi-asserted-by":"crossref","unstructured":"De Angelis, F.L., Di Marzo Serugendo, G.: Towards a spatial language for run-time assessments in self-organizing systems. In: 2015 IEEE 9th International Conference on Self-Adaptive and Self-Organizing Systems, Cambridge, MA, USA, 21\u201325 September 2015, pp. 174\u2013175. IEEE Computer Society (2015)","DOI":"10.1109\/SASO.2015.32"},{"issue":"1","key":"483_CR20","doi-asserted-by":"publisher","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."},{"issue":"4","key":"483_CR21","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1109\/69.404033","volume":"7","author":"A Bimbo Del","year":"1995","unstructured":"Del Bimbo, A., 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."},{"issue":"4","key":"483_CR22","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1017\/S0269888916000199","volume":"31","author":"SA Dobson","year":"2016","unstructured":"Dobson, S.A., Viroli, M., Fernandez-Marquez, J.L., Zambonelli, F., Stevenson, G., Di\u00a0Marzo Serugendo, G., Montagna, S., Pianini, D., Ye, J., Castelli, G., Rosi, A.: Spatial awareness in pervasive ecosystems. Knowl. Eng. Rev. 31(4), 343\u2013366 (2016)","journal-title":"Knowl. Eng. Rev."},{"key":"483_CR23","first-page":"995","volume-title":"Handbook of Theoretical Computer Science (Vol. B)","author":"EA Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science (Vol. B), pp. 995\u20131072. MIT Press, Cambridge (1990)"},{"key":"483_CR24","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-642-15300-6_5","volume-title":"Geographic Information Science, Lecture Notes in Computer Science","author":"A Fathi","year":"2010","unstructured":"Fathi, A., Krumm, J.: Detecting road intersections from GPS traces. In: Fabrikant, S.I., Reichenbacher, T., van Kreveld, M., Schlieder, C. (eds.) Geographic Information Science, Lecture Notes in Computer Science, vol. 6292, pp. 56\u201369. Springer, Berlin (2010)"},{"key":"483_CR25","doi-asserted-by":"crossref","unstructured":"Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: 53rd IEEE Conference on Decision and Control, pp. 108\u2013113 (2014)","DOI":"10.1109\/CDC.2014.7039367"},{"key":"483_CR26","unstructured":"Grilletti, G.: Spatio-temporal model checking: Explicit and abstraction-based methods. Master\u2019s thesis, Dipartimento di Matematica, Universit\u00e0 di Pisa (2016)"},{"issue":"3","key":"483_CR27","doi-asserted-by":"publisher","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":"483_CR28","doi-asserted-by":"crossref","unstructured":"John III, J.B., Clark, R.J., Williamson, D.W., Eisenstein, D.D., Platzman, L.K.: Building a self-organizing urban bus route. In: Sixth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW 2012, Lyon, France, 10\u201314 September 2012, pp. 66\u201370. IEEE Computer Society (2012)","DOI":"10.1109\/SASOW.2012.20"},{"issue":"4","key":"483_CR29","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1016\/j.trb.2011.11.001","volume":"46","author":"JB John III","year":"2012","unstructured":"John III, J.B., Eisenstein, D.D.: A self-coordinating bus route to resist bus bunching. Transp. Res. Part B Methodol. 46(4), 481\u2013491 (2012)","journal-title":"Transp. Res. Part B Methodol."},{"issue":"3","key":"483_CR30","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/j.entcs.2007.12.010","volume":"194","author":"M John","year":"2008","unstructured":"John, M., Ewald, R., Uhrmacher, A.M.: A spatial extension to the pi calculus. Electron. Notes Theor. Comput. Sci. 194(3), 133\u2013148 (2008). Proceedings of the First Workshop From Biology To Concurrency and back (FBTC 2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"483_CR31","doi-asserted-by":"publisher","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, Berlin (2007)"},{"key":"483_CR32","unstructured":"Letchner, J., Krumm, J., Horvitz, E.: Trip router with individualized preferences (TRIP): incorporating personalization into route planning. In: Proceedings of the 18th Conference on Innovative Applications of Artificial Intelligence\u2014volume 2, IAAI\u201906, pp. 1795\u20131800. AAAI Press (2006)"},{"key":"483_CR33","doi-asserted-by":"crossref","unstructured":"Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Runtime Verification\u20146th International Conference, RV 2015 Vienna, Austria, 22\u201325 September 2015. Proceedings, volume 9333 of Lecture Notes in Computer Science, pp. 21\u201337. Springer (2015)","DOI":"10.1007\/978-3-319-23820-3_2"},{"key":"483_CR34","unstructured":"Newell, G.F., Potts, R.B.: Maintaining a bus schedule. In: Proceedings of 2nd Australian Road Research Board, volume 2, pp. 388\u2013393 (1964)"},{"issue":"4","key":"483_CR35","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1061\/(ASCE)SU.1943-5428.0000056","volume":"137","author":"C Ordo\u00f1ez","year":"2011","unstructured":"Ordo\u00f1ez, C., Mart\u00ednez, J., Rodr\u00edguez-P\u00e9rez, J., Reyes, A.: Detection of outliers in GPS measurements by using functional-data analysis. J. Surv. Eng. 137(4), 150\u2013155 (2011)","journal-title":"J. Surv. Eng."},{"key":"483_CR36","doi-asserted-by":"crossref","unstructured":"Reijsbergen, D., Gilmore, S.: Formal punctuality analysis of frequent bus services using headway data. In: Horv\u00e1th, A., Wolter, K. (eds.) Computer Performance Engineering\u201411th European Workshop, EPEW 2014, Florence, Italy, 11\u201312 September 2014. Proceedings, volume 8721 of Lecture Notes in Computer Science, pp. 164\u2013178. Springer (2014)","DOI":"10.1007\/978-3-319-10885-8_12"},{"key":"483_CR37","unstructured":"Ruan, Mi., Lin, J.: An investigation of bus headway regularity and service performance in Chicago bus transit system. In: Transport Chicago, Annual Conference, vol. 14 (2009)"},{"key":"483_CR38","unstructured":"Strathman, J.G., Kimpel, T.J., Callas, S.: Headway deviation effects on bus passenger loads: analysis of Tri-Met\u2019s archived AVL-APC data. Technical Report PR126, Portland State University, Centre for Urban Studies, Oregon (2003)"},{"key":"483_CR39","doi-asserted-by":"crossref","unstructured":"Tsigkanos, C., Kehrer, T., Ghezzi, C.: Modeling and verification of evolving cyber-physical spaces. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2017, Paderborn, Germany, 4\u20138 September 2017, pp. 38\u201348. ACM (2017)","DOI":"10.1145\/3106237.3106299"},{"key":"483_CR40","doi-asserted-by":"crossref","unstructured":"Tsigkanos, C., Pasquale, L., Ghezzi, C., Nuseibeh, B.: Ariadne: topology aware adaptive security for cyber-physical systems. In: 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering, volume 2, pp. 729\u2013732 (2015)","DOI":"10.1109\/ICSE.2015.234"},{"key":"483_CR41","doi-asserted-by":"publisher","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, Berlin (2007)"},{"issue":"1","key":"483_CR42","doi-asserted-by":"publisher","first-page":"1831","DOI":"10.1016\/j.trb.2011.07.009","volume":"45","author":"Y Xuan","year":"2011","unstructured":"Xuan, Y., Argote, J., Daganzo, C.F.: Dynamic bus holding strategies for schedule reliability: optimal linear control and performance analysis. Transp. Res. Part B Methodol. 45(1), 1831\u20131845 (2011)","journal-title":"Transp. Res. Part B Methodol."},{"key":"483_CR43","doi-asserted-by":"crossref","unstructured":"Yan, Z.: Traj-ARIMA: a spatial-time series model for network-constrained trajectory. In: Proceedings of the Second International Workshop on Computational Transportation Science, IWCTS \u201910, pp. 11\u201316. ACM, New York (2010)","DOI":"10.1145\/1899441.1899446"},{"issue":"4","key":"483_CR44","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1287\/trsc.1060.0170","volume":"40","author":"J Zhao","year":"2006","unstructured":"Zhao, J., Dessouky, M., Bukkapatnam, S.: Optimal slack time for schedule-based transit operations. Transp. Sci. 40(4), 529\u2013539 (2006)","journal-title":"Transp. Sci."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-018-0483-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0483-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0483-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,30]],"date-time":"2025-06-30T00:19:09Z","timestamp":1751242749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-018-0483-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,24]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["483"],"URL":"https:\/\/doi.org\/10.1007\/s10009-018-0483-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,24]]},"assertion":[{"value":"24 January 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}