{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:11:28Z","timestamp":1746072688774,"version":"3.40.4"},"publisher-location":"Cham","reference-count":79,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908996","type":"print"},{"value":"9783031909009","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The correct operation of safety-critical distributed embedded systems is crucial. Following a model-driven approach, the relevant system aspects must be captured and rigorous ideally fully-automatic analysis of (probabilistic) timed safety properties must be supported. Probabilistic Timed Graph Transformation Systems (PTGTSs) support the modeling of such systems and analysis of such properties via model checking or simulation. However, they only support the modeling of probabilistic choice with a fixed numbers of outcomes and non-deterministic timing delays via timing constraints limiting applicability (descriptive expressiveness) and usefulness (precision of analysis results).<\/jats:p>\n          <jats:p>To remedy this drawback of PTGTSs, we (a) extend PTGTSs to Stochastic Timed Graph Transformation Systems (STGTSs) integrating discrete\/continuous random variables to capture stochastic behavior and (b) outline an adaptation of PTGTS model checking for STGTSs to enable analysis w.r.t. probabilistic timed safety properties. Relying on a running example in which shuttles navigating on a track topology must avoid derailing, we exemplify STGTS support for modeling and analysis.\n<\/jats:p>","DOI":"10.1007\/978-3-031-90900-9_10","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:45:19Z","timestamp":1745988319000},"page":"188-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Stochastic Timed Graph Transformation Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9828-618X","authenticated-orcid":false,"given":"Sven","family":"Schneider","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9275-806X","authenticated-orcid":false,"given":"Maria","family":"Maximova","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4723-730X","authenticated-orcid":false,"given":"Holger","family":"Giese","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"R. Alur and D. L. Dill. \u201cA Theory of Timed Automata\u201d. In: Theor. Comput. Sci. 126.2 (1994), pp. 183\u2013235. doi: https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8.","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"10_CR2","unstructured":"Amazon. Neptune. url: https:\/\/aws.amazon.com\/neptune\/."},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"T. Arendt, E. Biermann, S. Jurack, C. Krause, and G. Taentzer. \u201cHenshin: Advanced Concepts and Tools for In-Place EMF Model Transformations\u201d. In: Model Driven Engineering Languages and Systems - 13th International Conference, MODELS 2010, Oslo, Norway, October 3-8, 2010, Proceedings, Part I. Ed. by D. C. Petriu, N. Rouquette, and \u00d8. Haugen. Vol. 6394. Lecture Notes in Computer Science. Springer, 2010, pp. 121\u2013135. isbn: 978-3-642-16144-5. doi: https:\/\/doi.org\/10.1007\/978-3-642-16145-2_9.","DOI":"10.1007\/978-3-642-16145-2_9"},{"key":"10_CR4","unstructured":"Augur 2. Universit\u00e4t Duisburg-Essen. 2008. url: https:\/\/www.ti.inf.uni-due.de\/en\/research\/tools\/augur2."},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"A. Aziz, K. Sanwal, V. Singhal, and R. K. Brayton. \u201cModel-checking continous-time Markov chains\u201d. In: ACM Trans. Comput. Log. 1.1 (2000), pp. 162\u2013170. doi: https:\/\/doi.org\/10.1145\/343369.343402.","DOI":"10.1145\/343369.343402"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"C. Baier, B. R. Haverkort, H. Hermanns, and J. Katoen. \u201cModel Checking Continuous-Time Markov Chains by Transient Analysis\u201d. In: Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings. Ed. by E. A. Emerson and A. P. Sistla. Vol. 1855. Lecture Notes in Computer Science. Springer, 2000, pp. 358\u2013372. doi: https:\/\/doi.org\/10.1007\/10722167_28.","DOI":"10.1007\/10722167_28"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"C. Baier, B. R. Haverkort, H. Hermanns, and J. Katoen. \u201cModel-Checking Algorithms for Continuous-Time Markov Chains\u201d. In: IEEE Trans. Software Eng. 29.6 (2003), pp. 524\u2013541. doi: https:\/\/doi.org\/10.1109\/TSE.2003.1205180.","DOI":"10.1109\/TSE.2003.1205180"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"M. Bebbington, C. Lai, and R. Zitikis. \u201cUseful periods for lifetime distributions with bathtub shaped hazard rate functions\u201d. In: IEEE Trans. Reliab. 55.2 (2006), pp. 245\u2013251. doi: https:\/\/doi.org\/10.1109\/TR.2001.874943.","DOI":"10.1109\/TR.2001.874943"},{"key":"10_CR9","unstructured":"B. Becker. \u201cArchitectural modelling and verification of open service-oriented systems of systems\u201d. PhD thesis. Hasso Plattner Institute, University of Potsdam, 2014. url: http:\/\/nbn-resolving.de\/urn:nbn:de:kobv:517-opus-70158."},{"key":"10_CR10","unstructured":"B. Becker and H. Giese. Cyber-Physical Systems with Dynamic Structure: Towards Modeling and Verification of Inductive Invariants. Tech. rep. 64. Hasso Plattner Institute, University of Potsdam, 2012. url: https:\/\/nbn-resolving.org\/urn:nbn:de:kobv:517-opus-62437."},{"key":"10_CR11","unstructured":"B. Becker and H. Giese. Modeling and Verifying Dynamic Evolving Service-Oriented Architectures. Tech. rep. 75. Hasso Plattner Institute, University of Potsdam, 2013. url: https:\/\/nbn-resolving.org\/urn:nbn:de:kobv:517-opus-65112."},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"B. Becker and H. Giese. \u201cOn Safe Service-Oriented Real-Time Coordination for Autonomous Vehicles\u201d. In: 11th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2008), 5-7 May 2008, Orlando, Florida, USA. IEEE Computer Society, 2008, pp. 203\u2013210. isbn: 978-0-7695-3132-8. doi: https:\/\/doi.org\/10.1109\/ISORC.2008.13. url: https:\/\/ieeexplore.ieee.org\/xpl\/mostRecentIssue.jsp?punumber=4519543.","DOI":"10.1109\/ISORC.2008.13"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"J. Bengtsson and W. Yi. \u201cTimed Automata: Semantics, Algorithms and Tools\u201d. In: Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichst\u00e4tt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned]. Ed. by J. Desel, W. Reisig, and G. Rozenberg. Vol. 3098. Lecture Notes in Computer Science. Springer, 2003, pp. 87\u2013124. doi: https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3.","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"H. C. Bohnenkamp, P. R. D\u2019Argenio, H. Hermanns, and J. Katoen. \u201cMODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems\u201d. In: IEEE Trans. Software Eng. 32.10 (2006), pp.\u00a0812\u2013830. doi: https:\/\/doi.org\/10.1109\/TSE.2006.104.","DOI":"10.1109\/TSE.2006.104"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. \u201cKronos: A Model-Checking Tool for Real-Time Systems\u201d. In: Computer Aided Verification, 10th International Conference, CAV \u201998, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings. Ed. by A. J. Hu and M. Y. Vardi. Vol. 1427. Lecture Notes in Computer Science. Springer, 1998, pp. 546\u2013550. doi: https:\/\/doi.org\/10.1007\/BFb0028779.","DOI":"10.1007\/BFb0028779"},{"key":"10_CR16","unstructured":"Christian Krause. IPTA edition of PRISM. https:\/\/www.hpi.uni-potsdam.de\/giese\/public\/mdelab\/2011\/06\/08\/ipta-edition-of-prism\/. Hasso Plattner Institute at the University of Potsdam, 2011."},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine. \u201cThe Tool KRONOS\u201d. In: Hybrid Systems III: Verification and Control, Proceedings of the DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA. Ed. by R. Alur, T. A. Henzinger, and E. D. Sontag. Vol. 1066. Lecture Notes in Computer Science. Springer, 1995, pp. 208\u2013219. isbn: 3-540-61155-X. doi: https:\/\/doi.org\/10.1007\/BFb0020947.","DOI":"10.1007\/BFb0020947"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"D. L. Dill. \u201cTiming Assumptions and Verification of Finite-State Concurrent Systems\u201d. In: Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings. Ed. by J. Sifakis. Vol. 407. Lecture Notes in Computer Science. Springer, 1989, pp. 197\u2013212. doi: https:\/\/doi.org\/10.1007\/3-540-52148-8_17.","DOI":"10.1007\/3-540-52148-8_17"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"R. Durrett. Probability: Theory and Examples (Cambridge Series in Statistical and Probabilistic Mathematics). 5th\u00a0ed. Vol. 49. Cambridge New York, NY: Cambridge University Press, 2019. isbn: 978-1-108-47368-2.","DOI":"10.1017\/9781108591034"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"J. Dyck and H. Giese. \u201ck-Inductive Invariant Checking for Graph Transformation Systems\u201d. In: Graph Transformation - 10th International Conference, ICGT 2017, Held as Part of STAF 2017, Marburg, Germany, July 18-19, 2017, Proceedings. Ed. by J. de Lara and D. Plump. Vol. 10373. Lecture Notes in Computer Science. Springer, 2017, pp.\u00a0142\u2013158. isbn: 978-3-319-61469-4. doi: https:\/\/doi.org\/10.1007\/978-3-319-61470-0_9.","DOI":"10.1007\/978-3-319-61470-0_9"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer. Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2006. isbn: 978-3-540-31187-4. doi: https:\/\/doi.org\/10.1007\/3-540-31188-2.","DOI":"10.1007\/3-540-31188-2"},{"key":"10_CR22","unstructured":"W. Feller. An introduction to probability theory and its applications, Volume 1. Wiley, 1968. isbn: 978-0471257080."},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"M. Fr\u00e4nzle, E. M. Hahn, H. Hermanns, N. Wolovick, and L. Zhang. \u201cMeasurability and safety verification for stochastic hybrid systems\u201d. In: Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011. Ed. by M. Caccamo, E. Frazzoli, and R. Grosu. ACM, 2011, pp.\u00a043\u201352. doi: https:\/\/doi.org\/10.1145\/1967701.1967710.","DOI":"10.1145\/1967701.1967710"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"A. H. Ghamarian, M. de Mol, A. Rensink, E. Zambon, and M. Zimakova. \u201cModelling and analysis using GROOVE\u201d. In: Int. J. Softw. Tools Technol. Transf. 14.1 (2012), pp. 15\u201340. doi: https:\/\/doi.org\/10.1007\/s10009-011-0186-x.","DOI":"10.1007\/s10009-011-0186-x"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"H. Giese. \u201cModeling and Verification of Cooperative Self-adaptive Mechatronic Systems\u201d. In: Reliable Systems on Unreliable Networked Platforms - 12th Monterey Workshop 2005, Laguna Beach, CA, USA, September 22-24, 2005. Revised Selected Papers. Ed. by F. Kordon and J. Sztipanovits. Vol. 4322. Lecture Notes in Computer Science. Springer, 2005, pp. 258\u2013280. isbn: 978-3-540-71155-1. doi: https:\/\/doi.org\/10.1007\/978-3-540-71156-8_14.","DOI":"10.1007\/978-3-540-71156-8_14"},{"key":"10_CR26","unstructured":"GROOVE Team. Graphs for Object-Oriented Verification (GROOVE). url: https:\/\/groove.cs.utwente.nl. University of Twente, 2011."},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"S. Gyapay, R. Heckel, and D. Varr\u00f3. \u201cGraph Transformation with Time: Causality and Logical Clocks\u201d. In: Graph Transformation, First International Conference, ICGT 2002, Barcelona, Spain, October 7-12, 2002, Proceedings. Ed. by A. Corradini, H. Ehrig, H. Kreowski, and G. Rozenberg. Vol. 2505. Lecture Notes in Computer Science. Springer, 2002, pp. 120\u2013134. doi: https:\/\/doi.org\/10.1007\/3-540-45832-8_11.","DOI":"10.1007\/3-540-45832-8_11"},{"key":"10_CR28","unstructured":"S. Gyapay, D. Varr\u00f3, and R. Heckel. \u201cGraph Transformation with Time\u201d. In: Fundam. Inform. 58.1 (2003), pp. 1\u201322. url: https:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi58-1-02."},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"E. M. Hahn, A. Hartmanns, and H. Hermanns. \u201cReachability and Reward Checking for Stochastic Timed Automata\u201d. In: Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70 (2014). doi: https:\/\/doi.org\/10.14279\/tuj.eceasst.70.968.","DOI":"10.14279\/tuj.eceasst.70.968"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"E. M. Hahn, A. Hartmanns, H. Hermanns, and J. Katoen. \u201cA compositional modelling and analysis framework for stochastic hybrid systems\u201d. In: Formal Methods Syst. Des. 43.2 (2013), pp. 191\u2013232. doi: https:\/\/doi.org\/10.1007\/s10703-012-0167-z.","DOI":"10.1007\/s10703-012-0167-z"},{"key":"10_CR31","doi-asserted-by":"publisher","unstructured":"A. Hartmanns. \u201cModel-Checking and Simulation for Stochastic Timed Systems\u201d. In: Formal Methods for Components and Objects - 9th International Symposium, FMCO 2010, Graz, Austria, November 29 - December 1, 2010. Revised Papers. Ed. by B. K. Aichernig, F. S. de Boer, and M. M. Bonsangue. Vol. 6957. Lecture Notes in Computer Science. Springer, 2010, pp. 372\u2013391. doi: https:\/\/doi.org\/10.1007\/978-3-642-25271-6_20.","DOI":"10.1007\/978-3-642-25271-6_20"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"A. Hartmanns and H. Hermanns. \u201cA Modest Approach to Checking Probabilistic Timed Automata\u201d. In: QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009. IEEE Computer Society, 2009, pp. 187\u2013196. doi: https:\/\/doi.org\/10.1109\/QEST.2009.41.","DOI":"10.1109\/QEST.2009.41"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"A. Hartmanns and H. Hermanns. \u201cThe Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification\u201d. In: Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings. Ed. by E. \u00c1brah\u00e1m and K. Havelund. Vol. 8413. Lecture Notes in Computer Science. Springer, 2014, pp. 593\u2013598. doi: https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51.","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"R. Heckel, G. Lajios, and S. Menge. \u201cStochastic Graph Transformation Systems\u201d. In: ICGT 2004. Ed. by H. Ehrig, G. Engels, F. Parisi-Presicce, and G. Rozenberg. Vol. 3256. LNCS. Springer, 2004, pp.\u00a0210\u2013225. doi: https:\/\/doi.org\/10.1007\/978-3-540-30203-2_16.","DOI":"10.1007\/978-3-540-30203-2_16"},{"key":"10_CR35","unstructured":"R. Heckel, G. Lajios, and S. Menge. \u201cStochastic Graph Transformation Systems\u201d. In: Fundam. Inform. 74.1 (2006), pp. 63\u201384. url: https:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi74-1-04."},{"key":"10_CR36","unstructured":"Henshin Team. Henshin. https:\/\/www.eclipse.org\/henshin\/. 2021."},{"key":"10_CR37","doi-asserted-by":"publisher","unstructured":"T. A. Henzinger. \u201cThe Theory of Hybrid Automata\u201d. In: Verification of Digital and Hybrid Systems. Ed. by M. K. Inan and R. P. Kurshan. Berlin, Heidelberg: Springer Berlin Heidelberg, 2000, pp. 265\u2013292. isbn: 978-3-642-59615-5. doi: https:\/\/doi.org\/10.1007\/978-3-642-59615-5_13.","DOI":"10.1007\/978-3-642-59615-5_13"},{"key":"10_CR38","doi-asserted-by":"publisher","unstructured":"H. Hermanns, D. N. Jansen, and Y. S. Usenko. \u201cFrom StoCharts to MoDeST: a comparative reliability analysis of train radio communications\u201d. In: Proceedings of the Fifth International Workshop on Software and Performance, WOSP 2005, Palma, Illes Balears, Spain, July 12-14, 2005. ACM, 2005, pp. 13\u201323. doi: https:\/\/doi.org\/10.1145\/1071021.1071023.","DOI":"10.1145\/1071021.1071023"},{"key":"10_CR39","doi-asserted-by":"publisher","unstructured":"E. Jakumeit, S. Buchwald, D. Wagelaar, L. Dan, \u00c1. Heged\u00fcs, M. Herrmannsd\u00f6rfer, T. Horn, E. Kalnina, C. Krause, K. Lano, M. Lepper, A. Rensink, L. M. Rose, S. W\u00e4tzoldt, and S. Mazanek. \u201cA survey and comparison of transformation tools based on the transformation tool contest\u201d. In: Sci. Comput. Program. 85 (2014), pp. 41\u201399. doi: https:\/\/doi.org\/10.1016\/j.scico.2013.10.009.","DOI":"10.1016\/j.scico.2013.10.009"},{"key":"10_CR40","doi-asserted-by":"publisher","unstructured":"D. N. Jansen, H. Hermanns, and J. Katoen. \u201cA Probabilistic Extension of UML Statecharts\u201d. In: Formal Techniques in Real-Time and Fault-Tolerant Systems, 7th International Symposium, FTRTFT 2002, Co-sponsored by IFIP WG 2.2, Oldenburg, Germany, September 9-12, 2002, Proceedings. Ed. by W. Damm and E. Olderog. Vol. 2469. Lecture Notes in Computer Science. Springer, 2002, pp. 355\u2013374. doi: https:\/\/doi.org\/10.1007\/3-540-45739-9_21.","DOI":"10.1007\/3-540-45739-9_21"},{"key":"10_CR41","doi-asserted-by":"publisher","unstructured":"J. Katoen, M. Z. Kwiatkowska, G. Norman, and D. Parker. \u201cFaster and Symbolic CTMC Model Checking\u201d. In: Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001, Aachen, Germany, September 12-14, 2001, Proceedings. Ed. by L. de Alfaro and S. Gilmore. Vol. 2165. Lecture Notes in Computer Science. Springer, 2001, pp.\u00a023\u201338. doi: https:\/\/doi.org\/10.1007\/3-540-44804-7_2.","DOI":"10.1007\/3-540-44804-7_2"},{"key":"10_CR42","doi-asserted-by":"publisher","unstructured":"B. K\u00f6nig and V. Kozioura. \u201cAugur 2\u2014A New Version of a Tool for the Analysis of Graph Transformation Systems\u201d. In: ENTCS 211 (2008), pp.\u00a0201\u2013210. doi: https:\/\/doi.org\/10.1016\/j.entcs.2008.04.042.","DOI":"10.1016\/j.entcs.2008.04.042"},{"key":"10_CR43","doi-asserted-by":"publisher","unstructured":"C. Krause and H. Giese. \u201cModel Checking Probabilistic Real-Time Properties for Service-Oriented Systems with Service Level Agreements\u201d. In: Proceedings 13th International Workshop on Verification of Infinite-State Systems, INFINITY 2011, Taipei, Taiwan, 10th October 2011. Ed. by F. Yu and C. Wang. Vol. 73. EPTCS. 2011, pp. 64\u201378. doi: https:\/\/doi.org\/10.4204\/EPTCS.73.8.","DOI":"10.4204\/EPTCS.73.8"},{"key":"10_CR44","doi-asserted-by":"publisher","unstructured":"C. Krause and H. Giese. \u201cProbabilistic Graph Transformation Systems\u201d. In: Graph Transformations - 6th International Conference, ICGT 2012, Bremen, Germany, September 24-29, 2012. Proceedings. Ed. by H. Ehrig, G. Engels, H. Kreowski, and G. Rozenberg. Vol. 7562. Lecture Notes in Computer Science. Springer, 2012, pp. 311\u2013325. isbn: 978-3-642-33653-9. doi: https:\/\/doi.org\/10.1007\/978-3-642-33654-6_21.","DOI":"10.1007\/978-3-642-33654-6_21"},{"key":"10_CR45","unstructured":"Kronos Team. Kronos. https:\/\/www-verimag.imag.fr\/DIST-TOOLS\/TEMPO\/kronos\/. 2002."},{"key":"10_CR46","doi-asserted-by":"publisher","unstructured":"M. Z. Kwiatkowska, G. Norman, and D. Parker. \u201cPRISM 4.0: Verification of Probabilistic Real-Time Systems\u201d. In: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Ed. by G. Gopalakrishnan and S. Qadeer. Vol. 6806. Lecture Notes in Computer Science. Springer, 2011, pp.\u00a0585\u2013591. isbn: 978-3-642-22109-5. doi: https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"10_CR47","doi-asserted-by":"publisher","unstructured":"M. Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. \u201cAutomatic verification of real-time systems with discrete probability distributions\u201d. In: Theor. Comput. Sci. 282.1 (2002), pp.\u00a0101\u2013150. doi: https:\/\/doi.org\/10.1016\/S0304-3975(01)00046-9.","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"10_CR48","doi-asserted-by":"publisher","unstructured":"M. Z. Kwiatkowska, G. Norman, J. Sproston, and F. Wang. \u201cSymbolic Model Checking for Probabilistic Timed Automata\u201d. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings. Ed. by Y. Lakhnech and S. Yovine. Vol. 3253. Lecture Notes in Computer Science. Springer, 2004, pp. 293\u2013308. isbn: 3-540-23167-6. doi: https:\/\/doi.org\/10.1007\/978-3-540-30206-3_21.","DOI":"10.1007\/978-3-540-30206-3_21"},{"key":"10_CR49","doi-asserted-by":"publisher","unstructured":"J. de Lara, E. Guerra, A. Boronat, R. Heckel, and P. Torrini. \u201cDomain-specific discrete event modelling and simulation using graph transformation\u201d. In: Softw. Syst. Model. 13.1 (2014), pp.\u00a0209\u2013238. doi: https:\/\/doi.org\/10.1007\/s10270-012-0242-3.","DOI":"10.1007\/s10270-012-0242-3"},{"key":"10_CR50","doi-asserted-by":"publisher","unstructured":"M. Maximova, H. Giese, and C. Krause. \u201cProbabilistic Timed Graph Transformation Systems\u201d. In: Graph Transformation - 10th International Conference, ICGT 2017, Held as Part of STAF 2017, Marburg, Germany, July 18-19, 2017, Proceedings. Ed. by J. de Lara and D. Plump. Vol. 10373. Lecture Notes in Computer Science. Springer, 2017, pp.\u00a0159\u2013175. isbn: 978-3-319-61469-4. doi: https:\/\/doi.org\/10.1007\/978-3-319-61470-0_10.","DOI":"10.1007\/978-3-319-61470-0_10"},{"key":"10_CR51","unstructured":"M. Maximova, H. Giese, and C. Krause. Probabilistic timed graph transformation systems. Tech. rep. 118. Potsdam, Germany: Hasso Plattner Institute at the University of Potsdam, 2017."},{"key":"10_CR52","doi-asserted-by":"publisher","unstructured":"M. Maximova, H. Giese, and C. Krause. \u201cProbabilistic timed graph transformation systems\u201d. In: J. Log. Algebr. Meth. Program. 101 (2018), pp. 110\u2013131. doi: https:\/\/doi.org\/10.1016\/j.jlamp.2018.09.003.","DOI":"10.1016\/j.jlamp.2018.09.003"},{"key":"10_CR53","doi-asserted-by":"publisher","unstructured":"M. Maximova, S. Schneider, and H. Giese. \u201cCompositional Analysis of Probabilistic Timed Graph Transformation Systems\u201d. In: Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. Ed. by E. Guerra and M. Stoelinga. Vol. 12649. Lecture Notes in Computer Science. Springer, 2021, pp. 196\u2013217. doi: https:\/\/doi.org\/10.1007\/978-3-030-71500-7_10.","DOI":"10.1007\/978-3-030-71500-7_10"},{"key":"10_CR54","doi-asserted-by":"publisher","unstructured":"M. Maximova, S. Schneider, and H. Giese. \u201cCompositional Analysis of Probabilistic Timed Graph Transformation Systems\u201d. In: Form. Asp. Comput. (Nov. 2022). Just Accepted. issn: 0934-5043. doi: https:\/\/doi.org\/10.1145\/3572782.","DOI":"10.1145\/3572782"},{"key":"10_CR55","doi-asserted-by":"publisher","unstructured":"M. Maximova, S. Schneider, and H. Giese. Interval Probabilistic Timed Graph Transformation Systems. Tech. rep. 134. Hasso Plattner Institute, University of Potsdam, 2021. doi: https:\/\/doi.org\/10.25932\/publishup-51289.","DOI":"10.25932\/publishup-51289"},{"key":"10_CR56","doi-asserted-by":"publisher","unstructured":"M. Maximova, S. Schneider, and H. Giese. \u201cInterval Probabilistic Timed Graph Transformation Systems\u201d. In: Graph Transformation - 14th International Conference, ICGT 2021, Held as Part of STAF 2021, Virtual Event, June 24-25, 2021, Proceedings. Ed. by F. Gadducci and T. Kehrer. Vol. 12741. Lecture Notes in Computer Science. Springer, 2021, pp.\u00a0221\u2013239. doi: https:\/\/doi.org\/10.1007\/978-3-030-78946-6_12.","DOI":"10.1007\/978-3-030-78946-6_12"},{"key":"10_CR57","unstructured":"Modest Team. The Modest Toolset. https:\/\/www.modestchecker.net\/. Universiteit Twente, 2023."},{"key":"10_CR58","unstructured":"Neo4J Team. Neo4J. url: https:\/\/neo4j.com\/."},{"key":"10_CR59","unstructured":"S. Neumann. \u201cModellierung und Verifikation zeitbehafteter Graphtransformationssysteme mittels Groove\u201d. MA thesis. University of Paderborn, 2007."},{"key":"10_CR60","doi-asserted-by":"publisher","unstructured":"J. R. Norris. Markov Chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, 1997. doi: https:\/\/doi.org\/10.1017\/CBO9780511810633.","DOI":"10.1017\/CBO9780511810633"},{"key":"10_CR61","unstructured":"OMG. Unified Modeling Language. 2017. url: https:\/\/www.omg.org\/spec\/UML\/."},{"key":"10_CR62","doi-asserted-by":"publisher","unstructured":"F. Orejas. \u201cSymbolic graphs for attributed graph constraints\u201d. In: J. Symb. Comput. 46.3 (2011), pp. 294\u2013315. doi: https:\/\/doi.org\/10.1016\/j.jsc.2010.09.009.","DOI":"10.1016\/j.jsc.2010.09.009"},{"key":"10_CR63","unstructured":"K. Pennemann. \u201cDevelopment of correct graph transformation systems\u201d. urn: urn:nbn:de:gbv:715-oops-9483. PhD thesis. University of Oldenburg, Germany, 2009. url: https:\/\/oops.uni-oldenburg.de\/884\/."},{"key":"10_CR64","unstructured":"PRISM Team. PRISM Probabilistic Model Checker. https:\/\/www.prismmodelchecker.org\/. 2023."},{"key":"10_CR65","doi-asserted-by":"publisher","unstructured":"M. O. Rabin. \u201cProbabilistic Automata\u201d. In: Information and Control 6.3 (1963), pp. 230\u2013245. doi: https:\/\/doi.org\/10.1016\/S0019-9958(63)90290-0.","DOI":"10.1016\/S0019-9958(63)90290-0"},{"key":"10_CR66","unstructured":"RailCab Project. url: https:\/\/www.hni.uni-paderborn.de\/cim\/projekte\/railcab."},{"key":"10_CR67","doi-asserted-by":"publisher","unstructured":"M. Rausand. Reliability of Safety-Critical Systems. Hoboken, New Jersey: John Wiley & Sons, Ltd, 2014. isbn: 978-1-118-11272-4. doi: https:\/\/doi.org\/10.1002\/9781118776353.","DOI":"10.1002\/9781118776353"},{"key":"10_CR68","unstructured":"S. M. Ross. Introduction to Probability Models. London, United Kingdom: Elsevier, Academic Press, 2019. isbn: 978-0-12-814346-9."},{"key":"10_CR69","unstructured":"SAP. Hana. url: https:\/\/www.sap.com\/products\/technology-platform\/hana.html."},{"key":"10_CR70","doi-asserted-by":"publisher","unstructured":"S. Schneider, M. Maximova, and H. Giese. \u201cProbabilistic Metric Temporal Graph Logic\u201d. In: Graph Transformation - 15th International Conference, ICGT 2022, Held as Part of STAF 2022, Nantes, France, July 7-8, 2022, Proceedings. Ed. by N. Behr and D. Str\u00fcber. Vol. 13349. Lecture Notes in Computer Science. Springer, 2022, pp. 58\u201376. doi: https:\/\/doi.org\/10.1007\/978-3-031-09843-7_4.","DOI":"10.1007\/978-3-031-09843-7_4"},{"key":"10_CR71","doi-asserted-by":"publisher","unstructured":"S. Schneider, M. Maximova, L. Sakizloglou, and H. Giese. \u201cFormal testing of timed graph transformation systems using metric temporal graph logic\u201d. In: Int. J. Softw. Tools Technol. Transf. 23.3 (2021), pp. 411\u2013488. doi: https:\/\/doi.org\/10.1007\/s10009-020-00585-w.","DOI":"10.1007\/s10009-020-00585-w"},{"key":"10_CR72","unstructured":"R. Segala. \u201cModeling and verification of randomized distributed real-time systems\u201d. PhD thesis. Massachusetts Institute of Technology, Cambridge, MA, USA, 1995. url: https:\/\/hdl.handle.net\/1721.1\/36560."},{"key":"10_CR73","doi-asserted-by":"publisher","unstructured":"A. N. Shiryaev. Probability-1. 3rd\u00a0ed. Title Graduate Texts in Mathematics. Springer New York, NY. doi: https:\/\/doi.org\/10.1007\/978-0-387-72206-1.","DOI":"10.1007\/978-0-387-72206-1"},{"key":"10_CR74","unstructured":"UPPAAL Team. UPPAAL. https:\/\/uppaal.org\/. Department of Information Technology at Uppsala University, Sweden and Department of Computer Science at Aalborg University, Denmark, 2021."},{"key":"10_CR75","doi-asserted-by":"publisher","unstructured":"G. P. Yanev. \u201cExponential and Hypoexponential Distributions: Some Characterizations\u201d. In: Mathematics 8.12 (2020). issn: 2227-7390. doi: https:\/\/doi.org\/10.3390\/math8122207.","DOI":"10.3390\/math8122207"},{"key":"10_CR76","doi-asserted-by":"publisher","unstructured":"W. Yi. \u201cReal-Time Behaviour of Asynchronous Agents\u201d. In: CONCUR \u201990, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings. Ed. by J. C. M. Baeten and J. W. Klop. Vol. 458. Lecture Notes in Computer Science. Springer, 1990, pp. 502\u2013520. doi: https:\/\/doi.org\/10.1007\/BFb0039080.","DOI":"10.1007\/BFb0039080"},{"key":"10_CR77","doi-asserted-by":"publisher","unstructured":"J. Zhang, J. Zhao, Z. Huang, and Z. Cao. \u201cModel Checking Interval Probabilistic Timed Automata\u201d. In: 2009 First International Conference on Information Science and Engineering. 2009, pp.\u00a04936\u20134940. doi: https:\/\/doi.org\/10.1109\/ICISE.2009.749.","DOI":"10.1109\/ICISE.2009.749"},{"key":"10_CR78","doi-asserted-by":"publisher","unstructured":"C. Z\u00f6llner, M. Barkowsky, M. Maximova, and H. Giese. \u201cOn the Complexity of Simulating Probabilistic Timed Graph Transformation Systems\u201d. In: Graph Transformation - 14th International Conference, ICGT 2021, Held as Part of STAF 2021, Virtual Event, June 24-25, 2021, Proceedings. Ed. by F. Gadducci and T. Kehrer. Vol. 12741. Lecture Notes in Computer Science. Springer, 2021, pp. 262\u2013279. doi: https:\/\/doi.org\/10.1007\/978-3-030-78946-6_14.","DOI":"10.1007\/978-3-030-78946-6_14"},{"key":"10_CR79","doi-asserted-by":"publisher","unstructured":"C. Z\u00f6llner, M. Barkowsky, M. Maximova, M. Schneider, and H. Giese. \u201cA Simulator for Probabilistic Timed Graph Transformation Systems with Complex Large-Scale Topologies\u201d. In: Graph Transformation - 13th International Conference, ICGT 2020, Held as Part of STAF 2020, Bergen, Norway, June 25-26, 2020, Proceedings. Ed. by F. Gadducci and T. Kehrer. Vol. 12150. Lecture Notes in Computer Science. Springer, 2020, pp.\u00a0325\u2013334. doi: https:\/\/doi.org\/10.1007\/978-3-030-51372-6_20.","DOI":"10.1007\/978-3-030-51372-6_20"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90900-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:45:28Z","timestamp":1745988328000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90900-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908996","9783031909009"],"references-count":79,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90900-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}