{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T09:08:16Z","timestamp":1725527296606},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642008665"},{"type":"electronic","value":"9783642008672"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00867-2_3","type":"book-chapter","created":{"date-parts":[[2009,3,2]],"date-time":"2009-03-02T09:04:21Z","timestamp":1235984661000},"page":"44-56","source":"Crossref","is-referenced-by-count":3,"title":["Temporal Verification of Fault-Tolerant Protocols"],"prefix":"10.1007","author":[{"given":"Michael","family":"Fisher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boris","family":"Konev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexei","family":"Lisitsa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-27813-9_27","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular Model Checking for LTL(MSO). In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 348\u2013360. Springer, Heidelberg (2004)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/11817949_7","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"P.A. Abdulla","year":"2006","unstructured":"Abdulla, P.A., Jonsson, B., Rezine, A., Saksena, M.: Proving Liveness by Backwards Reachability. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 95\u2013109. Springer, Heidelberg (2006)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/3-540-45757-7_9","volume-title":"Logics in Artificial Intelligence","author":"A. Artale","year":"2002","unstructured":"Artale, A., Franconi, E., Wolter, F., Zakharyaschev, M.: A Temporal Description Logic for Reasoning over Conceptual Schemas and Queries. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS, vol.\u00a02424, pp. 98\u2013110. Springer, Heidelberg (2002)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-61474-5_92","volume-title":"Computer Aided Verification","author":"N. Bjorner","year":"1996","unstructured":"Bjorner, N., Browne, A., Chang, E., Colon, M., Kapur, A., Manna, Z., Sipma, H.B., Uribe, T.E.: STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 415\u2013418. Springer, Heidelberg (1996)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Calder, M., Miller, A.: An Automatic Abstraction Technique for Verifying Featured, Parameterised Systems. Theoretical Computer Science (to appear)","DOI":"10.1016\/j.tcs.2008.03.034"},{"key":"3_CR6","first-page":"96","volume-title":"Proc. ICDCS Workshop on Distributed System Validation and Verification","author":"D. Chkliaev","year":"2000","unstructured":"Chkliaev, D., van der Stock, P., Hooman, J.: Mechanical Verification of a Non-Blocking Atomic Commitment Protocol. In: Proc. ICDCS Workshop on Distributed System Validation and Verification, pp. 96\u2013103. IEEE, Los Alamitos (2000)"},{"key":"3_CR7","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"1","key":"3_CR8","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/1119439.1119443","volume":"7","author":"A. Degtyarev","year":"2006","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: Monodic Temporal Resolution. ACM Transactions on Computational Logic\u00a07(1), 108\u2013150 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"3","key":"3_CR9","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G. Delzanno","year":"2003","unstructured":"Delzanno, G.: Constraint-based Verification of Parametrized Cache Coherence Protocols. Formal Methods in System Design\u00a023(3), 257\u2013301 (2003)","journal-title":"Formal Methods in System Design"},{"key":"3_CR10","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)"},{"key":"3_CR11","first-page":"352","volume-title":"Proc. 14th IEEE Symp. Logic in Computer Science (LICS)","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the Verification of Broadcast Protocols. In: Proc. 14th IEEE Symp. Logic in Computer Science (LICS), pp. 352\u2013359. IEEE CS Press, Los Alamitos (1999)"},{"key":"3_CR12","series-title":"NATO Security through Science Series: Information and Communication","volume-title":"Verification of Infinite State Systems and Security","author":"M. Fisher","year":"2006","unstructured":"Fisher, M., Konev, B., Lisitsa, A.: Practical Infinite-state Verification with Temporal Reasoning. In: Verification of Infinite State Systems and Security. NATO Security through Science Series: Information and Communication, vol.\u00a01. IOS Press, Amsterdam (2006)"},{"key":"3_CR13","first-page":"460","volume-title":"Proc. 16th International Florida Artificial Intelligence Research Society Conference (FLAIRS)","author":"D. Gabelaia","year":"2003","unstructured":"Gabelaia, D., Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: On the Computational Complexity of Spatio-Temporal Logics. In: Proc. 16th International Florida Artificial Intelligence Research Society Conference (FLAIRS), pp. 460\u2013464. AAAI Press, Menlo Park (2003)"},{"key":"3_CR14","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I. Hodkinson","year":"2000","unstructured":"Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable Fragments of First-order Temporal Logics. Annals of Pure and Applied Logic\u00a0106, 85\u2013134 (2000)","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","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, vol.\u00a03097, pp. 326\u2013330. Springer, Heidelberg (2004)"},{"issue":"1-2","key":"3_CR17","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":"3_CR18","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Propositional Temporal Logics: Decidability and Completeness. International Journal of the IGPL\u00a08, 55\u201385","DOI":"10.1093\/jigpal\/8.1.55"},{"key":"3_CR19","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)"},{"key":"3_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering\u00a021, 107\u2013122","DOI":"10.1109\/32.345827"},{"key":"3_CR22","unstructured":"R\u00f6ckl, C.: Proving write invalidate cache coherence with bisimulations in Isabelle\/HOL. In: In Proc. of FBT 2000, Shaker, pp. 69\u201378 (2000)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"598","DOI":"10.1007\/978-3-540-39910-0_26","volume-title":"Verification: Theory and Practice","author":"A. Pnueli","year":"2004","unstructured":"Pnueli, A., Arons, T.: TLPVS: A PVS-based LTL verification system. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 598\u2013625. Springer, Heidelberg (2004)"},{"issue":"1-2","key":"3_CR24","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(1-2), 133\u2013145 (2002)","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Lecture Notes in Computer Science","Methods, Models and Tools for Fault Tolerance"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00867-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T06:31:05Z","timestamp":1558161065000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00867-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642008665","9783642008672"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00867-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}