{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T07:46:06Z","timestamp":1766043966976,"version":"3.48.0"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032054340"},{"type":"electronic","value":"9783032054357"}],"license":[{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-05435-7_15","type":"book-chapter","created":{"date-parts":[[2025,9,13]],"date-time":"2025-09-13T01:30:24Z","timestamp":1757727024000},"page":"252-273","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Monitoring Distributed Systems Based on\u00a0Partial Order Executions with\u00a0Global States"],"prefix":"10.1007","author":[{"given":"Moran","family":"Omer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ely","family":"Porat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vijay K.","family":"Garg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,12]]},"reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s10703-005-4592-0","volume":"26","author":"R Alur","year":"2005","unstructured":"Alur, R., McMillan, K., Peled, D.: Deciding global partial-order properties. Formal Methods Syst. Des. 26(1), 7\u201325 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Peled, D., Penczek, W.: Model-checking of causality properties. In: LICS 1995, San Diego, CA, pp. 90-100","DOI":"10.1109\/LICS.1995.523247"},{"issue":"3","key":"15_CR3","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0020-0190(99)00005-8","volume":"69","author":"R Alur","year":"1999","unstructured":"Alur, R., Peled, D.: Undecidability of partial order logics. Inf. Process. Lett. 69(3), 137\u2013143 (1999)","journal-title":"Inf. Process. Lett."},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"111251","DOI":"10.1016\/j.jss.2022.111251","volume":"187","author":"G Audrito","year":"2022","unstructured":"Audrito, G., Damiani, F., Stolz, V., Torta, G., Viroli, M.: Distributed runtime verification by past-CTL and the field calculus. J. Syst. Softw. 187, 111251 (2022)","journal-title":"J. Syst. Softw."},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5","volume-title":"Lectures on Runtime Verification \u2013 Introductory and Advanced Topics","year":"2018","unstructured":"Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification \u2013 Introductory and Advanced Topics. LNCS, vol. 10457. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"Runtime Verification","author":"A Bauer","year":"2007","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126\u2013138. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77395-5_11"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/S0169-023X(02)00136-2","volume":"44","author":"B Bollig","year":"2003","unstructured":"Bollig, B., Leucker, M.: Deciding LTL over Mazurkiewicz traces. Data Knowl. Eng. 44(2), 219\u2013238 (2003)","journal-title":"Data Knowl. Eng."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Henzinger, T.A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. Logical Methods Comput. Sci. 11(1) (2015)","DOI":"10.2168\/LMCS-11(1:20)2015"},{"key":"15_CR9","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/214451.214456","volume":"3","author":"KM Chandy","year":"1985","unstructured":"Chandy, K.M., Lamport, L.: Distributed snapshots: determining the global state of distributed systems. ACM Trans. Comput. Syst. 3, 63\u201375 (1985)","journal-title":"ACM Trans. Comput. Syst."},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s004460050049","volume":"11","author":"CM Chase","year":"1998","unstructured":"Chase, C.M., Garg, V.K.: Detection of global predicates: techniques and their limitations. Distrib. Comput. 11, 191\u2013201 (1998)","journal-title":"Distrib. Comput."},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM 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. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"84091","DOI":"10.1109\/ACCESS.2023.3298329","volume":"11","author":"LM Danielsson","year":"2023","unstructured":"Danielsson, L.M., Sa\u0144chez, C.: Decentralized stream runtime verification for timed asynchronous networks. IEEE Access 11, 84091\u201384112 (2023)","journal-title":"IEEE Access"},{"key":"15_CR13","unstructured":"Dominguez, J., Nanevski, A.: Visibility and separability for a declarative linearizability proof of the timestamped stack. In: CONCUR 2023, pp. 1\u201316 (2023)"},{"key":"15_CR14","unstructured":"Fidge, C.: Timestamps in message-passing systems that preserve the partial ordering. In: Raymond, K. (ed.) Proceedings of the 11th Australian Computer Science Conference (ACSC\u201988), vol. 10, pp. 56\u201366 (1987)"},{"key":"15_CR15","first-page":"1","volume":"20","author":"R Ganguly","year":"2020","unstructured":"Ganguly, R., Momtaz, A., Bonakdarpour, B.: Distributed runtime verification under partial synchrony. OPODIS 20, 1\u201317 (2020)","journal-title":"OPODIS"},{"key":"15_CR16","unstructured":"Garg, V.K.: Elements of Distributed Computing. Wiley (2002)"},{"issue":"5\u20136","key":"15_CR17","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s00446-006-0018-5","volume":"19","author":"VK Garg","year":"2007","unstructured":"Garg, V.K., Skawratananond, Ch., Mittal, N.: Timestamping messages and events in a distributed system using synchronous communication. Distrib. Comput. 19(5\u20136), 387\u2013402 (2007)","journal-title":"Distrib. Comput."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Genest, B., Kuske, D., Muscholl, A., Peled, D.: Snapshot verification. In: TACAS 2005. LNCS, vol. 3440, pp. 510\u2013525. Springer, Verlag (2005)","DOI":"10.1007\/978-3-540-31980-1_33"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201902). LNCS, vol. 2280, pp. 342\u2013356. Springer, Verlag (2002)","DOI":"10.1007\/3-540-46002-0_24"},{"issue":"3","key":"15_CR21","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Jard, C., Jourdan, G.V., Jeron, T., Rampon, J.X.: A general approach to trace-checking in distributed computing systems. In: 14th International Conference on Distributed Computing Systems, Pozman, Poland, pp. 396\u2013403 (1994)","DOI":"10.1109\/ICDCS.1994.302443"},{"issue":"3","key":"15_CR23","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0304-3975(90)90096-Z","volume":"75","author":"S Katz","year":"1990","unstructured":"Katz, S., Peled, D.: Interleaving set temporal logic. Theoret. Comput. Sci. 75(3), 263\u2013287 (1990)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"15_CR24","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems - specification. Springer (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"15_CR26","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. In: Concurrency: The Works of Leslie Lamport, pp. 179\u2013196 (2019)"},{"key":"15_CR27","unstructured":"Mattern, F.: Virtual time and global states of distributed systems. In: Proceedings of Workshop on Parallel and Distributed Algorithms, Chateau de Bonas, France, Elsevier, pp. 215\u2013226 (1988)"},{"key":"15_CR28","unstructured":"Mazurkiewicz, A.: Trace semantics. In: Proceedings of Advances in Petri Nets 1986, Bad Honnef. LNCS, vol. 255, pp. 279\u2013324. Springer, Verlag (1987)"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45414-4_6","volume-title":"Distributed Computing","author":"N Mittal","year":"2001","unstructured":"Mittal, N., Garg, V.K.: Computation slicing: techniques and theory. In: Welch, J. (ed.) DISC 2001. LNCS, vol. 2180, pp. 78\u201392. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45414-4_6"},{"issue":"3","key":"15_CR30","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s00446-004-0117-0","volume":"17","author":"N Mittal","year":"2005","unstructured":"Mittal, N., Garg, V.K.: Techniques and applications of computation slicing. Distrib. Comput. 17(3), 251\u2013277 (2005)","journal-title":"Distrib. Comput."},{"issue":"42","key":"15_CR31","doi-asserted-by":"publisher","first-page":"4180","DOI":"10.1016\/j.tcs.2009.03.002","volume":"410","author":"P Niebert","year":"2009","unstructured":"Niebert, P., Peled, D.: Efficient model checking for LTL with partial order snapshots. Theor. Comput. Sci. 410(42), 4180\u20134189 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-75142-7_32","volume-title":"Distributed Computing","author":"VA Ogale","year":"2007","unstructured":"Ogale, V.A., Garg, V.K.: Detecting temporal logic predicates on distributed computations. In: Pelc, A. (ed.) DISC 2007. LNCS, vol. 4731, pp. 420\u2013434. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75142-7_32"},{"key":"15_CR33","unstructured":"Papadimitriou, C.H.: The Theory of Database Concurrency Control. Computer Science Press (1986)"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Penczek, W., Kuiper, R.: Traces and Logic. In: The Book of Traces, pp. 307\u2013390 (1995)","DOI":"10.1142\/9789814261456_0010"},{"issue":"3","key":"15_CR35","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/0020-0190(92)90007-I","volume":"43","author":"W Penczek","year":"1992","unstructured":"Penczek, W.: On undecidability of propositional temporal logics on trace systems. Inf. Process. Lett. 43(3), 147\u2013153 (1992)","journal-title":"Inf. Process. Lett."},{"key":"15_CR36","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. Theoret. Comput. Sci. 126, 143\u2013182 (1994)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"15_CR37","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S0304-3975(97)00219-3","volume":"195","author":"D Peled","year":"1998","unstructured":"Peled, D., Wilke, T., Wolper, P.: An algorithmic approach for checking closure properties of temporal logic specifications and omega-regular languages. Theoret. Comput. Sci. 195(2), 183\u2013203 (1998)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR38","doi-asserted-by":"crossref","unstructured":"Pinter, S.S., Wolper, P.: A temporal logic for reasoning about partially ordered computations (extended abstract). In: PODC, pp. 28\u201337 (1984)","DOI":"10.1145\/800222.806733"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Reisig, W.: Partial order semantics versus interleaving semantics for CSP-like languages and its impact on fairness. In: ICALP 1984. LNCS, vol. 172, pp. 403\u2013413. Springer, Verlag (1984)","DOI":"10.1007\/3-540-13345-3_37"},{"key":"15_CR40","doi-asserted-by":"crossref","unstructured":"Sen, A., Garg, V.K.: Detecting temporal logic predicates in distributed programs using computation slicing. In: OPODIS 2003, pp. 171\u2013183 (2003)","DOI":"10.1007\/978-3-540-27860-3_17"},{"key":"15_CR41","doi-asserted-by":"crossref","unstructured":"Sen, K., Vardhan, A., Agha, G., Rosu, G.: Decentralized runtime analysis of multithreaded applications. In: IPDPS 2006, 25\u201329 April 2006, Rhodes Island, Greece (2006)","DOI":"10.1109\/IPDPS.2006.1639591"},{"key":"15_CR42","doi-asserted-by":"crossref","unstructured":"Stoller, S., Liu, Y.A.: Efficient symbolic detection of global properties in distributed systems. In: CAV 1998. LNCS, vol. 1427, pp. 357\u2013368. Springer, Verlag (1998)","DOI":"10.1007\/BFb0028758"},{"issue":"2","key":"15_CR43","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1006\/inco.2001.2956","volume":"179","author":"PS Thiagarajan","year":"2002","unstructured":"Thiagarajan, P.S., Walukiewicz, I.: An expressively complete linear time temporal logic for Mazurkiewicz traces. Inf. Comput. 179(2), 230\u2013249 (2002)","journal-title":"Inf. Comput."},{"key":"15_CR44","doi-asserted-by":"crossref","unstructured":"Walukiewicz, I.: Difficult configurations \u2013 on the complexity of LTrL. In: International Colloquium on Automata, Languages and Programming, ICALP 1998. LNCS, vol. 1443, pp. 140\u2013151. Springer, Verlag (1998)","DOI":"10.1007\/BFb0055048"},{"key":"15_CR45","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115, 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"15_CR46","doi-asserted-by":"crossref","unstructured":"Willams, V.V.: On some fine-grained questions in algorithms and complexity. In: ICM 2018, pp. 3447\u20133487 (2018)","DOI":"10.1142\/9789813272880_0188"},{"issue":"2\u20133","key":"15_CR47","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1016\/j.tcs.2005.09.023","volume":"348","author":"R Williams","year":"2005","unstructured":"Williams, R.: A new algorithm for optimal 2-constraint satisfaction and its implications. Theoret. Comput. Sci. 348(2\u20133), 357\u2013365 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR48","doi-asserted-by":"crossref","unstructured":"Winskel, G.: Event structures. In: Advances in Petri Nets, pp. 325\u2013392 (1986)","DOI":"10.1007\/3-540-17906-2_31"},{"key":"15_CR49","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths (extended abstract). In: FOCS 1983, pp. 185\u2013194 (1983)","DOI":"10.1109\/SFCS.1983.51"},{"key":"15_CR50","unstructured":"PoET tool source code. https:\/\/github.com\/moraneus\/PoET"},{"key":"15_CR51","unstructured":"Kairos tool source code. https:\/\/github.com\/moraneus\/kairos"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05435-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T07:43:27Z","timestamp":1766043807000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05435-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,12]]},"ISBN":["9783032054340","9783032054357"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05435-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,9,12]]},"assertion":[{"value":"12 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Graz","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv25.isec.tugraz.at\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}