{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T08:56:56Z","timestamp":1766048216850},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253334"},{"type":"electronic","value":"9783540319801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_33","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:44:59Z","timestamp":1278888299000},"page":"510-525","source":"Crossref","is-referenced-by-count":3,"title":["Snapshot Verification"],"prefix":"10.1007","author":[{"given":"Blaise","family":"Genest","sequence":"first","affiliation":[]},{"given":"Dietrich","family":"Kuske","sequence":"additional","affiliation":[]},{"given":"Anca","family":"Muscholl","sequence":"additional","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-540-45187-7_3","volume-title":"CONCUR 2003 - Concurrency Theory","author":"R. Alur","year":"2003","unstructured":"Alur, R., Chaudhuri, S., Etessami, K., Guha, S., Yannakakis, M.: Compression of Partially Ordered Strings. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 42\u201356. Springer, Heidelberg (2003)"},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1007\/3-540-48224-5_65","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Realizability and Verification of MSC Graphs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 797\u2013808. Springer, Heidelberg (2001)"},{"issue":"5","key":"33_CR3","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time Temporal Logic. JACM\u00a049(5), 672\u2013713 (2002)","journal-title":"JACM"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BFb0055039","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"1998","unstructured":"Alur, R., McMillan, K., Peled, D.: Deciding Global Partial-Order Properties. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 41\u201352. Springer, Heidelberg (1998)"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Peled, D., Penczek, W.: Model-Checking of Causality Properties. In: LICS 1995, pp. 90\u2013100 (1995)","DOI":"10.1109\/LICS.1995.523247"},{"key":"33_CR6","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/214451.214456","volume":"3","author":"K.M. Chandy","year":"1985","unstructured":"Chandy, K.M., Lamport, L.: Distributed Snapshots: Determining the Global State of Distributed Systems. ACM Transactions on Computer Systems\u00a03, 63\u201375 (1985)","journal-title":"ACM Transactions on Computer Systems"},{"key":"33_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-45653-8_4","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"V. Diekert","year":"2001","unstructured":"Diekert, V., Gastin, P.: Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 55\u201369. Springer, Heidelberg (2001)"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-540-24698-5_27","volume-title":"LATIN 2004: Theoretical Informatics","author":"V. Diekert","year":"2004","unstructured":"Diekert, V., Gastin, P.: Pure Future Local Temporal Logics are Expressively Complete for Mazurkiewicz Traces. In: Farach-Colton, M. (ed.) LATIN 2004. LNCS, vol.\u00a02976, pp. 232\u2013241. Springer, Heidelberg (2004)"},{"key":"33_CR9","doi-asserted-by":"publisher","DOI":"10.1142\/9789814261456","volume-title":"The Book of Traces","author":"V. Diekert","year":"1995","unstructured":"Diekert, V., Rozenberg, G.: The Book of Traces. World Scientific, Singapore (1995)"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of Tree Automata and Logics of Programs. In: FOCS 1988 (1988)","DOI":"10.1109\/SFCS.1988.21949"},{"issue":"3","key":"33_CR11","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1109\/71.277788","volume":"5","author":"V.K. Garg","year":"1994","unstructured":"Garg, V.K., Waldecker, B.: Detecting Weak Unstable Predicates in Distributed Programs. IEEE Transactions on Parallel and Distributed Systems\u00a05(3), 299\u2013307 (1994)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-540-45187-7_15","volume-title":"CONCUR 2003 - Concurrency Theory","author":"P. Gastin","year":"2003","unstructured":"Gastin, P., Kuske, D.: Satisfiability and Model-Checking for MSO-definable Temporal Logics are in PSPACE. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 222\u2013236. Springer, Heidelberg (2003)"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"938","DOI":"10.1007\/3-540-45465-9_80","volume-title":"Automata, Languages and Programming","author":"P. Gastin","year":"2002","unstructured":"Gastin, P., Mukund, M.: An Elementary Expressively Complete Temporal Logic for Mazurkiewicz Traces. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 938\u2013949. Springer, Heidelberg (2002)"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly Automatic Verification of Linear Temporal Logic. In: PSTV 1995, pp. 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/3-540-45995-2_31","volume-title":"LATIN 2002: Theoretical Informatics","author":"B. Genest","year":"2002","unstructured":"Genest, B., Muscholl, A.: Pattern Matching and Membership for Hierarchical Message Sequence Charts. In: Rajsbaum, S. (ed.) LATIN 2002. LNCS, vol.\u00a02286, pp. 326\u2013340. Springer, Heidelberg (2002)"},{"key":"33_CR16","doi-asserted-by":"crossref","unstructured":"Peled, D., Pnueli, A.: Proving Partial Order Liveness Properties. In: ICALP 1990, pp. 553\u2013571 (1990)","DOI":"10.1007\/BFb0032058"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"648","DOI":"10.1007\/3-540-45022-X_55","volume-title":"Automata, Languages and Programming","author":"D. Kuske","year":"2000","unstructured":"Kuske, D.: Infinite Series-parallel Pomsets: Logic and Languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 648\u2013662. Springer, Heidelberg (2000)"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","first-page":"279","volume-title":"Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986","author":"A. Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace semantics. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol.\u00a0255, pp. 279\u2013324. Springer, Heidelberg (1987)"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-45187-7_17","volume-title":"CONCUR 2003 - Concurrency Theory","author":"N. Markey","year":"2003","unstructured":"Markey, N., Schnoebelen, P.: Model-checking a Path. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 251\u2013265. Springer, Heidelberg (2003)"},{"key":"33_CR20","doi-asserted-by":"crossref","unstructured":"Peled, D.: Specification and Verification of Message Sequence Charts. In: FORTE\/PSTV 2000, pp. 139\u2013154 (2000)","DOI":"10.1007\/978-0-387-35533-7_9"},{"key":"33_CR21","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(94)90009-4","volume":"126","author":"D. Peled","year":"1994","unstructured":"Peled, D., Pnueli, A.: Proving Partial Order Properties. Theoretical Computer Science\u00a0126, 143\u2013182 (1994)","journal-title":"Theoretical Computer Science"},{"key":"33_CR22","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-642-60207-8_23","volume-title":"Jewels are Forever","author":"W. Plandowski","year":"1999","unstructured":"Plandowski, W., Rytter, W.: Complexity of Language Recognition Problems for Compressed Words. In: Jewels are Forever, pp. 262\u2013272. Springer, Heidelberg (1999)"},{"key":"33_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/BFb0028758","volume-title":"Computer Aided Verification","author":"S. Stoller","year":"1998","unstructured":"Stoller, S., Liu, Y.A.: Efficient Symbolic Detection of Global Properties in Distributed Systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 357\u2013368. Springer, Heidelberg (1998)"},{"issue":"2","key":"33_CR24","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1006\/inco.2001.2956","volume":"179","author":"P.S. Thiagarajan","year":"2002","unstructured":"Thiagarajan, P.S., Walukiewicz, I.: An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. Information and Computation\u00a0179(2), 230\u2013249 (2002)","journal-title":"Information and Computation"},{"key":"33_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning About Infinite Computations. Information and Computation\u00a0115, 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"33_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/BFb0055048","volume-title":"Automata, Languages and Programming","author":"I. Walukiewicz","year":"1998","unstructured":"Walukiewicz, I.: Difficult Configurations \u2013 On the Complexity of LTrL. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 140\u2013151. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31980-1_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:32:48Z","timestamp":1605760368000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}