{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,6]],"date-time":"2025-12-06T04:45:44Z","timestamp":1764996344867,"version":"3.37.3"},"reference-count":84,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:00:00Z","timestamp":1626480000000},"content-version":"vor","delay-in-days":46,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Hasso-Plattner-Institut f\u00fcr Digital Engineering gGmbH"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Embedded real-time systems generate state sequences where time elapses between state changes. Ensuring that such systems adhere to a provided specification of admissible or desired behavior is essential. Formal model-based testing is often a suitable cost-effective approach. We introduce an extended version of the formalism of symbolic graphs, which encompasses types as well as attributes, for representing states of dynamic systems. Relying on this extension of symbolic graphs, we present a novel formalism of timed graph transformation systems (TGTSs) that supports the model-based development of dynamic real-time systems at an abstract level where possible state changes and delays are specified by graph transformation rules. We then introduce an extended form of the <jats:italic>metric temporal graph logic<\/jats:italic> (MTGL) with increased expressiveness to improve the applicability of MTGL for the specification of timed graph sequences generated by a TGTS. Based on the metric temporal operators of MTGL and its built-in graph binding mechanics, we express properties on the structure and attributes of graphs as well as on the occurrence of graphs over time that are related by their inner structure. We provide formal support for checking whether a single generated timed graph sequence adheres to a provided MTGL specification. Relying on this logical foundation, we develop a testing framework for TGTSs that are specified using MTGL. Lastly, we apply this testing framework to a running example by using our prototypical implementation in the tool <jats:sc>AutoGraph<\/jats:sc>.<\/jats:p>","DOI":"10.1007\/s10009-020-00585-w","type":"journal-article","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T18:02:31Z","timestamp":1626544951000},"page":"411-488","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Formal testing of timed graph transformation systems using metric temporal graph logic"],"prefix":"10.1007","volume":"23","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-0001-6971-1589","authenticated-orcid":false,"given":"Lucas","family":"Sakizloglou","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":[[2021,7,17]]},"reference":[{"key":"585_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS \u201990), Philadelphia, Pennsylvania, USA, June 4\u20137, 1990, pp. 414\u2013425. IEEE Computer Society (1990). https:\/\/doi.org\/10.1109\/LICS.1990.113766","DOI":"10.1109\/LICS.1990.113766"},{"key":"585_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Dill, D.L.: The theory of timed automata. In: de\u00a0Bakker, J.W., Huizing, C., de\u00a0Roever, W.P., Rozenberg, G. (eds.) Real-Time: Theory in Practice, REX Workshop, Mook, The Netherlands, June 3\u20137, 1991, Proceedings, Lecture Notes in Computer Science, vol. 600, pp. 45\u201373. Springer (1991). https:\/\/doi.org\/10.1007\/BFb0031987","DOI":"10.1007\/BFb0031987"},{"key":"585_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. In: Logrippo, L. (ed.) Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 19\u201321, 1991, pp. 139\u2013152. ACM (1991). https:\/\/doi.org\/10.1145\/112600.112613","DOI":"10.1145\/112600.112613"},{"issue":"1","key":"585_CR4","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35\u201377 (1993). https:\/\/doi.org\/10.1006\/inco.1993.1025","journal-title":"Inf. Comput."},{"issue":"1","key":"585_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181\u2013204 (1994). https:\/\/doi.org\/10.1145\/174644.174651","journal-title":"J. ACM"},{"issue":"1","key":"585_CR6","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996). https:\/\/doi.org\/10.1145\/227595.227602","journal-title":"J. ACM"},{"key":"585_CR7","doi-asserted-by":"publisher","unstructured":"Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: Advanced concepts and tools for in-place EMF model transformations. In: Petriu, D.C.,\u00a0Rouquette, N.,\u00a0Haugen, \u00d8. (eds.) Model Driven Engineering Languages and Systems\u201413th International Conference, MODELS 2010, Oslo, Norway, October 3\u20138, 2010, Proceedings, Part I, Lecture Notes in Computer Science, vol. 6394, pp. 121\u2013135. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-16145-2_9","DOI":"10.1007\/978-3-642-16145-2_9"},{"key":"585_CR8","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). MIT Press, Cambridge (2008)"},{"key":"585_CR9","doi-asserted-by":"publisher","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B., Lluch-Lafuente, A.: A temporal graph logic for verification of graph transformation systems. In: Fiadeiro, J.L.,\u00a0Schobbens, P. (eds.) Recent Trends in Algebraic Development Techniques, 18th International Workshop, WADT 2006, La Roche en Ardenne, Belgium, June 1\u20133, 2006, Revised Selected Papers, Lecture Notes in Computer Science, vol. 4409, pp. 1\u201320. Springer (2006). https:\/\/doi.org\/10.1007\/978-3-540-71998-4_1","DOI":"10.1007\/978-3-540-71998-4_1"},{"issue":"7","key":"585_CR10","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1016\/j.ic.2008.04.002","volume":"206","author":"P Baldan","year":"2008","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B.: A framework for the verification of infinite-state graph transformation systems. Inf. Comput. 206(7), 869\u2013907 (2008)","journal-title":"Inf. Comput."},{"key":"585_CR11","doi-asserted-by":"publisher","unstructured":"Barkowsky, M., Giese, H.: Hybrid search plan generation for generalized graph pattern matching. In: Guerra, E., Orejas, F. (eds.) Graph Transformation\u201412th International Conference, ICGT 2019, Held as Part of STAF 2019, Eindhoven, The Netherlands, July 15\u201316, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11629, pp. 212\u2013229. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-23611-3_13","DOI":"10.1007\/978-3-030-23611-3_13"},{"key":"585_CR12","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Deshmukh, J.V., Donz\u00e9, A., Fainekos, G.E., Maler, O., Nickovic, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification- Introductory and Advanced Topics. Lecture Notes in Computer Science, vol. 10457. Springer, New York (2018). pp. 135\u2013175. https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5","DOI":"10.1007\/978-3-319-75632-5_5"},{"issue":"2","key":"585_CR13","doi-asserted-by":"publisher","first-page":"15:1","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1\u201315:45 (2015). https:\/\/doi.org\/10.1145\/2699444","journal-title":"J. ACM"},{"issue":"4","key":"585_CR14","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s00236-017-0295-4","volume":"55","author":"DA Basin","year":"2018","unstructured":"Basin, D.A., Klaedtke, F., Zalinescu, E.: Algorithms for monitoring real-time properties. Acta Inf. 55(4), 309\u2013338 (2018). https:\/\/doi.org\/10.1007\/s00236-017-0295-4","journal-title":"Acta Inf."},{"key":"585_CR15","doi-asserted-by":"publisher","unstructured":"Becker, B., Giese, H.: On safe service-oriented real-time coordination for autonomous vehicles. In: 11th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2008), 5\u20137 May 2008, Orlando, Florida, USA, pp. 203\u2013210. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/ISORC.2008.13","DOI":"10.1109\/ISORC.2008.13"},{"key":"585_CR16","doi-asserted-by":"publisher","unstructured":"Beyhl, T., Blouin, D., Giese, H., Lambers, L.: On the operationalization of graph queries with generalized discrimination networks. In: Echahed, R., Minas, M. (eds.) Graph Transformation\u20149th International Conference, ICGT 2016, in Memory of Hartmut Ehrig, Held as Part of STAF 2016, Vienna, Austria, July 5\u20136, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9761, pp. 170\u2013186. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40530-8_11","DOI":"10.1007\/978-3-319-40530-8_11"},{"key":"585_CR17","doi-asserted-by":"publisher","unstructured":"Bi, F., Chang, L., Lin, X., Qin, L., Zhang, W.: Efficient subgraph matching by postponing cartesian products. In: \u00d6zcan, F., Koutrika, G., Madden, S. (eds.) Proceedings of the: International Conference on Management of Data, SIGMOD Conference 2016, San Francisco, CA, USA, June 26\u2013July 01, 2016, pp. 1199\u20131214. ACM (2016). https:\/\/doi.org\/10.1145\/2882903.2915236","DOI":"10.1145\/2882903.2915236"},{"key":"585_CR18","doi-asserted-by":"publisher","unstructured":"Bohnenkamp, H.C., Belinfante, A.: Timed testing with torx. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18\u201322, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3582, pp. 173\u2013188. Springer (2005). https:\/\/doi.org\/10.1007\/11526841_13","DOI":"10.1007\/11526841_13"},{"key":"585_CR19","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Laroussinie, F., Markey, N., Ouaknine, J., Worrell, J.: Timed temporal logics. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools\u2014Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 10460, pp. 211\u2013230. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_11","DOI":"10.1007\/978-3-319-63121-9_11"},{"key":"585_CR20","doi-asserted-by":"publisher","unstructured":"Bozga, M., David, A., Hartmanns, A., Hermanns, H., Larsen, K.G., Legay, A., Tretmans, J.: State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems. In: Rosenstiel, W., Thiele, L. (eds.) 2012 Design, Automation & Test in Europe Conference & Exhibition, DATE 2012, Dresden, Germany, March 12\u201316, 2012, pp. 370\u2013375. IEEE (2012). https:\/\/doi.org\/10.1109\/DATE.2012.6176499","DOI":"10.1109\/DATE.2012.6176499"},{"key":"585_CR21","doi-asserted-by":"publisher","unstructured":"B\u00far, M., Ujhelyi, Z., Horv\u00e1th, \u00c1., Varr\u00f3, D.: Local search-based pattern matching features in emf-incquery. In:\u00a0Parisi-Presicce, F.,\u00a0Westfechtel, B. (eds.) Graph Transformation\u20148th International Conference, ICGT 2015, Held as Part of STAF 2015, L\u2019Aquila, Italy, July 21\u201323, 2015. Proceedings of the Lecture Notes in Computer Science, vol. 9151, pp. 275\u2013282. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21145-9_18","DOI":"10.1007\/978-3-319-21145-9_18"},{"issue":"2","key":"585_CR22","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986). https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"585_CR23","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1142\/9789812384720_0005","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations","author":"B Courcelle","year":"1997","unstructured":"Courcelle, B.: The expression of graph properties and graph transformations in monadic second-order logic. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pp. 313\u2013400. World Scientific, Singapore (1997)"},{"key":"585_CR24","doi-asserted-by":"publisher","unstructured":"Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool KRONOS. In:\u00a0Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) Hybrid Systems III: Verification and Control, Proceedings of the DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems, October 22\u201325, 1995, Ruttgers University, New Brunswick, NJ, USA, Lecture Notes in Computer Science, vol. 1066, pp. 208\u2013219. Springer (1995). https:\/\/doi.org\/10.1007\/BFb0020947","DOI":"10.1007\/BFb0020947"},{"key":"585_CR25","doi-asserted-by":"publisher","unstructured":"de\u00a0Lemos, R., Garlan, D., Ghezzi, C., Giese, H. (eds.): Software Engineering for Self-Adaptive Systems III. Assurances\u2014International Seminar, Dagstuhl Castle, Germany, December 15\u201319, 2013, Revised Selected and Invited Papers, Lecture Notes in Computer Science, vol. 9640. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-74183-3","DOI":"10.1007\/978-3-319-74183-3"},{"key":"585_CR26","doi-asserted-by":"publisher","unstructured":"de\u00a0Lemos, R., Giese, H., M\u00fcller, H.A., Shaw, M. (eds.): Software Engineering for Self-Adaptive Systems II\u2014International Seminar, Dagstuhl Castle, Germany, October 24\u201329, 2010 Revised Selected and Invited Papers, Lecture Notes in Computer Science, vol. 7475. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-35813-5","DOI":"10.1007\/978-3-642-35813-5"},{"key":"585_CR27","doi-asserted-by":"publisher","unstructured":"Dyck, J., Giese, H.: k-inductive invariant checking for graph transformation systems. In: de Lara, J., Plump, D. (eds.): Graph Transformation\u201410th International Conference, ICGT 2017, Held as Part of STAF 2017, Marburg, Germany, July 18\u201319, 2017, Proceedings of the Lecture Notes in Computer Science, vol. 10373. Springer (2017), pp. 142\u2013158. https:\/\/doi.org\/10.1007\/978-3-319-61470-0_9","DOI":"10.1007\/978-3-319-61470-0_9"},{"key":"585_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of Algebraic Specification 1: Equations und Initial Semantics, EATCS Monographs on Theoretical Computer Science","author":"H Ehrig","year":"1985","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1: Equations und Initial Semantics, EATCS Monographs on Theoretical Computer Science, vol. 6. Springer, New York (1985). https:\/\/doi.org\/10.1007\/978-3-642-69962-7"},{"key":"585_CR29","volume-title":"Fundamentals of Algebraic Graph Transformation","author":"H Ehrig","year":"2006","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer, New York (2006)"},{"key":"585_CR30","first-page":"139","volume":"98","author":"H Ehrig","year":"2009","unstructured":"Ehrig, H., Hermann, F., Prange, U.: Cospan DPO approach: an alternative for DPO graph transformations. Bull. EATCS 98, 139\u2013149 (2009)","journal-title":"Bull. EATCS"},{"issue":"1\u20132","key":"585_CR31","doi-asserted-by":"publisher","first-page":"35","DOI":"10.3233\/FI-2012-705","volume":"118","author":"H Ehrig","year":"2012","unstructured":"Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: $$\\cal{M}$$-adhesive transformation systems with nested application conditions. Part 2: embedding, critical pairs and local confluence. Fundam. Inf. 118(1\u20132), 35\u201363 (2012). https:\/\/doi.org\/10.3233\/FI-2012-705","journal-title":"Fundam. Inf."},{"key":"585_CR32","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000357","author":"H Ehrig","year":"2014","unstructured":"Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: $$\\cal{M}$$-adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation. Math. Struct. Comput. Sci. (2014). https:\/\/doi.org\/10.1017\/S0960129512000357","journal-title":"Math. Struct. Comput. Sci."},{"key":"585_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47980-3","volume-title":"Graph and Model Transformation-General Framework and Applications. Monographs in Theoretical Computer Science. An EATCS Series","author":"H Ehrig","year":"2015","unstructured":"Ehrig, H., Ermel, C., Golas, U., Hermann, F.: Graph and Model Transformation-General Framework and Applications. Monographs in Theoretical Computer Science. An EATCS Series. Springer, New York (2015). https:\/\/doi.org\/10.1007\/978-3-662-47980-3"},{"key":"585_CR34","unstructured":"EMF Henshin. http:\/\/www.eclipse.org\/modeling\/emft\/henshin (2013)"},{"issue":"1","key":"585_CR35","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s00165-017-0440-4","volume":"30","author":"M Gerhold","year":"2018","unstructured":"Gerhold, M., Stoelinga, M.: Model-based testing of probabilistic systems. Form. Asp. Comput. 30(1), 77\u2013106 (2018). https:\/\/doi.org\/10.1007\/s00165-017-0440-4","journal-title":"Form. Asp. Comput."},{"issue":"1","key":"585_CR36","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/s10009-011-0186-x","volume":"14","author":"AH Ghamarian","year":"2012","unstructured":"Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using GROOVE. STTT 14(1), 15\u201340 (2012). https:\/\/doi.org\/10.1007\/s10009-011-0186-x","journal-title":"STTT"},{"key":"585_CR37","doi-asserted-by":"publisher","unstructured":"Giese, H., Lambers, L., Becker, B., Hildebrandt, S., Neumann, S., Vogel, T., W\u00e4tzoldt, S.: Graph transformations for mde, adaptation, and models at runtime. In:\u00a0Bernardo, M.,\u00a0Cortellessa, V.,\u00a0Pierantonio, A. (eds.) Formal Methods for Model-Driven Engineering\u201412th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2012, Bertinoro, Italy, June 18\u201323, 2012. Advanced Lectures, Lecture Notes in Computer Science, vol. 7320, pp. 137\u2013191. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-30982-3_5","DOI":"10.1007\/978-3-642-30982-3_5"},{"key":"585_CR38","doi-asserted-by":"publisher","unstructured":"Giese, H., Maximova, M., Sakizloglou, L., Schneider, S.: Metric temporal graph logic over typed attributed graphs. In: H\u00e4hnle, R., van der Aalst,W.M.P. (eds.): Fundamental Approaches to Software Engineering\u201422nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings of the Lecture Notes in Computer Science, vol. 11424. Springer (2019). pp. 282\u2013298. https:\/\/doi.org\/10.1007\/978-3-030-16722-6_16","DOI":"10.1007\/978-3-030-16722-6_16"},{"key":"585_CR39","doi-asserted-by":"publisher","unstructured":"Giese, H.: Modeling and verification of cooperative self-adaptive mechatronic systems. In:\u00a0Kordon, F.,\u00a0Sztipanovits, J. (eds.) Reliable Systems on Unreliable Networked Platforms\u201412th Monterey Workshop 2005, Laguna Beach, CA, USA, September 22\u201324, 2005. Revised Selected Papers, Lecture Notes in Computer Science, vol. 4322, pp. 258\u2013280. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-71156-8_14","DOI":"10.1007\/978-3-540-71156-8_14"},{"key":"585_CR40","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.18.268","author":"H Giese","year":"2009","unstructured":"Giese, H., Hildebrandt, S., Seibel, A.: Improved flexibility and scalability by interpreting story diagrams. ECEASST (2009). https:\/\/doi.org\/10.14279\/tuj.eceasst.18.268","journal-title":"ECEASST"},{"key":"585_CR41","unstructured":"Graphs for Object-Oriented Verification (GROOVE). http:\/\/groove.cs.utwente.nl (2011)"},{"issue":"1","key":"585_CR42","first-page":"1","volume":"58","author":"S Gyapay","year":"2003","unstructured":"Gyapay, S., Varr\u00f3, D., Heckel, R.: Graph transformation with time. Fundam. Inf. 58(1), 1\u201322 (2003)","journal-title":"Fundam. Inf."},{"issue":"2","key":"585_CR43","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1017\/S0960129508007202","volume":"19","author":"A Habel","year":"2009","unstructured":"Habel, A., Pennemann, K.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(2), 245\u2013296 (2009). https:\/\/doi.org\/10.1017\/S0960129508007202","journal-title":"Math. Struct. Comput. Sci."},{"key":"585_CR44","doi-asserted-by":"publisher","unstructured":"Havelund, K., Peled, D.: Efficient runtime verification of first-order temporal properties. In:\u00a0Gallardo, M.,\u00a0Merino, P. (eds.) Model Checking Software\u201425th International Symposium, SPIN 2018, Malaga, Spain, June 20\u201322, 2018, Proceedings of the Lecture Notes in Computer Science, vol. 10869, pp. 26\u201347. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94111-0_2","DOI":"10.1007\/978-3-319-94111-0_2"},{"key":"585_CR45","doi-asserted-by":"publisher","unstructured":"Havelund, K., Reger, G., Thoma, D., Zalinescu, E.: Monitoring events that carry data. In: Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification - Introductory and Advanced Topics. Lecture Notes in Computer Science, vol. 10457. Springer, New York (2018). pp. 61\u2013102. https:\/\/doi.org\/10.1007\/978-3-319-75632-5_3","DOI":"10.1007\/978-3-319-75632-5_3"},{"key":"585_CR46","unstructured":"Heckel, R.: Open graph transformation systems: a new approach to the compositional modelling of concurrent and reactive systems. Ph.D. thesis, Technical University of Berlin, Germany (1998). http:\/\/d-nb.info\/95713598X"},{"key":"585_CR47","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1142\/9789812815149_0016","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation Volume 2: Applications, Languages and Tools","author":"R Heckel","year":"1999","unstructured":"Heckel, R., Engels, G., Ehrig, H., Taentzer, G.: A view-based approach to system modeling based on open graph transformation systems. In: Ehrig, H., Engels, G., Kreowski, H.J., Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformation Volume 2: Applications, Languages and Tools, pp. 639\u2013668. World Scientific, Singapore (1999). https:\/\/doi.org\/10.1142\/9789812815149_0016"},{"issue":"1","key":"585_CR48","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1023\/A:1008734426504","volume":"9","author":"R Heckel","year":"2001","unstructured":"Heckel, R., Ehrig, H., Wolter, U., Corradini, A.: Double-pullback transitions and coalgebraic loose semantics for graph transformation systems. Appl. Categ. Struct. 9(1), 83\u2013110 (2001). https:\/\/doi.org\/10.1023\/A:1008734426504","journal-title":"Appl. Categ. Struct."},{"issue":"4","key":"585_CR49","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1017\/S0960129501003553","volume":"12","author":"R Heckel","year":"2002","unstructured":"Heckel, R., Llabr\u00e9s, M., Ehrig, H., Orejas, F.: Concurrency and loose semantics of open graph transformation systems. Math. Struct. Comput. Sci. 12(4), 349\u2013376 (2002). https:\/\/doi.org\/10.1017\/S0960129501003553","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"585_CR50","first-page":"63","volume":"74","author":"R Heckel","year":"2006","unstructured":"Heckel, R., Lajios, G., Menge, S.: Stochastic graph transformation systems. Fundam. Inf. 74(1), 63\u201384 (2006)","journal-title":"Fundam. Inf."},{"key":"585_CR51","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In:\u00a0Kuich, W. (ed.) Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13\u201317, 1992, Proceedings of the Lecture Notes in Computer Science, vol. 623, pp. 545\u2013558. Springer (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_103","DOI":"10.1007\/3-540-55719-9_103"},{"key":"585_CR52","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Raskin, J., Schobbens, P.: The regular real-time languages. In: Larsen, K.G.,\u00a0Skyum, S.,\u00a0Winskel, G. (eds.) Automata, Languages and Programming, 25th International Colloquium, ICALP\u201998, Aalborg, Denmark, July 13\u201317, 1998, Proceedings of the Lecture Notes in Computer Science, vol. 1443, pp. 580\u2013591. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0055086","DOI":"10.1007\/BFb0055086"},{"key":"585_CR53","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A.: It\u2019s about time: Real-time logics reviewed. In:\u00a0Sangiorgi, D.,.\u00a0de\u00a0Simone, R. (eds.) CONCUR \u201998: Concurrency Theory, 9th International Conference, Nice, France, September 8\u201311, 1998, Proceedings of the Lecture Notes in Computer Science, vol. 1466, pp. 439\u2013454. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0055640","DOI":"10.1007\/BFb0055640"},{"key":"585_CR54","unstructured":"Henzinger, T.A.: The temporal specification and verification of real-time systems. Ph.D. thesis, Standford University, USA (1991)"},{"key":"585_CR55","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.6.49","author":"\u00c1 Horv\u00e1th","year":"2007","unstructured":"Horv\u00e1th, \u00c1., Varr\u00f3, G., Varr\u00f3, D.: Generic search plans for matching advanced graph patterns. ECEASST (2007). https:\/\/doi.org\/10.14279\/tuj.eceasst.6.49","journal-title":"ECEASST"},{"key":"585_CR56","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.scico.2013.10.009","volume":"85","author":"E Jakumeit","year":"2014","unstructured":"Jakumeit, E., Buchwald, S., Wagelaar, D., Dan, L., Heged\u00fcs, \u00c1., Herrmannsd\u00f6rfer, M., Horn, T., Kalnina, E., Krause, C., Lano, K., Lepper, M., Rensink, A., Rose, L.M., W\u00e4tzoldt, S., Mazanek, S.: A survey and comparison of transformation tools based on the transformation tool contest. Sci. Comput. Program. 85, 41\u201399 (2014). https:\/\/doi.org\/10.1016\/j.scico.2013.10.009","journal-title":"Sci. Comput. Program."},{"key":"585_CR57","doi-asserted-by":"publisher","unstructured":"Kang, E., Mu, D., Huang, L.: Probabilistic verification of timing constraints in automotive systems using UPPAAL-SMC. In: Furia, C.A.,\u00a0Winter, K. (eds.) Integrated Formal Methods\u201414th International Conference, IFM 2018, Maynooth, Ireland, September 5\u20137, 2018, Proceedings of the Lecture Notes in Computer Science, vol. 11023, pp. 236\u2013254. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_14","DOI":"10.1007\/978-3-319-98938-9_14"},{"key":"585_CR58","doi-asserted-by":"publisher","unstructured":"Klein, F., Giese, H.: Joint structural and temporal property specification using timed story scenario diagrams. In: Dwyer, M.B.,\u00a0Lopes, A. (eds.) Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, Held as Part of the Joint European Conferences, on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24\u2013April 1, 2007, Proceedings of the Lecture Notes in Computer Science, vol. 4422, pp. 185\u2013199. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-71289-3_16","DOI":"10.1007\/978-3-540-71289-3_16"},{"key":"585_CR59","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/j.entcs.2008.04.042","volume":"211","author":"B K\u00f6nig","year":"2008","unstructured":"K\u00f6nig, B., Kozioura, V.: Augur 2\u2013A new version of a tool for the analysis of graph transformation systems. ENTCS 211, 201\u2013210 (2008). https:\/\/doi.org\/10.1016\/j.entcs.2008.04.042","journal-title":"ENTCS"},{"issue":"4","key":"585_CR60","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255\u2013299 (1990). https:\/\/doi.org\/10.1007\/BF01995674","journal-title":"Real Time Syst."},{"key":"585_CR61","doi-asserted-by":"publisher","unstructured":"Krause, C., Giese, H.: Probabilistic graph transformation systems. In:\u00a0Ehrig, H.,\u00a0Engels, G.,\u00a0Kreowski, H.,\u00a0Rozenberg, G. (eds.) Graph Transformations\u20146th International Conference, ICGT 2012, Bremen, Germany, September 24\u201329, 2012. Proceedings of the Lecture Notes in Computer Science, vol. 7562, pp. 311\u2013325. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33654-6_21","DOI":"10.1007\/978-3-642-33654-6_21"},{"key":"585_CR62","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In:\u00a0Gopalakrishnan, G.,\u00a0Qadeer, S. (eds.) Computer Aided Verification\u201423rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings of the Lecture Notes in Computer Science, vol. 6806, pp. 585\u2013591. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"585_CR63","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. In:\u00a0Lakhnech, Y.,\u00a0Yovine, S. (eds.) 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 of the Lecture Notes in Computer Science, vol. 3253, pp. 293\u2013308. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_21","DOI":"10.1007\/978-3-540-30206-3_21"},{"issue":"7","key":"585_CR64","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"MZ Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027\u20131077 (2007). https:\/\/doi.org\/10.1016\/j.ic.2007.01.004","journal-title":"Inf. Comput."},{"issue":"5","key":"585_CR65","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293\u2013303 (2009). https:\/\/doi.org\/10.1016\/j.jlap.2008.08.004","journal-title":"J. Log. Algebr. Program."},{"key":"585_CR66","doi-asserted-by":"publisher","unstructured":"Maximova, M., Giese, H., Krause, C.: Probabilistic timed graph transformation systems. In: de Lara, J., Plump, D. (eds.): Graph Transformation\u201410th International Conference, ICGT 2017, Held as Part of STAF 2017, Marburg, Germany, July 18\u201319, 2017, Proceedings of the Lecture Notes in Computer Science, vol. 10373. Springer (2017) pp. 159\u2013175. https:\/\/doi.org\/10.1007\/978-3-319-61470-0_10","DOI":"10.1007\/978-3-319-61470-0_10"},{"key":"585_CR67","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.jlamp.2018.09.003","volume":"101","author":"M Maximova","year":"2018","unstructured":"Maximova, M., Giese, H., Krause, C.: Probabilistic timed graph transformation systems. J. Log. Algebr. Meth. Program. 101, 110\u2013131 (2018). https:\/\/doi.org\/10.1016\/j.jlamp.2018.09.003","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"585_CR68","unstructured":"Microsoft Corporation: Z3. https:\/\/github.com\/Z3Prover\/z3"},{"key":"585_CR69","unstructured":"Neumann, S.: Modellierung und Verifikation zeitbehafteter Graphtransformationssysteme mittels Groove. Master\u2019s thesis, University of Paderborn (2007)"},{"key":"585_CR70","doi-asserted-by":"publisher","unstructured":"Orejas, F., Ehrig, H., Prange, U.: A logic of graph constraints. In: Fiadeiro, J.L.,\u00a0Inverardi, P. (eds.) Fundamental Approaches to Software Engineering, 11th International Conference, FASE 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008. Proceedings of the Lecture Notes in Computer Science, vol. 4961, pp. 179\u2013198. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78743-3_14","DOI":"10.1007\/978-3-540-78743-3_14"},{"key":"585_CR71","unstructured":"Orejas, F., Lambers, L.: Symbolic attributed graphs for attributed graph transformation. ECEASST 30 (2010). http:\/\/journal.ub.tu-berlin.de\/index.php\/eceasst\/article\/view\/405"},{"key":"585_CR72","doi-asserted-by":"publisher","unstructured":"Orejas, F.: Attributed graph constraints. In:\u00a0Ehrig, H.,\u00a0Heckel, R.,\u00a0Rozenberg, G.,\u00a0Taentzer, G. (eds.) Graph Transformations, 4th International Conference, ICGT 2008, Leicester, United Kingdom, September 7\u201313, 2008. Proceedings of the Lecture Notes in Computer Science, vol. 5214, pp. 274\u2013288. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-87405-8_19","DOI":"10.1007\/978-3-540-87405-8_19"},{"issue":"3","key":"585_CR73","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1016\/j.jsc.2010.09.009","volume":"46","author":"F Orejas","year":"2011","unstructured":"Orejas, F.: Symbolic graphs for attributed graph constraints. J. Symb. Comput. 46(3), 294\u2013315 (2011). https:\/\/doi.org\/10.1016\/j.jsc.2010.09.009","journal-title":"J. Symb. Comput."},{"issue":"1\u20132","key":"585_CR74","doi-asserted-by":"publisher","first-page":"65","DOI":"10.3233\/FI-2012-706","volume":"118","author":"F Orejas","year":"2012","unstructured":"Orejas, F., Lambers, L.: Lazy graph transformation. Fundam. Inf. 118(1\u20132), 65\u201396 (2012). https:\/\/doi.org\/10.3233\/FI-2012-706","journal-title":"Fundam. Inf."},{"key":"585_CR75","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26\u201329 June 2005, Chicago, IL, USA, pp. 188\u2013197. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/LICS.2005.33","DOI":"10.1109\/LICS.2005.33"},{"key":"585_CR76","unstructured":"Pennemann, K.: Development of correct graph transformation systems. Ph.D. thesis, University of Oldenburg, Germany (2009). http:\/\/oops.uni-oldenburg.de\/884\/"},{"key":"585_CR77","doi-asserted-by":"publisher","unstructured":"Raskin, J., Schobbens, P.: State clock logic: a decidable real-time logic. In:\u00a0Maler, O. (ed.) Hybrid and Real-Time Systems, International Workshop. HART\u201997, Grenoble, France, March 26\u201328, 1997, Proceedings of the Lecture Notes in Computer Science, vol. 1201, pp. 33\u201347. Springer (1997). https:\/\/doi.org\/10.1007\/BFb0014711","DOI":"10.1007\/BFb0014711"},{"key":"585_CR78","doi-asserted-by":"publisher","unstructured":"Rensink, A.: Representing first-order logic using graphs. In:\u00a0Ehrig, H.,\u00a0Engels, G.,\u00a0Parisi-Presicce, F.,\u00a0Rozenberg, G. (eds.) Graph Transformations, Second International Conference, ICGT 2004, Rome, Italy, September 28\u2013October 2, 2004, Proceedings of the Lecture Notes in Computer Science, vol. 3256, pp. 319\u2013335. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30203-2_23","DOI":"10.1007\/978-3-540-30203-2_23"},{"key":"585_CR79","doi-asserted-by":"publisher","unstructured":"Schneider, S., Dyck, J., Giese, H.: Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions. In:\u00a0Gadducci, F.,\u00a0Kehrer, T. (eds.) Graph Transformation\u201413th International Conference, ICGT 2020, Held as Part of STAF 2020, Bergen, Norway, June 25\u201326, 2020, Proceedings of the Lecture Notes in Computer Science, vol. 12150, pp. 257\u2013275. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51372-6_15","DOI":"10.1007\/978-3-030-51372-6_15"},{"key":"585_CR80","doi-asserted-by":"publisher","unstructured":"Schneider, S., Lambers, L., Orejas, F.: A logic-based incremental approach to graph repair. In: H\u00e4hnle, R., van der Aalst,W.M.P. (eds.): Fundamental Approaches to Software Engineering\u201422nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings of the Lecture Notes in Computer Science, vol. 11424. Springer (2019). pp. 151\u2013167. https:\/\/doi.org\/10.1007\/978-3-030-16722-6_9","DOI":"10.1007\/978-3-030-16722-6_9"},{"key":"585_CR81","doi-asserted-by":"publisher","unstructured":"Schneider, S., Sakizloglou, L., Maximova, M., Giese, H.: Optimistic and pessimistic on-the-fly analysis for metric temporal graph logic. In:\u00a0Gadducci, F.,\u00a0Kehrer, T. (eds.) Graph Transformation\u201413th International Conference, ICGT 2020, Held as Part of STAF 2020, Bergen, Norway, June 25\u201326, 2020, Proceedings of the Lecture Notes in Computer Science, vol. 12150, pp. 276\u2013294. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51372-6_16","DOI":"10.1007\/978-3-030-51372-6_16"},{"issue":"6","key":"585_CR82","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1007\/s10009-018-0496-3","volume":"20","author":"S Schneider","year":"2018","unstructured":"Schneider, S., Lambers, L., Orejas, F.: Automated reasoning for attributed graph properties. STTT 20(6), 705\u2013737 (2018). https:\/\/doi.org\/10.1007\/s10009-018-0496-3","journal-title":"STTT"},{"key":"585_CR83","unstructured":"The Attributed Graph Grammar System (AGG). http:\/\/www.user.tu-berlin.de\/o.runge\/agg\/ (2017)"},{"key":"585_CR84","doi-asserted-by":"publisher","unstructured":"Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In:\u00a0Langmaack, H., de\u00a0Roever, W.P.,\u00a0Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems\u2014ProCoS, L\u00fcbeck, Germany, September 19\u201323, Proceedings of the Lecture Notes in Computer Science, vol. 863, pp. 694\u2013715. Springer (1994). https:\/\/doi.org\/10.1007\/3-540-58468-4_191","DOI":"10.1007\/3-540-58468-4_191"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00585-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00585-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00585-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,30]],"date-time":"2021-07-30T08:07:53Z","timestamp":1627632473000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00585-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6]]},"references-count":84,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,6]]}},"alternative-id":["585"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00585-w","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2021,6]]},"assertion":[{"value":"17 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}