{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:14:59Z","timestamp":1762460099476,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,9,30]]},"abstract":"<jats:p>The analysis of behavioral models is of high importance for cyber-physical systems, as the systems often encompass complex behavior based on, e.g., concurrent components with mutual exclusion or probabilistic failures on demand. The rule-based formalism of Probabilistic Timed Graph Transformation Systems (PTGTSs) is a suitable choice when the models representing states of the system can be understood as graphs and timed and probabilistic behavior is important. However, model checking PTGTSs is limited to systems with rather small state spaces.<\/jats:p>\n          <jats:p>\n            We present an approach for the analysis of large-scale systems modeled as PTGTSs by systematically decomposing their state spaces into manageable fragments. To obtain qualitative and quantitative analysis results for a large-scale system, we verify that results obtained for its fragments serve as overapproximations for the corresponding results of the large-scale system. Hence, our approach allows for the detection of violations of qualitative and quantitative safety properties for the large-scale system under analysis. We consider a running example in which shuttles drive on tracks of a large-scale topology and autonomously coordinate their local behavior with other shuttles nearby. For this running example, we verify that (a) shuttles can always make the expected forward progress using several properties, (b) shuttles never collide, and (c) shuttles are unlikely to execute emergency brakes in two scenarios. In our evaluation, we apply an implementation of our approach in the tool\n            <jats:sc>AutoGraph<\/jats:sc>\n            to our running example.\n          <\/jats:p>","DOI":"10.1145\/3572782","type":"journal-article","created":{"date-parts":[[2022,11,30]],"date-time":"2022-11-30T13:05:47Z","timestamp":1669813547000},"page":"1-79","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Compositional Analysis of Probabilistic Timed Graph Transformation Systems"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9275-806X","authenticated-orcid":false,"given":"Maria","family":"Maximova","sequence":"first","affiliation":[{"name":"University of Potsdam,Hasso Plattner Institute, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9828-618X","authenticated-orcid":false,"given":"Sven","family":"Schneider","sequence":"additional","affiliation":[{"name":"University of Potsdam,Hasso Plattner Institute, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4723-730X","authenticated-orcid":false,"given":"Holger","family":"Giese","sequence":"additional","affiliation":[{"name":"University of Potsdam,Hasso Plattner Institute, Germany"}]}],"member":"320","published-online":{"date-parts":[[2023,9,13]]},"reference":[{"key":"e_1_3_3_2_2","volume-title":"UPPAAL","author":"Department of Information Technology at Uppsala University, Sweden and Department of Computer Science at Aalborg University, Denmark","year":"2021","unstructured":"Department of Information Technology at Uppsala University, Sweden and Department of Computer Science at Aalborg University, Denmark 2021. UPPAAL. Department of Information Technology at Uppsala University, Sweden and Department of Computer Science at Aalborg University, Denmark. Retrieved from https:\/\/uppaal.org\/."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_3_4_2","volume-title":"International Conference on Integrated Design & Process Technology","author":"Baldan Paolo","year":"2002","unstructured":"Paolo Baldan, Andrea Corradini, and Barbara K\u00f6nig. 2002. Static analysis of distributed systems with mobility specified by graph grammars\u2014A case study. In International Conference on Integrated Design & Process Technology. SDPS."},{"key":"e_1_3_3_5_2","volume-title":"Architectural Modelling and Verification of Open Service-oriented Systems of Systems","author":"Becker Basil","year":"2014","unstructured":"Basil Becker. 2014. Architectural Modelling and Verification of Open Service-oriented Systems of Systems. Ph. D. Dissertation. Hasso-Plattner-Institut f\u00fcr Softwaresystemtechnik, Universit\u00e4t Potsdam. Retrieved from http:\/\/opus.kobv.de\/ubp\/volltexte\/2014\/7015\/."},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134297"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.13"},{"key":"e_1_3_3_8_2","volume-title":"Correct Dynamic Service-oriented Architectures: Modeling and Compositional Verification with Dynamic Collaborations","author":"Becker Basil","year":"2009","unstructured":"Basil Becker, Holger Giese, and Stefan Neumann. 2009. Correct Dynamic Service-oriented Architectures: Modeling and Compositional Verification with Dynamic Collaborations. Technical Report 29. Hasso Plattner Institute at the University of Potsdam."},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-012-0242-3"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52148-8_17"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21145-9_2"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.12.006"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51372- 6_13"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78946-6_9"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.25932\/publishup-44274"},{"key":"e_1_3_3_18_2","volume-title":"Fundamentals of Algebraic Graph Transformation","author":"Ehrig Hartmut","year":"2006","unstructured":"Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. 2006. Fundamentals of Algebraic Graph Transformation. Springer."},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33654-6_16"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71156-8_14"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_16"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36249-1_6"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940078"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508007202"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30203-2_16"},{"issue":"1","key":"e_1_3_3_26_2","first-page":"63","article-title":"Stochastic graph transformation systems","volume":"74","author":"Heckel Reiko","year":"2006","unstructured":"Reiko Heckel, Georgios Lajios, and Sebastian Menge. 2006. Stochastic graph transformation systems. Fundam. Inform. 74, 1 (2006), 63\u201384. Retrieved from http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi74-1-04.","journal-title":"Fundam. Inform."},{"key":"e_1_3_3_27_2","unstructured":"Henshin Team. 2021. Henshin. Retrieved from https:\/\/www.eclipse.org\/henshin\/."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2465449.2465456"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44804-7_2"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.73.8"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33654-6_21"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2013.10.001"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_21"},{"key":"e_1_3_3_36_2","volume-title":"Behavior and Confluence Analysis of M-adhesive Transformation Systems Using M-functors","author":"Maximova Maria","year":"2019","unstructured":"Maria Maximova. 2019. Behavior and Confluence Analysis of M-adhesive Transformation Systems Using M-functors. Ph. D. Dissertation. Technical University of Berlin, Germany. Retrieved from https:\/\/nbn-resolving.org\/urn:nbn:de:101:1-2019122500571906965554."},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.09.003"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71500-7_10"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78946-6_12"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78946-6_12"},{"key":"e_1_3_3_41_2","unstructured":"Microsoft Corporation. 2021. Z3. Retrieved from https:\/\/github.com\/Z3Prover\/z3."},{"key":"e_1_3_3_42_2","volume-title":"Communication and Concurrency","author":"Milner Robin","year":"1989","unstructured":"Robin Milner. 1989. Communication and Concurrency. Prentice Hall."},{"key":"e_1_3_3_43_2","volume-title":"Modellierung und Verifikation zeitbehafteter Graphtransformationssysteme mittelsGroove","author":"Neumann Stefan","year":"2007","unstructured":"Stefan Neumann. 2007. Modellierung und Verifikation zeitbehafteter Graphtransformationssysteme mittelsGroove. Master\u2019s Thesis. University of Paderborn."},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810633"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.09.009"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2012-706"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(63)90290-0"},{"key":"e_1_3_3_48_2","unstructured":"RailCab Team. 2023. RailCab Project. Retrieved from https:\/\/www.hni.uni-paderborn.de\/cim\/projekte\/railcab."},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14162-1_26"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51372-6_15"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0496-3"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00585-w"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51372-6_16"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.5555\/239648"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0421-7"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICISE.2009.749"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3572782","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3572782","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:08Z","timestamp":1750182668000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3572782"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,13]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9,30]]}},"alternative-id":["10.1145\/3572782"],"URL":"https:\/\/doi.org\/10.1145\/3572782","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2023,9,13]]},"assertion":[{"value":"2022-01-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-13","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}