{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:03:08Z","timestamp":1776304988492,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540686767","type":"print"},{"value":"9783540686798","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-68679-8_8","type":"book-chapter","created":{"date-parts":[[2008,6,10]],"date-time":"2008-06-10T02:58:16Z","timestamp":1213066696000},"page":"114-132","source":"Crossref","is-referenced-by-count":20,"title":["Explicit State Model Checking for Graph Grammars"],"prefix":"10.1007","author":[{"given":"Arend","family":"Rensink","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-3-540-28644-8_6","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P. Baldan","year":"2004","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B.: Verifying finite-state graph grammars: An unfolding-based approach. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 83\u201398. Springer, Heidelberg (2004)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-71998-4_1","volume-title":"Recent Trends in Algebraic Development Techniques","author":"P. Baldan","year":"2007","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., Schobbens, P.-Y. (eds.) WADT 2006. LNCS, vol.\u00a04409, pp. 1\u201320. Springer, Heidelberg (2007)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-45832-8_4","volume-title":"Graph Transformation","author":"P. Baldan","year":"2002","unstructured":"Baldan, P., K\u00f6nig, B.: Approximating the behaviour of graph transformation systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol.\u00a02505, pp. 14\u201329. Springer, Heidelberg (2002)"},{"issue":"5-6","key":"8_CR4","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1996","unstructured":"Dill, D.L.: The mur\u03c6 verification system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 390\u2013393. Springer, Heidelberg (1996)"},{"issue":"1","key":"8_CR6","first-page":"135","volume":"74","author":"H. Ehrig","year":"2006","unstructured":"Ehrig, H., Ehrig, K., Habel, A., Pennemann, K.H.: Theory of constraints and application conditions: From graphs to high-level structures. Fundam. Inform.\u00a074(1), 135\u2013166 (2006)","journal-title":"Fundam. Inform."},{"issue":"1","key":"8_CR7","first-page":"31","volume":"74","author":"H. Ehrig","year":"2006","unstructured":"Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamental theory for typed attributed graphs and graph transformation based on adhesive HLR categories. Fundam. Inform.\u00a074(1), 31\u201361 (2006)","journal-title":"Fundam. Inform."},{"key":"8_CR8","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, Heidelberg (2006)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-540-24727-2_12","volume-title":"Foundations of Software Science and Computation Structures","author":"H. Ehrig","year":"2004","unstructured":"Ehrig, H., K\u00f6nig, B.: Deriving bisimulation congruences in the dpo approach to graph rewriting. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 151\u2013166. Springer, Heidelberg (2004)"},{"issue":"1","key":"8_CR10","first-page":"1","volume":"74","author":"H. Ehrig","year":"2006","unstructured":"Ehrig, H., Padberg, J., Prange, U., Habel, A.: Adhesive high-level replacement systems: A new categorical framework for graph transformation. Fundam. Inform.\u00a074(1), 1\u201329 (2006)","journal-title":"Fundam. Inform."},{"issue":"1\/2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design\u00a09(1\/2), 105\u2013131 (1996)","journal-title":"Formal Methods in System Design"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Ferreira, A.P.L., Foss, L., Ribeiro, L.: Formal verification of object-oriented graph grammars specifications. In: Rensink, A., Heckel, R., K\u00f6nig, B. (eds.) Graph Transformation for Concurrency and Verification (GT-VC). Electr. Notes Theor. Comput. Sci, vol.\u00a0175, pp. 101\u2013114 (2007)","DOI":"10.1016\/j.entcs.2007.04.020"},{"issue":"3\/4","key":"8_CR13","doi-asserted-by":"crossref","first-page":"287","DOI":"10.3233\/FI-1996-263404","volume":"26","author":"A. Habel","year":"1996","unstructured":"Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Inform.\u00a026(3\/4), 287\u2013313 (1996)","journal-title":"Fundam. Inform."},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/11841883_30","volume-title":"Graph Transformations","author":"A. Habel","year":"2006","unstructured":"Habel, A., Pennemann, K.H.: Satisfiability of high-level conditions. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol.\u00a04178, pp. 430\u2013444. Springer, Heidelberg (2006)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","first-page":"121","volume-title":"CONCUR 2001 - Concurrency Theory","author":"D. Hirsch","year":"2001","unstructured":"Hirsch, D., Montanari, U.: Synchronized hyperedge replacement with name mobility. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 121\u2013136. Springer, Heidelberg (2001)"},{"issue":"5","key":"8_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"8_CR17","unstructured":"Java PathFinder \u2013 A Formal Methods Tool for Java, http:\/\/ase.arc.nasa.gov\/people\/havelund\/jpf.html"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/11768869_15","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"H. Kastenberg","year":"2006","unstructured":"Kastenberg, H., Kleppe, A.G., Rensink, A.: Defining object-oriented execution semantics using graph transformations. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol.\u00a04037, pp. 186\u2013201. Springer, Heidelberg (2006)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/11691372_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. K\u00f6nig","year":"2006","unstructured":"K\u00f6nig, B., Kozioura, V.: Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 197\u2013211. Springer, Heidelberg (2006)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/978-3-540-24727-2_20","volume-title":"Foundations of Software Science and Computation Structures","author":"S. Lack","year":"2004","unstructured":"Lack, S., Sobocinski, P.: Adhesive categories. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 273\u2013288. Springer, Heidelberg (2004)"},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.entcs.2006.01.017","volume":"152","author":"L. Lambers","year":"2006","unstructured":"Lambers, L., Ehrig, H., Orejas, F.: Efficient detection of conflicts in graph-based model transformation. Electr. Notes Theor. Comput. Sci.\u00a0152, 97\u2013109 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"4","key":"8_CR22","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.entcs.2007.04.019","volume":"175","author":"T. Levendovszky","year":"2007","unstructured":"Levendovszky, T., Prange, U., Ehrig, H.: Termination criteria for dpo transformations with injective matches. Electron. Notes Theor. Comput. Sci.\u00a0175(4), 87\u2013100 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"8_CR23","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0304-3975(93)90068-5","volume":"109","author":"M. L\u00f6we","year":"1993","unstructured":"L\u00f6we, M.: Algebraic approach to single-pushout graph transformation. Theoretical Computer Science\u00a0109(1\u20132), 181\u2013224 (1993)","journal-title":"Theoretical Computer Science"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Formal Methods for Mobile Computing","author":"U. Montanari","year":"2005","unstructured":"Montanari, U., Pistore, M.: History-dependent automata: An introduction. In: Bernardo, M., Bogliolo, A. (eds.) SFM-Moby 2005. LNCS, vol.\u00a03465, pp. 1\u201328. Springer, Heidelberg (2005)"},{"key":"8_CR25","unstructured":"Rensink, A.: Towards model checking graph grammars. In: Gruner, S., Presti, S.L., eds.: Workshop on Automated Verification of Critical Systems (AVoCS), Southampton, UK. Volume DSSE-TR-, -02 of Technical Report., University of Southampton (2003) 150\u2013160 (2003)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-540-24725-8_28","volume-title":"Programming Languages and Systems","author":"A. Rensink","year":"2004","unstructured":"Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 401\u2013415. Springer, Heidelberg (2004)"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/978-3-540-25959-6_40","volume-title":"Applications of Graph Transformations with Industrial Relevance","author":"A. Rensink","year":"2004","unstructured":"Rensink, A.: The GROOVE simulator: A tool for state space generation. In: Pfaltz, J.L., Nagl, M., B\u00f6hlen, B. (eds.) AGTIVE 2003. LNCS, vol.\u00a03062, pp. 479\u2013485. Springer, Heidelberg (2004)"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/978-3-540-30203-2_23","volume-title":"Graph Transformations","author":"A. Rensink","year":"2004","unstructured":"Rensink, A.: Representing first-order logic using graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol.\u00a03256, pp. 319\u2013335. Springer, Heidelberg (2004)"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/11817949_8","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"A. Rensink","year":"2006","unstructured":"Rensink, A.: Model checking quantified computation tree logic. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 110\u2013125. Springer, Heidelberg (2006)"},{"key":"8_CR30","unstructured":"Rensink, A.: Isomorphism checking in GROOVE. In: Z\u00fcndorf, A., Varr\u00f3, D. (eds.) Graph-Based Tools (GraBaTs). Electronic Communications of the EASST, European Association of Software Science and Technology, vol.\u00a01, Natal, Brazil (September 2007)"},{"issue":"1","key":"8_CR31","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.entcs.2006.01.022","volume":"157","author":"A. Rensink","year":"2006","unstructured":"Rensink, A., Distefano, D.: Abstract graph transformation. Electr. Notes Theor. Comput. Sci.\u00a0157(1), 39\u201359 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"8_CR32","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1109\/TAIC-PART.2006.5","volume-title":"Testing: Academia and Industry Conference - Practice And Research Techniques (TAIC PART)","author":"D.M.B. Robby","year":"2006","unstructured":"Robby, D.M.B., Hatcliff, J.: Bogor: A flexible framework for creating software model checkers. In: McMinn, P. (ed.) Testing: Academia and Industry Conference - Practice And Research Techniques (TAIC PART), pp. 3\u201322. IEEE Computer Society, Los Alamitos (2006)"},{"key":"8_CR33","series-title":"Foundations","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation","year":"1997","unstructured":"Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation. Foundations, vol.\u00a0I. World Scientific, Singapore (1997)"},{"issue":"3","key":"8_CR34","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S. Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"8_CR35","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s10270-003-0050-x","volume":"3","author":"D. Varr\u00f3","year":"2004","unstructured":"Varr\u00f3, D.: Automated formal verification of visual modeling languages by model checking. Software and System Modeling\u00a03(2), 85\u2013113 (2004)","journal-title":"Software and System Modeling"}],"container-title":["Lecture Notes in Computer Science","Concurrency, Graphs and Models"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68679-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T04:05:48Z","timestamp":1588737948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68679-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540686767","9783540686798"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68679-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}