{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T20:10:34Z","timestamp":1740341434708,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540220947"},{"type":"electronic","value":"9783540247739"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24773-9_8","type":"book-chapter","created":{"date-parts":[[2010,8,4]],"date-time":"2010-08-04T04:08:27Z","timestamp":1280894907000},"page":"95-110","source":"Crossref","is-referenced-by-count":2,"title":["Monodic ASMs and Temporal Verification"],"prefix":"10.1007","author":[{"given":"Michael","family":"Fisher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexei","family":"Lisitsa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Abstract State Machines: A Formal Method for Specification and Verification, http:\/\/www.eecs.umich.edu\/gasm\/"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Blass, A., Gurevich, Y.: Abstract State Machines Capture Parallel Algorithms. ACM Transactions on Computational Logic\u00a04(4) (October 2003)","DOI":"10.1145\/937555.937561"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48257-1_1","volume-title":"Applied Formal Methods - FM-Trends 98","author":"E. B\u00f6rger","year":"1999","unstructured":"B\u00f6rger, E.: High Level System Design and Analysis using Abstract State Machines. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol.\u00a01641, pp. 1\u201343. Springer, Heidelberg (1999)"},{"key":"8_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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, Springer, Heidelberg (2002)"},{"key":"8_CR5","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking, Dec. 1999. MIT Press, Cambridge (1999)"},{"key":"8_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-45422-5_3","volume-title":"KI 2001: Advances in Artificial Intelligence","author":"A. Degtyarev","year":"2001","unstructured":"Degtyarev, A., Fisher, M.: Towards First-Order Temporal Resolution. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI 2001. LNCS (LNAI), vol.\u00a02174, pp. 18\u201332. Springer, Heidelberg (2001)"},{"key":"8_CR7","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-19","author":"A. Degtyarev","year":"2003","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, Springer, Heidelberg (2003)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Fisher, M., Lisitsa, A.: Equality and Monodic First-Order Temporal Logic. Studia Logica\u00a0(72), 147\u2013156 (2002)","DOI":"10.1023\/A:1021352309671"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-46419-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Castillo Del","year":"2000","unstructured":"Del Castillo, G., Winter, K.: Model Checking Support for the ASM High-Level Language. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 331\u2013346. Springer, Heidelberg (2000)"},{"key":"8_CR10","unstructured":"Delzanno, G.: Constraint-based verification in Parametrized Cache Coherence Protocols. To appear in Formal Methods in System Design"},{"key":"8_CR11","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: Handbook of Theoretical Computer Science, pp. 996\u20131072. Elsevier, Amsterdam (1990)"},{"issue":"1","key":"8_CR12","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":"Computational Logic"},{"key":"8_CR13","unstructured":"Fisher, M., Lisitsa, A.: Deductive Verification of Cache Coherence Protocols. In: Proceedings of the 3rd Workshop on Automated Verification of Critical Systems AVoCS 2003, Southampton, UK, April 2003, pp. 177\u2013186 (2003)"},{"key":"8_CR14","unstructured":"Fisher, M., Lisitsa, A.: Temporal Verification of Monodic Abstract State Machines Technical Report ULCS-03-011, University of Liverpool Department of Computer Science (April 2003), available at http:\/\/www.csc.liv.ac.uk\/research\/techreports"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/3-540-44518-8_17","volume-title":"Abstract State Machines - Theory and Applications","author":"A. Gargantini","year":"2000","unstructured":"Gargantini, A., Riccobene, E.: Encoding Abstract State Machines in PVS. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol.\u00a01912, pp. 303\u2013322. Springer, Heidelberg (2000)"},{"key":"8_CR16","first-page":"9","volume-title":"Specification and Validation Methods","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: Specification and Validation Methods, pp. 9\u201336. Oxford University Press, Oxford (1995)"},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/343369.343384","volume":"1","author":"Y. Gurevich","year":"2000","unstructured":"Gurevich, Y.: Sequential Abstract State Machines Capture Sequential Algorithms. ACM Transactions on Computational Logic\u00a01(1), 77\u2013111 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1109\/LICS.2001.932489","volume-title":"Proc. 16th Annual IEEE Symposium on Logic in Computer Science (LICS)","author":"Y. Gurevich","year":"2001","unstructured":"Gurevich, Y.: Logician in the land of OS: Abstract State Machines at Microsoft. In: Proc. 16th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 129\u2013136. IEEE Computer Society, Los Alamitos (2001)"},{"key":"8_CR19","unstructured":"Gl\u00e4sser, U., Gurevich, Y., Veanes, M.: Universal Plug and Play Models. Technical Report MSR-TR-2001-59, Microsoft Research (June 2001)"},{"key":"8_CR20","unstructured":"Gurevich, Y., Schulte, W., Veanes, M.: Toward Industrial Strength Abstract State Machines. Technical Report MSR-TR-2001-98, Microsoft Research (October 2001)"},{"key":"8_CR21","volume-title":"The Cache memory Book","author":"J. Handy","year":"1993","unstructured":"Handy, J.: The Cache memory Book. Academic Press, London (1993)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Hodkinson, I.: Monodic Packed Fragment with Equality is Decidable. Studia Logica\u00a0(72), 185\u2013197 (2002)","DOI":"10.1023\/A:1021356410579"},{"key":"8_CR23","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_CR24","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_CR25","unstructured":"Hustadt, U., Schmidt, R.A.: Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers. In: 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_CR26","first-page":"533","volume-title":"Proc. KR 2002","author":"U. Hustadt","year":"2002","unstructured":"Hustadt, U., Schmidt, R.A.: Scientific Benchmarking with Temporal Logic Decision Procedures. In: Proc. KR 2002, pp. 533\u2013544. Morgan Kaufmann, San Francisco (2002)"},{"key":"8_CR27","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_CR28","volume-title":"Proceedings of TIMEICTL 2003","author":"B. Konev","year":"2003","unstructured":"Konev, B., Degtyarev, A., Dixon, C., Fisher, M., Hustadt, U.: Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case. In: Proceedings of TIMEICTL 2003, Cairns, Queensland, Australia, July 2003, IEEE CS Press, Los Alamitos (2003)"},{"key":"8_CR29","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann Publishers, San Mateo (1996)"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"Z. Manna","year":"1996","unstructured":"Manna, Z., The STeP group: Step: Deductive\u2013algorithmic verification of reactive and realtime systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"8_CR31","doi-asserted-by":"crossref","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_CR32","doi-asserted-by":"crossref","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_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-36498-6_20","volume-title":"Abstract State Machines 2003. Advances in Theory and Practice","author":"A. Nowack","year":"2003","unstructured":"Nowack, A.: Deciding the Verification Problem for Abstract State Machines. In: B\u00f6rger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol.\u00a02589, pp. 341\u2013371. Springer, Heidelberg (2003)"},{"key":"8_CR34","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1016\/B978-0-12-450010-5.50026-8","volume-title":"AI and Mathematical Theory of Computation: Papers in Honor of John McCarthy","author":"R. Reiter","year":"1991","unstructured":"Reiter, R.: The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression. In: AI and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 359\u2013380. Academic Press, London (1991)"},{"key":"8_CR35","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BFb0054254","volume-title":"Automated Deduction - CADE-15","author":"J. Richardson","year":"1998","unstructured":"Richardson, J., Smaill, A., Green, I.: System description: Proof planning in higher-order logic with \u03bbclam. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 129\u2013131. Springer, Heidelberg (1998)"},{"issue":"4","key":"8_CR36","first-page":"377","volume":"3","author":"G. Schellhorn","year":"1997","unstructured":"Schellhorn, G., Ahrendt, W.: Reasoning about Abstract State Machines: The WAM Case Study. Journal of Universal Computer Science\u00a03(4), 377\u2013413 (1997)","journal-title":"Journal of Universal Computer Science"},{"issue":"3","key":"8_CR37","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"P. Sistla","year":"1985","unstructured":"Sistla, P., Clarke, E.M.: Complexity of Propositional Linear Temporal Logics. ACM Journal\u00a032(3), 733\u2013749 (1985)","journal-title":"ACM Journal"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-44518-8_18","volume-title":"Abstract State Machines - Theory and Applications","author":"M. Spielmann","year":"2000","unstructured":"Spielmann, M.: Model Checking Abstract StateMachines and Beyond. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol.\u00a01912, pp. 323\u2013340. Springer, Heidelberg (2000)"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-44518-8_19","volume-title":"Abstract State Machines - Theory and Applications","author":"K. Winter","year":"2000","unstructured":"Winter, K.: Towards a Methodology for Model Checking ASM: Lessons Learned from the FLASH Case Study. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol.\u00a01912, pp. 341\u2013360. Springer, Heidelberg (2000)"},{"key":"8_CR40","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5804.001.0001","volume-title":"Reasoning about Rational Agents","author":"M. Wooldridge","year":"2000","unstructured":"Wooldridge, M.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)"},{"key":"8_CR41","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0168-0072(01)00124-5","volume":"118","author":"F. Wolter","year":"2002","unstructured":"Wolter, F., Zakharyaschev, M.: Axiomatizing the Monodic Fragment of First-Order Temporal Logic. Annals of Pure and Applied logic\u00a0118, 133\u2013145 (2002)","journal-title":"Annals of Pure and Applied logic"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines 2004. Advances in Theory and Practice"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24773-9_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T19:42:13Z","timestamp":1740339733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24773-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540220947","9783540247739"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24773-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}