{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,22]],"date-time":"2026-06-22T19:38:13Z","timestamp":1782157093423,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540373766","type":"print"},{"value":"9783540373773","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817949_8","type":"book-chapter","created":{"date-parts":[[2006,8,2]],"date-time":"2006-08-02T19:59:29Z","timestamp":1154548769000},"page":"110-125","source":"Crossref","is-referenced-by-count":16,"title":["Model Checking Quantified Computation Tree Logic"],"prefix":"10.1007","author":[{"given":"Arend","family":"Rensink","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B., LLuch Lafuente, A.: A temporal graph logic for abstractions of graph rewrite systems. Draft (2005)"},{"issue":"3","key":"8_CR2","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1008278803780","volume":"7","author":"D.A. Basin","year":"1998","unstructured":"Basin, D.A., Matthews, S., Vigano, L.: Labelled modal logics: Quantifiers. Journal of Logic, Language and Information\u00a07(3), 237\u2013263 (1998)","journal-title":"Journal of Logic, Language and Information"},{"key":"8_CR3","unstructured":"Bojanczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on words with data. Research Report 2005-004, LIAFA \u2014 Laboratoire d\u2019Informatique Algorithmique: Fondements et Applications (2005)"},{"key":"8_CR4","unstructured":"Castellini, C., Smaill, A.: A modular, tactic-based approach for first-order temporal theorem proving. In: International Conference on Temporal Logic (ICTL) (2000)"},{"key":"8_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/11532231_17","volume-title":"Automated Deduction \u2013 CADE-20","author":"C. Castellini","year":"2005","unstructured":"Castellini, C., Smaill, A.: Proof planning for first-order temporal logic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 235\u2013249. Springer, Heidelberg (2005)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"8_CR7","first-page":"117","volume-title":"Symposium on Principles of Programming Languages (POPL)","author":"E.M. Clarke","year":"1983","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In: Symposium on Principles of Programming Languages (POPL), pp. 117\u2013126. ACM Press, New York (1983)"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/s100090200075","volume":"4","author":"J.C. Corbett","year":"2002","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby: Expressing checkable properties of dynamic systems: the bandera specification language. International Journal on Software Tools for Technology\u00a04(1), 34\u201356 (2002)","journal-title":"International Journal on Software Tools for Technology"},{"issue":"1","key":"8_CR9","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"Dam, M.: CTL\u22c6 and ECTL\u22c6 as fragments of the modal \u03bc-calculus. Theoretical Comput. Sci.\u00a0126(1), 77\u201396 (1994)","journal-title":"Theoretical Comput. Sci."},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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? on the automated verification of linked list structures. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 250\u2013262. Springer, Heidelberg (2004)"},{"key":"8_CR11","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/978-0-387-35608-2_36","volume-title":"Foundations of Information Technology in the Era of Network and Mobile Computing","author":"D. Distefano","year":"2002","unstructured":"Distefano, D., Rensink, A., Katoen, J.-P.: Model checking birth and death. In: Baeza-Yates, Montanari, Santoro (eds.) Foundations of Information Technology in the Era of Network and Mobile Computing. IFIP Conference Proceedings, vol.\u00a0223, pp. 435\u2013447. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"8_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/BFb0055899","volume-title":"Artificial Intelligence and Symbolic Computation","author":"M. Fitting","year":"1998","unstructured":"Fitting, M.: Bertrand Russell, Herbrand\u2019s Theorem, and the Assignment Statement. In: Calmet, J., Plaza, J. (eds.) AISC 1998. LNCS (LNAI), vol.\u00a01476, p. 14. Springer, Heidelberg (1998)"},{"issue":"1","key":"8_CR13","first-page":"5","volume":"39","author":"M. Fitting","year":"1999","unstructured":"Fitting, M.: On quantified modal logic. Fundamenta Informaticae\u00a039(1), 5\u2013121 (1999)","journal-title":"Fundamenta Informaticae"},{"key":"8_CR14","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-94-017-0454-0_3","volume-title":"Handbook of Philosophical Logic","author":"J.W. Garson","year":"2001","unstructured":"Garson, J.W.: Quantification in modal logic. In: Guenthner, F., Gabbay, D. (eds.) Handbook of Philosophical Logic, 2nd edn., vol.\u00a03, pp. 267\u2013323. Kluwer, Dordrecht (2001)","edition":"2"},{"key":"8_CR15","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holtzmann","year":"2003","unstructured":"Holtzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"8_CR16","unstructured":"Montanari, U., Pistore, M.: History-dependent automata. Technical Report TR-11-98, Department of Computer Science, University of Pisa (1998)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11419822_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_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1007\/3-540-44683-4_49","volume-title":"Mathematical Foundations of Computer Science 2001","author":"F. Neven","year":"2001","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Towards regular languages over infinite alphabets. In: Sgall, J., Pultr, A., Kolman, P. (eds.) MFCS 2001. LNCS, vol.\u00a02136, pp. 560\u2013572. Springer, Heidelberg (2001)"},{"key":"8_CR19","unstructured":"Rensink, A.: Towards model checking graph grammars. In: Leuschel, Gruner, Presti, (eds.), Workshop on Automated Verification of Critical Systems (AVoCS), Technical Report DSSE\u2013TR\u20132003\u20132, pp. 150\u2013160. University of Southampton (2003)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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_CR21","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. LNCS, vol.\u00a02618, pp. 204\u2013222. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2006 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817949_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:29:57Z","timestamp":1619508597000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817949_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540373766","9783540373773"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11817949_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}