{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:29:41Z","timestamp":1759638581355,"version":"3.40.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319121536"},{"type":"electronic","value":"9783319121543"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-12154-3_15","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T08:20:23Z","timestamp":1413188423000},"page":"235-251","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Parameterized Model-Checking of Timed Systems with Conjunctive Guards"],"prefix":"10.1007","author":[{"given":"Luca","family":"Spalazzi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Spegni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,10,14]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0054179","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"1998","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying networks of timed processes (extended abstract). In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 298\u2013312. Springer, Heidelberg (1998)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Deneux, J., Mahata, P.: Multi-clock timed networks. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science, pp. 345\u2013354 (2004)","DOI":"10.1109\/LICS.2004.1319629"},{"issue":"1","key":"15_CR3","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/S0304-3975(01)00330-9","volume":"290","author":"PA Abdulla","year":"2003","unstructured":"Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theoret. Comput. Sci. 290(1), 241\u2013264 (2003)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of the Fifth Symposium on Logic in Computer Science, pp. 414\u2013425 (1990)","DOI":"10.1109\/LICS.1990.113766"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54013-4_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Aminof","year":"2014","unstructured":"Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 262\u2013281. Springer, Heidelberg (2014)"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K Apt","year":"1986","unstructured":"Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22, 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-662-44584-6_9","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"B Aminof","year":"2014","unstructured":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 109\u2013124. Springer, Heidelberg (2014)"},{"issue":"7","key":"15_CR8","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68\u201376 (2011)","journal-title":"Commun. ACM"},{"issue":"2","key":"15_CR9","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1022905120346","volume":"22","author":"S Ben-David","year":"2003","unstructured":"Ben-David, S., Eisner, C., Geist, D., Wolfsthal, Y.: Model checking at IBM. Formal Methods Sys. Des. 22(2), 101\u2013108 (2003)","journal-title":"Formal Methods Sys. Des."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. Technical report 316, UNU-IIST (2004)","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10703-008-0048-7","volume":"32","author":"A Bouajjani","year":"2008","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Verification of parametric concurrent systems with prioritised FIFO resource management. Formal Methods Syst. Des. 32, 129\u2013172 (2008)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/j.entcs.2009.02.044","volume":"231","author":"P Bouyer","year":"2009","unstructured":"Bouyer, P.: Model-checking timed temporal logics. Electron. Notes Theor. Comput. Sci. 231, 323\u2013341 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"15_CR13","unstructured":"Carioni, A., Ghilardi, S., Ranise, S.: MCMT in the land of parameterized timed automata. In: Proceedings of VERIFY@IJCAR 2010, pp. 1\u201316 (2010)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Browne, M.: Reasoning about networks with many identical finite-state processes. In: Proceedings of the 5th Annual ACM Symposium on Principles of Distributed Computing, pp. 240\u2013248 (1986)","DOI":"10.1145\/10590.10611"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"A Emerson","year":"2000","unstructured":"Emerson, A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE-17. LNCS, vol. 1831, pp. 236\u2013254. Springer, Heidelberg (2000)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"Computer Aided Verification","author":"A Emerson","year":"1996","unstructured":"Emerson, A., Namjoshi, K.: Automatic verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 87\u201398. Springer, Heidelberg (1996)"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Emerson, E., Namjoshi, K.: On model checking for non-deterministic infinite-state systems. In: Proceedings of 13th IEEE Symposium on Logic in Computer Science, pp. 70\u201380 (1998)","DOI":"10.1109\/LICS.1998.705644"},{"issue":"4","key":"15_CR18","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527\u2013550 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"3","key":"15_CR19","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"issue":"2","key":"15_CR20","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: The Verisoft approach. Formal Methods Syst. Des. 26(2), 77\u2013101 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Gothel, T., Glesner, S.: Towards the semi-automatic verification of parameterized real-time systems using network invariants. In: 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM), pp. 310\u2013314 (2010)","DOI":"10.1109\/SEFM.2010.38"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-16901-4_23","volume-title":"Formal Methods and Software Engineering","author":"Y Hanna","year":"2010","unstructured":"Hanna, Y., Samuelson, D., Basu, S., Rajan, H.: Automating Cut-off for Multi-parameterized systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 338\u2013354. Springer, Heidelberg (2010)"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-30793-5_2","volume-title":"Formal Techniques for Distributed Systems","author":"TT Johnson","year":"2012","unstructured":"Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FORTE\/FMOODS 2012. LNCS, vol. 7273, pp. 18\u201334. Springer, Heidelberg (2012)"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Kurshan, R., McMillan, K.: A structural induction theorem for processes. In: ACM Symposium on Principles of Distributed Computing, pp. 239\u2013247 (1989)","DOI":"10.1145\/72981.72998"},{"key":"15_CR25","unstructured":"Mansouri-Samani, M., Mehlitz, P., Pasareanu, C., Penix, J., Brat, G., Markosian, L., O\u2019Malley, O., Pressburger, T., Visser, W.: Program model checking-a practitioners guide. Technical report NASA\/TM-2008-214577, NASA (2008)"},{"issue":"3","key":"15_CR26","doi-asserted-by":"publisher","first-page":"811","DOI":"10.1016\/j.future.2011.11.010","volume":"29","author":"F Pagliarecci","year":"2013","unstructured":"Pagliarecci, F., Spalazzi, L., Spegni, F.: Model checking grid security. Future Gener. Comput. Syst. 29(3), 811\u2013827 (2013)","journal-title":"Future Gener. Comput. Syst."},{"key":"15_CR27","unstructured":"RTCA. Software Considerations in Airborne Systems and Equipment Certification. Technical report DO-178C, RTCA Inc. (2011)"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Spalazzi, L., Spegni, F.: Parameterized model-checking for timed systems with conjunctive guards (extended version) (2014). arxiv:1407.7305[cs.Lo]","DOI":"10.1007\/978-3-319-12154-3_15"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Yang, Q., Li, M.: A cut-off approach for bounded verification of parameterized systems. In: Proceedings of the International Conference on Software Engineering, pp. 345\u2013354. ACM (2010)","DOI":"10.1145\/1806799.1806851"},{"issue":"3\u20134","key":"15_CR30","first-page":"139","volume":"30","author":"L Zuck","year":"2004","unstructured":"Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comp. Lang. Syst. Struct. 30(3\u20134), 139\u2013169 (2004)","journal-title":"Comp. Lang. Syst. Struct."}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12154-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T03:40:08Z","timestamp":1746416408000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12154-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319121536","9783319121543"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12154-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"14 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}