{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T14:26:38Z","timestamp":1742394398273},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372158"},{"type":"electronic","value":"9783540372165"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11813040_37","type":"book-chapter","created":{"date-parts":[[2006,8,7]],"date-time":"2006-08-07T06:51:03Z","timestamp":1154933463000},"page":"557-572","source":"Crossref","is-referenced-by-count":13,"title":["Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Genon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"Massart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9dric","family":"Meuter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Alur, R., Peled, D., Penczek, W.: Model checking of causality properties. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS 1995), San Diego, California, pp. 90\u2013100 (1995)","key":"37_CR1","DOI":"10.1109\/LICS.1995.523247"},{"issue":"3","key":"37_CR2","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv.\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"key":"37_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An openSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Charron-Bost, B., Delporte-Gallet, C., Fauconnier, H.: Local and temporal predicates in distributed systems. ACM Trans. Program. Lang. Syst.\u00a017(1) (1995)","key":"37_CR4","DOI":"10.1145\/200994.201005"},{"issue":"4","key":"37_CR5","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s004460050049","volume":"11","author":"C.M. Chase","year":"1998","unstructured":"Chase, C.M., Garg, V.K.: Detection of global predicates: Techniques and their limitations. Distributed Computing\u00a011(4), 191\u2013201 (1998)","journal-title":"Distributed Computing"},{"key":"37_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)"},{"issue":"1","key":"37_CR7","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/214451.214456","volume":"3","author":"K. Mani Chandy","year":"1985","unstructured":"Mani Chandy, K., Lamport, L.: Distributed snapshots: Determining global states of distributed systems. ACM Trans. Comput. Syst.\u00a03(1), 63\u201375 (1985)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"2","key":"37_CR8","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1006\/jcss.2001.1817","volume":"64","author":"V. Diekert","year":"2002","unstructured":"Diekert, V., Gastin, P.: LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences\u00a064(2), 396\u2013418 (2002)","journal-title":"Journal of Computer and System Sciences"},{"issue":"2","key":"37_CR9","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s00165-005-0066-9","volume":"17","author":"B. Wachter De","year":"2005","unstructured":"De Wachter, B., Genon, A., Massart, T., Meuter, C.: The formal design of distributed controllers with dsl and spin. Formal Aspects of Computing\u00a017(2), 177\u2013200 (2005)","journal-title":"Formal Aspects of Computing"},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-27860-3_14","volume-title":"Principles of Distributed Systems","author":"B. Wachter De","year":"2004","unstructured":"De Wachter, B., Massart, T., Meuter, C.: dsl: An environment with automatic code distribution for industrial control systems. In: Papatriantafilou, M., Hunel, P. (eds.) OPODIS 2003. LNCS, vol.\u00a03144, pp. 132\u2013145. Springer, Heidelberg (2004)"},{"issue":"2-3","key":"37_CR11","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/s10009-003-0110-0","volume":"5","author":"G. Delzanno","year":"2004","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Covering sharing trees: a compact data structure for parameterized verification. STTT\u00a05(2-3), 268\u2013297 (2004)","journal-title":"STTT"},{"doi-asserted-by":"crossref","unstructured":"Esparza, J., R\u00f6mer, S., Vogler, W.: An improvement of mcmillan\u2019s unfolding algorithm. In: TACAS, pp. 87\u2013106 (1996)","key":"37_CR12","DOI":"10.1007\/3-540-61042-1_40"},{"unstructured":"Ganty, P.: Algorithmes et structures de donn\u00e9es efficaces pour la manipulation de contraintes sur les intervalles. Master\u2019s thesis, Universit\u00e9 Libre de Bruxelles (2002)","key":"37_CR13"},{"doi-asserted-by":"crossref","unstructured":"Garg, V.K., Mittal, N.: On slicing a distributed computation. In: ICDCS, pp. 322\u2013329 (2001)","key":"37_CR14","DOI":"10.1109\/ICDSC.2001.918962"},{"doi-asserted-by":"crossref","unstructured":"Genon, A., Massart, T., Meuter, C.: Monitoring distributed controllers: When an efficient ltl algorithm on sequences is needed to model-check traces. Technical Report 2006-59, CFV - Universit\u00e9 Libre de Bruxelles (2006)","key":"37_CR15","DOI":"10.1007\/11813040_37"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)","key":"37_CR16","DOI":"10.1007\/3-540-60761-7"},{"issue":"3","key":"37_CR17","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.: Detection of weak unstable predicates in distributed programs. IEEE Trans. Parallel Distrib. Syst.\u00a05(3), 299\u2013307 (1994)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"12","key":"37_CR18","doi-asserted-by":"publisher","first-page":"1323","DOI":"10.1109\/71.553309","volume":"7","author":"V.K. Garg","year":"1996","unstructured":"Garg, V.K., Waldecker, B.: Detection of strong unstable predicates in distributed programs. IEEE Trans. Parallel Distrib. Syst.\u00a07(12), 1323\u20131333 (1996)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"5","key":"37_CR19","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. Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"issue":"7","key":"37_CR20","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM\u00a021(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"37_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45251-6_6","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"M. Leuschel","year":"2001","unstructured":"Leuschel, M., Massart, T., Currie, A.: How to make fdr spin: Ltl model checking of csp by refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 99\u2013118. Springer, Heidelberg (2001)"},{"key":"37_CR22","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)"},{"unstructured":"Mattern, F.: Virtual time and global states of distributed systems. In: Cosnard, M., et al. (eds.) Proc. Workshop on Parallel and Distributed Algorithms, pp. 215\u2013226. North-Holland \/ Elsevier (1989)","key":"37_CR23"},{"doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.W.: Trace theory. Advances in Petri Nets, pp. 279\u2013324 (1986)","key":"37_CR24","DOI":"10.1007\/3-540-17906-2_30"},{"doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking: an approach to the state explosion problem, Carnegie Mellon University (1992)","key":"37_CR25","DOI":"10.1007\/978-1-4615-3190-6_3"},{"unstructured":"McMillan, K.L.: The smv system. Technical Report CMU-CS-92-131, Carnegie Mellon University (1992)","key":"37_CR26"},{"issue":"1","key":"37_CR27","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF01384314","volume":"6","author":"K.L. McMillan","year":"1995","unstructured":"McMillan, K.L.: A technique of state space search based on unfolding. Formal Methods in System Design\u00a06(1), 45\u201365 (1995)","journal-title":"Formal Methods in System Design"},{"key":"37_CR28","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.L. (ed.) DISC 2001. LNCS, vol.\u00a02180, pp. 78\u201392. Springer, Heidelberg (2001)"},{"issue":"3","key":"37_CR29","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. Distributed Computing\u00a017(3), 251\u2013277 (2005)","journal-title":"Distributed Computing"},{"key":"37_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-27860-3_17","volume-title":"Principles of Distributed Systems","author":"A. Sen","year":"2004","unstructured":"Sen, A., Garg, V.K.: Detecting Temporal Logic Predicates in Distributed Programs Using Computation Slicing. In: Papatriantafilou, M., Hunel, P. (eds.) OPODIS 2003. LNCS, vol.\u00a03144, pp. 171\u2013183. Springer, Heidelberg (2004)"},{"key":"37_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-540-24730-2_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Sen","year":"2004","unstructured":"Sen, K., Rosu, G., Agha, G.: Online efficient predictive safety analysis of multithreaded programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 123\u2013138. Springer, Heidelberg (2004)"},{"key":"37_CR32","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1109\/ICSE.2004.1317464","volume-title":"Proceedings of 26th International Conference on Software Engineering (ICSE 2004)","author":"K. Sen","year":"2004","unstructured":"Sen, K., Vardhan, A., Agha, G., Rosu, G.: Efficient decentralized monitoring of safety in distributed systems. In: Proceedings of 26th International Conference on Software Engineering (ICSE 2004), Edinburgh, UK, pp. 418\u2013427. IEEE, Los Alamitos (2004)"},{"key":"37_CR33","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1109\/LICS.1994.316047","volume-title":"Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, LICS 1994","author":"P.S. Thiagarajan","year":"1994","unstructured":"Thiagarajan, P.S.: A trace based extension of linear time temporal logic. In: Abramsky, S. (ed.) Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, LICS 1994, pp. 438\u2013447. IEEE Computer Society Press, Los Alamitos (1994)"},{"issue":"2","key":"37_CR34","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. Inf. Comput.\u00a0179(2), 230\u2013249 (2002)","journal-title":"Inf. Comput."},{"doi-asserted-by":"crossref","unstructured":"Valmari, A.: On-the-fly verification with stubborn sets. In: CAV, pp. 397\u2013408 (1993)","key":"37_CR35","DOI":"10.1007\/3-540-56922-7_33"},{"unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Symp. on Logic in Computer Science, Cambridge, June 1986, pp. 332\u2013344 (1986)","key":"37_CR36"}],"container-title":["Lecture Notes in Computer Science","FM 2006: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11813040_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:14:25Z","timestamp":1605626065000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11813040_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372158","9783540372165"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/11813040_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}