{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:22:55Z","timestamp":1742962975095,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757778"},{"type":"electronic","value":"9783031757785"}],"license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75778-5_14","type":"book-chapter","created":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T12:08:59Z","timestamp":1731845339000},"page":"297-308","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Measured Causes: Adding Time and Probability to True Concurrency"],"prefix":"10.1007","author":[{"given":"Ed","family":"Brinksma","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1955-5183","authenticated-orcid":false,"given":"Rom","family":"Langerak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3257-9059","authenticated-orcid":false,"given":"Diego","family":"Latella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5089-002X","authenticated-orcid":false,"given":"Mieke","family":"Massink","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"key":"14_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/BFb0055085","volume-title":"ICALP 1998","author":"C Baier","year":"1998","unstructured":"Baier, C., Katoen, J.P., Latella, D.: Metric semantics for true concurrent real time. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 568\u2013579. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055085"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Belmonte, G., Broccia, G., Ciancia, V., Latella, D., Massink, M.: Feasibility of spatial model checking for nevus segmentation. In: Bliudze, S., Gnesi, S., Plat, N., Semini, L. (eds.) 9th IEEE\/ACM International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2021, Madrid, Spain, 17\u201321 May 2021, pp. 1\u201312. IEEE (2021). https:\/\/doi.org\/10.1109\/FormaliSE52586.2021.00007","DOI":"10.1109\/FormaliSE52586.2021.00007"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-030-17462-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Belmonte","year":"2019","unstructured":"Belmonte, G., Ciancia, V., Latella, D., Massink, M.: VoxLogicA: a spatial model checker for declarative image analysis. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 281\u2013298. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_16"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Bezhanishvili, N., Ciancia, V., Gabelaia, D., Grilletti, G., Latella, D., Massink, M.: Geometric model checking of continuous space. Log. Methods Comput. Sci. 18(4) (2022). https:\/\/doi.org\/10.46298\/lmcs-18(4:7)2022","DOI":"10.46298\/lmcs-18(4:7)2022"},{"key":"14_CR5","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. 14, 25\u201359 (1987). https:\/\/doi.org\/10.1016\/0169-7552(87)90085-7","journal-title":"Comput. Netw."},{"key":"14_CR6","series-title":"Workshops in Computing","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-1-4471-3229-5_15","volume-title":"Semantics of Specification Languages (SoSL)","author":"B Botma","year":"1994","unstructured":"Botma, B.: Rendez- Vous with bundle event structures. In: Andrews, D.J., Groote, J.F., Middelburg, C.A. (eds.) Semantics of Specification Languages (SoSL). WC, pp. 270\u2013288. Springer, London (1994). https:\/\/doi.org\/10.1007\/978-1-4471-3229-5_15"},{"issue":"7","key":"14_CR7","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1093\/comjnl\/38.7.552","volume":"38","author":"E Brinksma","year":"1995","unstructured":"Brinksma, E., Katoen, J.P., Langerak, R., Latella, D.: A stochastic causality-based process algebra. Comput. J. 38(7), 552\u2013565 (1995). https:\/\/doi.org\/10.1093\/comjnl\/38.7.552","journal-title":"Comput. J."},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Brinksma, E., Katoen, J.P., Langerak, R., Latella, D.: Performance analysis and true concurrency semantics. In: Theories and Experiences for Real-Time System Development, pp. 309\u2013337. World Scientific (1994). https:\/\/doi.org\/10.1142\/9789812831583_0012","DOI":"10.1142\/9789812831583_0012"},{"issue":"9\u201310","key":"14_CR9","doi-asserted-by":"publisher","first-page":"925","DOI":"10.1016\/S0169-7552(97)00134-7","volume":"30","author":"E Brinksma","year":"1998","unstructured":"Brinksma, E., Katoen, J., Langerak, R., Latella, D.: Partial order models for quantitative extensions of LOTOS. Comput. Netw. 30(9\u201310), 925\u2013950 (1998). https:\/\/doi.org\/10.1016\/S0169-7552(97)00134-7","journal-title":"Comput. Netw."},{"issue":"2","key":"14_CR10","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-019-00511-9","volume":"22","author":"FB Buonamici","year":"2020","unstructured":"Buonamici, F.B., Belmonte, G., Ciancia, V., Latella, D., Massink, M.: Spatial logics and model checking for medical imaging. Int. J. Softw. Tools Technol. Transf. 22(2), 195\u2013217 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00511-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-031-35355-0_9","volume-title":"FORTE 2023","author":"V Ciancia","year":"2023","unstructured":"Ciancia, V., Gabelaia, D., Latella, D., Massink, M., de Vink, E.P.: On bisimilarity for polyhedral models and SLCS. In: Huisman, M., Ravara, A. (eds.) FORTE 2023. LNCS, vol. 13910, pp. 132\u2013151. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-35355-0_9"},{"issue":"3","key":"14_CR12","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s10009-018-0483-8","volume":"20","author":"V Ciancia","year":"2018","unstructured":"Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Int. J. Softw. Tools Technol. Transf. 20(3), 289\u2013311 (2018). https:\/\/doi.org\/10.1007\/s10009-018-0483-8","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-031-27481-7_16","volume-title":"FM 2023","author":"V Ciancia","year":"2023","unstructured":"Ciancia, V., Groote, J.F., Latella, D., Massink, M., de Vink, E.P.: Minimisation of spatial models using branching bisimilarity. In: Chechik, M., Katoen, J., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 263\u2013281. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_16"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model checking spatial logics for closure spaces. Log. Methods Comput. Sci. 12(4) (2016). https:\/\/doi.org\/10.2168\/LMCS-12(4:2)2016","DOI":"10.2168\/LMCS-12(4:2)2016"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1007\/978-3-319-47166-2_46","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"V Ciancia","year":"2016","unstructured":"Ciancia, V., Latella, D., Massink, M., Pa\u0161kauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 657\u2013673. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_46"},{"key":"14_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-031-15629-8_6","volume-title":"A Journey from Process Algebra via Timed Automata to Model Learning","author":"V Ciancia","year":"2022","unstructured":"Ciancia, V., Latella, D., Massink, M., de Vink, E.P.: Back-and-forth in space: on logics and bisimilarity in closure spaces. In: Jansen, N., Stoelinga, M., van den Bos, P. (eds.) A Journey from Process Algebra via Timed Automata to Model Learning. LNCS, vol. 13560, pp. 98\u2013115. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15629-8_6"},{"issue":"1","key":"14_CR17","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.tcs.2007.05.008","volume":"382","author":"R De Nicola","year":"2007","unstructured":"De Nicola, R., Katoen, J., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theor. Comput. Sci. 382(1), 42\u201370 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2007.05.008","journal-title":"Theor. Comput. Sci."},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-02930-1_36","volume-title":"Automata, Languages and Programming","author":"R De Nicola","year":"2009","unstructured":"De Nicola, R., Latella, D., Loreti, M., Massink, M.: Rate-based transition systems for stochastic process calculi. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 435\u2013446. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02930-1_36"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"De Nicola, R., Latella, D., Loreti, M., Massink, M.: A uniform definition of stochastic process calculi. ACM Comput. Surv. 46(1), 5:1\u20135:35 (2013). https:\/\/doi.org\/10.1145\/2522968.2522973","DOI":"10.1145\/2522968.2522973"},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.peva.2018.05.002","volume":"126","author":"N Gast","year":"2018","unstructured":"Gast, N., Latella, D., Massink, M.: A refined mean field approximation of synchronous discrete-time population models. Perform. Eval. 126, 1\u201321 (2018). https:\/\/doi.org\/10.1016\/j.peva.2018.05.002","journal-title":"Perform. Eval."},{"key":"14_CR21","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-78495-8_5","volume-title":"Messung, Modellierung und Bewertung von Rechen- und Kommunikationssystemen","author":"F Hartleb","year":"1993","unstructured":"Hartleb, F., Quick, A.: Performance evaluation of parallel programs - modeling and monitoring with the tool PEPP. In: Walke, B., Spaniol, O. (eds.) Messung, Modellierung und Bewertung von Rechen- und Kommunikationssystemen, pp. 51\u201363. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/978-3-642-78495-8_5"},{"key":"14_CR22","unstructured":"IEEE Computer Society: IEEE Standard for a High Performance Serial Bus. Std 1394-1995 (1996)"},{"key":"14_CR23","unstructured":"Katoen, J.P., Brinksma, E., Latella, D., Langerak, R.: Stochastic simulation of event structures. In: Ribaudo, M. (ed.) Proceedings of the 4th Workshop on Process Algebra and Performance Modeling (PAPM), pp. 21\u201340. CLUT, Torino (1996). ISBN 88-7992-120-7"},{"key":"14_CR24","unstructured":"Katoen, J.P., Latella, D., Langerak, R., Brinksma, E., Bolognesi, T.: A consistent causality based view on a timed process algebra. In: Cornell, A., Ionescu, D. (eds.) Third AMAST Workshop on Real-Time Systems, pp. 212\u2013226 (1996). Participant Proceedings. Available also as CTIT Technical Report series no 96-03 - ISSN 1381 - 3625"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Katoen, J.P.: Quantitative and qualitative extensions of event structures. Ph.D. thesis, University of Twente, Netherlands (1996). https:\/\/doi.org\/10.3990\/1.9789036507998","DOI":"10.3990\/1.9789036507998"},{"issue":"1\u20132","key":"14_CR26","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1016\/S0304-3975(99)00342-4","volume":"254","author":"JP Katoen","year":"2001","unstructured":"Katoen, J.P., Baier, C., Latella, D.: Metric semantics for true concurrent real time. Theor. Comput. Sci. 254(1\u20132), 501\u2013542 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(99)00342-4","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"14_CR27","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1008649927166","volume":"12","author":"JP Katoen","year":"1998","unstructured":"Katoen, J.P., Langerak, R., Brinksma, E., Latella, D., Bolognesi, T.: A consistent causality-based view on a timed process algebra including urgent interactions. Formal Methods Syst. Des. 12(2), 189\u2013216 (1998). https:\/\/doi.org\/10.1023\/A:1008649927166","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR28","first-page":"253","volume-title":"Formal Description Techniques, VI","author":"JP Katoen","year":"1994","unstructured":"Katoen, J.P., Langerak, R., Latella, D.: Modeling systems by probabilistic process algebra: an event structures approach. In: Tenney, R., Amer, P., \u00dcmit Uyar, M. (eds.) Formal Description Techniques, VI, pp. 253\u2013269. North Holland, Netherlands (1994)"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/3-540-61648-9_52","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J-P Katoen","year":"1996","unstructured":"Katoen, J.-P., Langerak, R., Latella, D., Brinksma, E.: On specifying real-time systems in a causality-based setting. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 385\u2013404. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61648-9_52"},{"key":"14_CR30","unstructured":"Langerak, R.: Bundle event structures: a non-interleaving semantics for LOTOS. In: Diaz, M., Groz, R. (eds.) Formal Description Techniques V, pp. 331\u2013346. IFIP transactions C, Communication systems, North Holland, Netherlands (1991). 5th International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols, FORTE 1992"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Langerak, R.: Deriving a graph rewriting system from a complete finite prefix of an unfolding. In: Castellani, I., Victor, B. (eds.) EXPRESS 1999, pp. 24\u201341. Electronic Notes in Theoretical Computer Science, Elsevier, Netherlands (1999). https:\/\/doi.org\/10.1016\/S1571-0661(05)80293-2. 6th International Workshop on Expressiveness in Concurrency, EXPRESS 1999","DOI":"10.1016\/S1571-0661(05)80293-2"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-48683-6_18","volume-title":"Computer Aided Verification","author":"R Langerak","year":"1999","unstructured":"Langerak, R., Brinksma, E.: A complete finite prefix for process algebra. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 184\u2013195. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_18"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-63141-0_22","volume-title":"CONCUR \u201997: Concurrency Theory","author":"R Langerak","year":"1997","unstructured":"Langerak, R., Brinksma, E., Katoen, J.-P.: Causal ambiguity and partial orders in event structures. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 317\u2013331. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63141-0_22"},{"key":"14_CR34","unstructured":"Latella, D.: Recursive bundle event structures. Technical report, 93-27, University of Twente, Netherlands (1993)"},{"key":"14_CR35","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.scico.2015.06.009","volume":"110","author":"D Latella","year":"2015","unstructured":"Latella, D., Loreti, M., Massink, M.: On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination. Sci. Comput. Program. 110, 23\u201350 (2015). https:\/\/doi.org\/10.1016\/j.scico.2015.06.009","journal-title":"Sci. Comput. Program."},{"key":"14_CR36","doi-asserted-by":"publisher","unstructured":"Latella, D., Massink, M., de\u00a0Vink, E.P.: Bisimulation of labelled state-to-function transition systems coalgebraically. Log. Methods Comput. Sci. 11(4) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(4:16)2015","DOI":"10.2168\/LMCS-11(4:16)2015"},{"key":"14_CR37","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Symbolic model checking. Kluwer (1993). https:\/\/doi.org\/10.1007\/978-1-4615-3190-6","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"1","key":"14_CR38","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF01384314","volume":"6","author":"KL McMillan","year":"1995","unstructured":"McMillan, K.L.: A technique of state space search based on unfolding. Formal Methods Syst. Des. 6(1), 45\u201365 (1995). https:\/\/doi.org\/10.1007\/BF01384314","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR39","unstructured":"Ruys, T.C.: Towards effective model checking. Ph.D. thesis, University of Twente (2001)"},{"key":"14_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-45319-9_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"TC Ruys","year":"2001","unstructured":"Ruys, T.C., Langerak, R., Katoen, J.-P., Latella, D., Massink, M.: First passage time analysis of stochastic process algebra using partial orders. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 220\u2013235. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_16"},{"issue":"1","key":"14_CR41","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1080\/17459737.2013.870610","volume":"8","author":"M Toro","year":"2014","unstructured":"Toro, M., Desainte-Catherine, M., Rueda, C.: Formal semantics for interactive music scores: a framework to design, specify properties and execute interactive scenarios. J. Math. Music 8(1), 93\u2013112 (2014). https:\/\/doi.org\/10.1080\/17459737.2013.870610","journal-title":"J. Math. Music"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75778-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T13:03:11Z","timestamp":1731848591000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75778-5_14"}},"subtitle":["Ten Papers with Pisa and Twente"],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"ISBN":["9783031757778","9783031757785"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75778-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"18 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that\u00a0are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}