{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:21:10Z","timestamp":1736400070728,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":62,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540339960"},{"type":"electronic","value":"9783540339977"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11750734_8","type":"book-chapter","created":{"date-parts":[[2006,4,11]],"date-time":"2006-04-11T11:09:15Z","timestamp":1144753755000},"page":"129-142","source":"Crossref","is-referenced-by-count":5,"title":["Implementing Temporal Logics: Tools for Execution and Proof"],"prefix":"10.1007","author":[{"given":"Michael","family":"Fisher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/S0747-7171(89)80070-7","volume":"8","author":"M. Abadi","year":"1989","unstructured":"Abadi, M., Manna, Z.: Temporal Logic Programming. Journal of Symbolic Computation\u00a08, 277\u2013295 (1989)","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(89)90138-2","volume":"64","author":"M. Abadi","year":"1989","unstructured":"Abadi, M.: The Power of Temporal Proofs. Theoretical Computer Science\u00a064, 35\u201384 (1989)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"8_CR3","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/BF01211631","volume":"7","author":"H. Barringer","year":"1995","unstructured":"Barringer, H., Fisher, M., Gabbay, D., Gough, G., Owens, R.: METATEM: An Introduction. Formal Aspects of Computing\u00a07(5), 533\u2013549 (1995)","journal-title":"Formal Aspects of Computing"},{"volume-title":"The Imperative Future: Principles of Executable Temporal Logics","year":"1996","key":"8_CR4","unstructured":"Barringer, H., Fisher, M., Gabbay, D., Owens, R., Reynolds, M. (eds.): The Imperative Future: Principles of Executable Temporal Logics. Research Studies Press, Chichester (1996)"},{"key":"8_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/3-540-36078-6_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Brotherston","year":"2002","unstructured":"Brotherston, J., Degtyarev, A., Fisher, M., Lisitsa, A.: Implementing Invariant Search via Temporal Resolution. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 86\u2013101. Springer, Heidelberg (2002)"},{"key":"8_CR6","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: SymbolicModel Checking: 1020 states and beyond. In: Proceedings of the 5th Symposium on Logic in Computer Science, Philadelphia (June 1990)"},{"key":"8_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: Monodic Temporal Resolution. ACM Transactions on Computational Logic\u00a07(1) (January 2006)","DOI":"10.1145\/1119439.1119443"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-39813-4_15","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Degtyarev","year":"2003","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: Handling equality in monodic temporal resolution. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, pp. 214\u2013228. Springer, Heidelberg (2003)"},{"issue":"2","key":"8_CR10","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1023\/A:1021352309671","volume":"72","author":"A. Degtyarev","year":"2002","unstructured":"Degtyarev, A., Fisher, M., Lisitsa, A.: Equality and Monodic First-Order Temporal Logic. Studia Logica\u00a072(2), 147\u2013156 (2002)","journal-title":"Studia Logica"},{"key":"8_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-45616-3_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Degtyarev","year":"2002","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: A simplified clausal resolution procedure for propositional linear-time temporal logic. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, p. 85. Springer, Heidelberg (2002)"},{"key":"8_CR12","unstructured":"Dixon, C.: Strategies for Temporal Resolution. PhD thesis, Department of Computer Science, University of Manchester, Manchester M13 9PL, U.K. (December 1995)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - Cade-13","author":"C. Dixon","year":"1996","unstructured":"Dixon, C.: Search Strategies for Resolution in Temporal Logics. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104. Springer, Heidelberg (1996)"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1023\/A:1018942108420","volume":"22","author":"C. Dixon","year":"1998","unstructured":"Dixon, C.: Temporal Resolution using a Breadth-First Search Algorithm. Annals of Mathematics and Artificial Intelligence\u00a022, 87\u2013115 (1998)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"8_CR15","volume-title":"Advances in Temporal Logic","author":"C. Dixon","year":"1999","unstructured":"Dixon, C.: Using Otter for Temporal Resolution. In: Advances in Temporal Logic. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Dixon, C.: Using Temporal Logics of Knowledge for Specification and Verification\u2014a Case Study. Journal of Applied Logic, (2005) (to appear)","DOI":"10.1016\/j.jal.2005.08.003"},{"key":"8_CR17","volume-title":"Proceedings of International Symposium on Temporal Representation and Reasoning (TIME)","author":"C. Dixon","year":"2004","unstructured":"Dixon, C., Fern\u00e1ndez Gago, M.-C., Fisher, M., van der Hoek, W.: Using temporal logics of knowledge in the formal verification of security protocols. In: Proceedings of International Symposium on Temporal Representation and Reasoning (TIME). IEEE CS Press, Los Alamitos (2004)"},{"key":"8_CR18","unstructured":"Dixon, C., Fisher, M.: Clausal Resolution for Logics of Time and Knowledge with Synchrony and Perfect Recall. In: Proceedings of Joint International Conference on Temporal Logic and Advances in Modal Logic (AiML-ICTL), Leipzig, Germany (October 2000)"},{"issue":"3","key":"8_CR19","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1093\/logcom\/8.3.345","volume":"8","author":"C. Dixon","year":"1998","unstructured":"Dixon, C., Fisher, M., Wooldridge, M.: Resolution for Temporal Logics of Knowledge. Journal of Logic and Computation\u00a08(3), 345\u2013372 (1998)","journal-title":"Journal of Logic and Computation"},{"key":"8_CR20","first-page":"996","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996\u20131072. Elsevier, Amsterdam (1990)"},{"key":"8_CR21","volume-title":"Proc. Twelfth International Joint Conference on Artificial Intelligence (IJCAI)","author":"M. Fisher","year":"1991","unstructured":"Fisher, M.: A Resolution Method for Temporal Logic. In: Proc. Twelfth International Joint Conference on Artificial Intelligence (IJCAI), Sydney, Australia. Morgan Kaufmann, San Francisco (1991)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"PARLE \u201993 Parallel Architectures and Languages Europe","author":"M. Fisher","year":"1993","unstructured":"Fisher, M.: Concurrent METATEM\u2014A Language for Modeling Reactive Systems. In: Reeve, M., Bode, A., Wolf, G. (eds.) PARLE 1993. LNCS, vol.\u00a0694. Springer, Heidelberg (1993)"},{"key":"8_CR23","volume-title":"Intelligent Agents","author":"M. Fisher","year":"1995","unstructured":"Fisher, M.: Representing and Executing Agent-Based Systems. In: Wooldridge, M., Jennings, N.R. (eds.) Intelligent Agents. Springer, Heidelberg (1995)"},{"issue":"1","key":"8_CR24","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1017\/S0269888900007670","volume":"11","author":"M. Fisher","year":"1996","unstructured":"Fisher, M.: An Introduction to Executable Temporal Logics. Knowledge Engineering Review\u00a011(1), 43\u201356 (1996)","journal-title":"Knowledge Engineering Review"},{"issue":"4","key":"8_CR25","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1093\/logcom\/7.4.429","volume":"7","author":"M. Fisher","year":"1997","unstructured":"Fisher, M.: A Normal Form for Temporal Logic and its Application in Theorem-Proving and Execution. Journal of Logic and Computation\u00a07(4), 429\u2013456 (1997)","journal-title":"Journal of Logic and Computation"},{"key":"8_CR26","volume-title":"Proceedings of International Joint Conference on Artificial Intelligence (IJCAI)","author":"M. Fisher","year":"1997","unstructured":"Fisher, M.: Implementing BDI-like Systems by Direct Execution. In: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, San Francisco (1997)"},{"issue":"1","key":"8_CR27","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s10458-004-3140-4","volume":"10","author":"M. Fisher","year":"2005","unstructured":"Fisher, M.: Temporal Development Methods for Agent-Based Systems. Journal of Autonomous Agents and Multi-Agent Systems\u00a010(1), 41\u201366 (2005)","journal-title":"Journal of Autonomous Agents and Multi-Agent Systems"},{"issue":"1","key":"8_CR28","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M. Fisher","year":"2001","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal Temporal Resolution. ACM Transactions on Computational Logic\u00a02(1), 12\u201356 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"8_CR29","volume-title":"Proceedings of International Joint Conference on Artificial Intelligence (IJCAI)","author":"M. Fisher","year":"1999","unstructured":"Fisher, M., Ghidini, C.: Programming Resource-Bounded Deliberative Agents. In: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, San Francisco (1999)"},{"key":"8_CR30","doi-asserted-by":"publisher","first-page":"849","DOI":"10.1145\/544862.544943","volume-title":"Proc. First International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS)","author":"M. Fisher","year":"2002","unstructured":"Fisher, M., Ghidini, C.: The ABC of Rational Agent Programming. In: Proc. First International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), pp. 849\u2013856. ACM Press, New York ( 2002)"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-540-25930-5_8","volume-title":"Objects, Agents, and Features","author":"M. Fisher","year":"2004","unstructured":"Fisher, M., Ghidini, C., Hirsch, B.: Organising Computation through Dynamic Grouping. In: Ryan, M.D., Meyer, J.-J.C., Ehrich, H.-D. (eds.) Objects, Agents, and Features. LNCS, vol.\u00a02975, pp. 117\u2013136. Springer, Heidelberg (2004)"},{"key":"8_CR32","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"849","DOI":"10.1007\/978-3-540-30200-1_2","volume-title":"Computational Logic in Multi-Agent Systems","author":"M. Fisher","year":"2004","unstructured":"Fisher, M., Ghidini, C., Hirsch, B.: Programming Groups of Rational Agents. In: Dix, J., Leite, J. (eds.) CLIMA 2004. LNCS (LNAI), vol.\u00a03259, pp. 849\u2013856. Springer, Heidelberg (2004)"},{"key":"8_CR33","volume-title":"Proceedings of Twelfth International Symposium on Languages for Intensional Programming (ISLIP)","author":"M. Fisher","year":"1999","unstructured":"Fisher, M., Kakoudakis, T.: Flexible Agent Grouping in Executable Temporal Logic. In: Proceedings of Twelfth International Symposium on Languages for Intensional Programming (ISLIP). World Scientific, Singapore (1999)"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013075","volume-title":"Logic Programming and Automated Reasoning","author":"M. Fisher","year":"1992","unstructured":"Fisher, M., Owens, R.: From the Past to the Future: Executing Temporal Logic Programs. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624. Springer, Heidelberg (1992)"},{"key":"8_CR35","unstructured":"Fern\u00e1ndez Gago, M.-C., Hustadt, U., Dixon, C., Fisher, M., Konev, B.: First-Order Temporal Verification in Practice. Accepted for publication in Journal of Automated Reasoning"},{"key":"8_CR36","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11533092_16","volume-title":"Computational Logic in Multi-Agent Systems","author":"B. Hirsch","year":"2005","unstructured":"Hirsch, B., Fisher, M., Ghidini, C., Busetta, P.: Organising Software in Active Environments. In: Leite, J., Torroni, P. (eds.) CLIMA 2004. LNCS (LNAI), vol.\u00a03487. Springer, Heidelberg (2005)"},{"key":"8_CR37","unstructured":"Hirsch, B.: Programming Rational Agents. PhD thesis, Department of Computer Science, University of Liverpool, United Kingdom (May 2005)"},{"issue":"2","key":"8_CR38","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1023\/A:1021356410579","volume":"72","author":"I. Hodkinson","year":"2002","unstructured":"Hodkinson, I.: Monodic Packed Fragment with Equality is Decidable. Studia Logica\u00a072(2), 185\u2013197 (2002)","journal-title":"Studia Logica"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Hodkinson, I., Wolter, F., Zakharyashev, M.: Decidable fragments of first-order temporal logics. Annals of Pure and Applied Logic (2000)","DOI":"10.1016\/S0168-0072(00)00018-X"},{"key":"8_CR40","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"issue":"5","key":"8_CR41","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. on Software Engineering\u00a023(5), 279\u2013295 (1997); Special issue on Formal Methods in Software Practice","journal-title":"IEEE Trans. on Software Engineering"},{"key":"8_CR42","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-45085-6_21","volume-title":"Automated Deduction \u2013 CADE-19","author":"U. Hustadt","year":"2003","unstructured":"Hustadt, U., Konev, B.: TRP++ 2.0: A temporal resolution prover. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 274\u2013278. Springer, Heidelberg (2003)"},{"key":"8_CR43","first-page":"533","volume-title":"Principles of Knowledge Representation and Reasoning: Proceedings of the Eighth International Conference (KR 2002)","author":"U. Hustadt","year":"2002","unstructured":"Hustadt, U., Schmidt, R.A.: Scientific benchmarking with temporal logic decision procedures. In: Fensel, D., Giunchiglia, F., McGuinness, D., Williams, M.-A. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Eighth International Conference (KR 2002), pp. 533\u2013544. Morgan Kaufmann, San Francisco (2002)"},{"key":"8_CR44","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-25984-8_23","volume-title":"Automated Reasoning","author":"U. Hustadt","year":"2004","unstructured":"Hustadt, U., Konev, B., Riazanov, A., Voronkov, A.: TeMP: A temporal monodic prover. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 326\u2013330. Springer, Heidelberg (2004)"},{"key":"8_CR45","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/11532231_15","volume-title":"Automated Deduction \u2013 CADE-20","author":"U. Hustadt","year":"2005","unstructured":"Hustadt, U., Konev, B., Schmidt, R.A.: Deciding monodic fragments by temporal resolution. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 204\u2013218. Springer, Heidelberg (2005)"},{"key":"8_CR46","unstructured":"Hustadt, U., Schmidt, R.A.: Formulae which highlight differences between temporal logic and dynamic logic provers. In: Giunchiglia, E., Massacci, F. (eds.) Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, Technical Report DII 14\/01, pp. 68\u201376. Dipartimento di Ingegneria dell\u2019Informazione, Unversit\u00e1 degli Studi di Siena (2001)"},{"key":"8_CR47","volume-title":"Logic in Computer Science","author":"M. Huth","year":"2000","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science. Cambridge University Press, Cambridge (2000)"},{"key":"8_CR48","unstructured":"Kellett, A.: Implementation Techniques for Concurrent METATEM. PhD thesis, Department of Computing and Mathematics, Manchester Metropolitan University (2000)"},{"key":"8_CR49","volume-title":"Proceedings of the Fourth International Workshop on Temporal Representation and Reasoning (TIME)","author":"A. Kellett","year":"1997","unstructured":"Kellett, A., Fisher, M.: Automata Representations for Concurrent METATEM. In: Proceedings of the Fourth International Workshop on Temporal Representation and Reasoning (TIME). IEEE Press, Los Alamitos (May 1997)"},{"issue":"1-2","key":"8_CR50","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.ic.2004.10.005","volume":"199","author":"B. Konev","year":"2005","unstructured":"Konev, B., Degtyarev, A., Dixon, C., Fisher, M., Hustadt, U.: Mechanising first-order temporal resolution. Information and Computation\u00a0199(1-2), 55\u201386 (2005)","journal-title":"Information and Computation"},{"key":"8_CR51","unstructured":"Lynch, N.A., Tuttle, M.R.: An Introduction to Input\/Output Automata. Technical Report MIT\/LCS\/TM-373, Laboratory for Computer Science, Massachusetts Institute of Technology (November 1988)"},{"key":"8_CR52","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)"},{"key":"8_CR53","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"8_CR54","unstructured":"Nalon, C., Dixon, C., Fisher, M.: Resolution for Synchrony and No Learning. In: Proceedings of Advances in Modal Logic Confernece (AiML-5), Manchester, UK (September 2004)"},{"key":"8_CR55","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of the Eighteenth Symposium on the Foundations of Computer Science, Providence, USA (November 1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"8_CR56","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001","volume-title":"Past, Present and Future","author":"A. Prior","year":"1967","unstructured":"Prior, A.: Past, Present and Future. Oxford University Press, Oxford (1967)"},{"key":"8_CR57","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45744-5_29","volume-title":"Automated Reasoning","author":"A. Riazanov","year":"2001","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 376\u2013380. Springer, Heidelberg (2001)"},{"issue":"3","key":"8_CR58","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: Complexity of propositional linear temporal logics. ACM Journal\u00a032(3), 733\u2013749 (1985)","journal-title":"ACM Journal"},{"key":"8_CR59","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(88)90045-X","volume":"57","author":"A. Szalas","year":"1988","unstructured":"Szalas, A., Holenderski, L.: Incompleteness of First-Order Temporal Logic with Until. Theoretical Computer Science\u00a057, 317\u2013325 (1988)","journal-title":"Theoretical Computer Science"},{"key":"8_CR60","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-First Search and Linear Graph Algorithms. SIAM Journal on Computing\u00a01, 146\u2013160 (1972)","journal-title":"SIAM Journal on Computing"},{"key":"8_CR61","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: International Conference on Automated Software Engineering (ASE) (September 2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"8_CR62","volume-title":"Reasoning about Rational Agents","author":"M. Wooldridge","year":"2000","unstructured":"Wooldridge, M.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)"}],"container-title":["Lecture Notes in Computer Science","Computational Logic in Multi-Agent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11750734_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,7]],"date-time":"2023-05-07T01:29:36Z","timestamp":1683422976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11750734_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540339960","9783540339977"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/11750734_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}