{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:38:37Z","timestamp":1743071917348,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175232"},{"type":"electronic","value":"9783319175249"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-17524-9_6","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"66-81","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Compositional Verification of Parameterised Timed Systems"],"prefix":"10.1007","author":[{"given":"L\u0103cr\u0103mioara","family":"A\u015ftef\u0103noaei","sequence":"first","affiliation":[]},{"given":"Souha","family":"Ben Rayana","sequence":"additional","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]},{"given":"Jacques","family":"Combaz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"6_CR1","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS (1996)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/978-3-642-24310-3_18","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"PA Abdulla","year":"2011","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R.: On the Verification of Timed Ad Hoc Networks. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 256\u2013270. Springer, Heidelberg (2011)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Deneux, J., Mahata, P.: Closed, open, and robust timed networks. ENTCS 138(3) (2005)","DOI":"10.1016\/j.entcs.2005.03.027"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-48092-7_9","volume-title":"Correct System Design","author":"PA Abdulla","year":"1999","unstructured":"Abdulla, P.A., Jonsson, B.: On the Existence of Network Invariants for Verifying Parameterized Systems. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 180\u2013197. Springer, Heidelberg (1999)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theor. Comput. Sci. 290(1) (2003)","DOI":"10.1016\/S0304-3975(01)00330-9"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/978-3-540-28644-8_3","volume-title":"CONCUR 2004 - Concurrency Theory","author":"PA Abdulla","year":"2004","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A Survey of Regular Model Checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35\u201348. Springer, Heidelberg (2004)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification","author":"R Alur","year":"1999","unstructured":"Alur, R.: Timed Automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8\u201322. Springer, Heidelberg (1999)"},{"key":"6_CR8","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: RTSS (1992)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/978-3-642-54862-8_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L A\u015ftef\u0103noaei","year":"2014","unstructured":"A\u015ftef\u0103noaei, L., Ben Rayana, S., Bensalem, S., Bozga, M., Combaz, J.: Compositional Invariant Generation for Timed Systems. In: \\\u2019{A}brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 263\u2013278. Springer, Heidelberg (2014)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/3-540-46419-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Baukus","year":"2000","unstructured":"Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting WS1S Systems to Verify Parameterized Networks. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 188\u2013203. Springer, Heidelberg (2000)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Baukus, K., Stahl, K., Bensalem, S., Lakhnech, Y.: Networks of processes with parameterized state space. ENTCS 50(4) (2001)","DOI":"10.1016\/S1571-0661(04)00190-2"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-540-88387-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"S Bensalem","year":"2008","unstructured":"Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional Verification for Component-Based Systems and Application. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64\u201379. Springer, Heidelberg (2008)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1007\/978-3-540-71209-1_54","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Bouajjani","year":"2007","unstructured":"Bouajjani, A., Jurski, Y., Sighireanu, M.: A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 690\u2013705. Springer, Heidelberg (2007)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/978-3-642-28891-3_28","volume-title":"NASA Formal Methods","author":"R Bruttomesso","year":"2012","unstructured":"Bruttomesso, R., Carioni, A., Ghilardi, S., Ranise, S.: Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 279\u2013294. Springer, Heidelberg (2012)"},{"key":"6_CR16","unstructured":"Carioni, A., Ghilardi, S., Ranise, S.: Mcmt in the land of parametrized timed automata. In: VERIFY@IJCAR (2010)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: CADE (2000)","DOI":"10.1007\/10721959_19"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL (1995)","DOI":"10.1145\/199448.199468"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A. P.: Symmetry and model checking. Formal Methods in System Design 9(1\/2) (1996)","DOI":"10.1007\/BF00625970"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Finkel, A.: A generalization of the procedure of karp and miller to well structured transition systems. In: ICALP (1987)","DOI":"10.1007\/3-540-18088-5_43"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2) (2001)","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3) (1992)","DOI":"10.1145\/146637.146681"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-3-540-71070-7_6","volume-title":"Automated Reasoning","author":"S Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT Model Checking of Array-Based Systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 67\u201382. Springer, Heidelberg (2008)"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/978-3-540-78499-9_33","volume-title":"Foundations of Software Science and Computational Structures","author":"P Habermehl","year":"2008","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What Else Is Decidable about Integer Arrays? In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474\u2013489. Springer, Heidelberg (2008)"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. (1994)","DOI":"10.1006\/inco.1994.1045"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On Local Reasoning in Verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 18\u201334. Springer, Heidelberg (2012)"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Legay, A., Bensalem, S., Boyer, B., Bozga, M.: Incremental generation of linear invariants for component-based systems. In: ACSD (2013)","DOI":"10.1109\/ACSD.2013.11"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: POPL (1997)","DOI":"10.1145\/263699.263747"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized networks of processes. Theor. Comput. Sci. 256(1\u20132) (2001)","DOI":"10.1016\/S0304-3975(00)00104-3"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: Symmetry and Completeness in the Analysis of Parameterized Systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 299\u2013313. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-69738-1_22"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Amir Pnueli","year":"2001","unstructured":"Pnueli, Amir, Ruah, Sitvanit, Zuck, Lenore D.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, Tiziana, Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Reich, J.: Processes, roles and their interactions. In: Proceedings of IWIGP (2012)","DOI":"10.4204\/EPTCS.78.3"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: AVMFSS (1989)","DOI":"10.1007\/3-540-52148-8_6"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: FORTE (1994)","DOI":"10.1007\/978-0-387-34878-0_18"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T00:45:35Z","timestamp":1676940335000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}