{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,6]],"date-time":"2025-12-06T04:34:52Z","timestamp":1764995692605},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540719977"},{"type":"electronic","value":"9783540719984"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71998-4_1","type":"book-chapter","created":{"date-parts":[[2007,6,19]],"date-time":"2007-06-19T22:07:11Z","timestamp":1182290831000},"page":"1-20","source":"Crossref","is-referenced-by-count":18,"title":["A Temporal Graph Logic for Verification of Graph Transformation Systems"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Corradini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"K\u00f6nig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Lluch Lafuente","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Baldan","year":"2001","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B.: A static analysis technique for graph transformation systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, Springer, Heidelberg (2001)"},{"key":"1_CR2","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":"1_CR3","series-title":"ENTCS","first-page":"5","volume-title":"Proc. of COMETA\u201903","author":"P. Baldan","year":"2004","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B., K\u00f6nig, B.: Verifying a behavioural logic for graph transformation systems. In: Proc. of COMETA\u201903. ENTCS, vol.\u00a0104, pp. 5\u201324. Elsevier, Amsterdam (2004)"},{"key":"1_CR4","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)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-44898-5_14","volume-title":"Static Analysis","author":"P. Baldan","year":"2003","unstructured":"Baldan, P., K\u00f6nig, B., K\u00f6nig, B.: A logic for analyzing abstractions of graph transformation systems. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 255\u2013272. Springer, Heidelberg (2003)"},{"key":"1_CR6","volume-title":"Handbook of Process Algebra","author":"J. Bradfield","year":"2001","unstructured":"Bradfield, J., Stirling, C.: Modal logics and mu-calculi: an introduction. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, Elsevier, Amsterdam (2001)"},{"key":"1_CR7","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1","author":"A. Corradini","year":"1997","unstructured":"Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., L\u00f6we, M.: Algebraic Approaches to Graph Transformation I: Basic Concepts and Double Pushout Approach. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1, World Scientific, Singapore (1997)"},{"key":"1_CR8","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1142\/9789812384720_0005","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1","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 Transformation: Foundations, vol. 1, pp. 313\u2013400. World Scientific, Singapore (1997)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/978-3-540-30538-5_21","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"D. Distefano","year":"2004","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: Who is pointing when to whom? In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 250\u2013262. Springer, Heidelberg (2004)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/978-3-540-39958-2_18","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"F. Dotti","year":"2003","unstructured":"Dotti, F., Foss, L., Ribeiro, L., Santos, O.M.: Verification of distributed object-based systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 261\u2013275. Springer, Heidelberg (2003)"},{"key":"1_CR11","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1","author":"H. Ehrig","year":"1997","unstructured":"Ehrig, H., Heckel, R., Korff, M., L\u00f6we, M., Ribeiro, L., Wagner, A., Corradini, A.: Algebraic Approaches to Graph Transformation II: Single Pushout Approach and Comparison with Double Pushout Approach. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1, World Scientific, Singapore (1997)"},{"issue":"3","key":"1_CR12","first-page":"143","volume":"30","author":"J. Esparza","year":"1994","unstructured":"Esparza, J., Nielsen, M.: Decidability issues for Petri nets - a survey. Journal of Information Processing and Cybernetic\u00a030(3), 143\u2013160 (1994)","journal-title":"Journal of Information Processing and Cybernetic"},{"key":"1_CR13","unstructured":"Franconi, E., Toman, D.: Fixpoint extensions of temporal description logics. In: Proc. of the International Workshop on Description Logics (DL2003), vol.\u00a081 of CEUR Workshop Proceedings (2003)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1007\/978-3-540-46464-8_22","volume-title":"Theory and Application of Graph Transformations","author":"F. Gadducci","year":"2000","unstructured":"Gadducci, F., Heckel, R., Koch, M.: A fully abstract model for graph intepreted temporal logic. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) TAGT 1998. LNCS, vol.\u00a01764, pp. 310\u2013322. Springer, Heidelberg (2000)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Gro\u00dfe-Rhode, M.: Algebra transformation systems as a unifying framework. Electronic Notes in Theoretical Computer Science\u00a051 (2001)","DOI":"10.1016\/S1571-0661(04)80199-3"},{"key":"1_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45653-8_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"I. Hodkinson","year":"2001","unstructured":"Hodkinson, I., Wolter, F., Zakharyaschev, M.: Monadic fragments of first-order temporal logics: 2000-2001 a.d. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 1\u201323. Springer, Heidelberg (2001)"},{"key":"1_CR17","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/0304-3975(91)90228-T","volume":"82","author":"R.R. Howell","year":"1991","unstructured":"Howell, R.R., Rosier, L.E., Yen, H.-C.: A taxonomy of fairness and temporal logic problems for Petri nets. Theoretical Computer Science\u00a082, 341\u2013372 (1991)","journal-title":"Theoretical Computer Science"},{"key":"1_CR18","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 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 197\u2013211. Springer, Heidelberg (2006)"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Grafa, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design\u00a06, 1\u201335 (1995)","journal-title":"Formal Methods in System Design"},{"key":"1_CR20","unstructured":"Rensink, A.: Towards model checking graph grammars. In: Proc. of the 3rd Workshop on Automated Verification of Critical Systems, Technical Report DSSE\u2013TR\u20132003\u20132, pp. 150\u2013160. University of Southampton (2003)"},{"key":"1_CR21","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":"1_CR22","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)"},{"volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1","year":"1997","key":"1_CR23","unstructured":"Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1. World Scientific, Singapore (1997)"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Schmidt, K.: Model-checking with coverability graphs. Formal Methods in System Design\u00a015(3) (1999)","DOI":"10.1023\/A:1008753219837"},{"issue":"2","key":"1_CR25","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s10270-003-0050-x","volume":"3","author":"D. Varr\u00f3","year":"2004","unstructured":"D.\u00a0Varr\u00f3. Automated formal verification of visual modeling languages by model checking. Software and System Modeling, 3(2):85\u2013113, 2004.","journal-title":"Software and System Modeling"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-36575-3_15","volume-title":"Programming Languages and Systems","author":"E. Yahav","year":"2003","unstructured":"Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, pp. 204\u2013222. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71998-4_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:27:52Z","timestamp":1605763672000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71998-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540719977","9783540719984"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71998-4_1","relation":{},"subject":[]}}