{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,4]],"date-time":"2025-10-04T18:22:10Z","timestamp":1759602130711},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319631202"},{"type":"electronic","value":"9783319631219"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63121-9_7","type":"book-chapter","created":{"date-parts":[[2017,7,24]],"date-time":"2017-07-24T08:05:15Z","timestamp":1500883515000},"page":"125-145","source":"Crossref","is-referenced-by-count":10,"title":["Property-Preserving Parallel Decomposition"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Steffen","sequence":"first","affiliation":[]},{"given":"Marc","family":"Jasper","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,25]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-28872-2_3","volume-title":"Fundamental Approaches to Software Engineering","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., David, A., Hennicker, R., Guldstrand Larsen, K., Legay, A., Nyman, U., W\u0105sowski, A.: Moving from specifications to contracts in component-based design. In: Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 43\u201358. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28872-2_3"},{"key":"7_CR2","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1016\/j.scico.2013.06.003","volume":"83","author":"SS Bauer","year":"2014","unstructured":"Bauer, S.S., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: A modal specification theory for components with data. Sci. Comput. Program. 83, 106\u2013128 (2014)","journal-title":"Sci. Comput. Program."},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-40184-8_7","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"N Bene\u0161","year":"2013","unstructured":"Bene\u0161, N., Delahaye, B., Fahrenberg, U., K\u0159et\u00ednsk\u00fd, J., Legay, A.: Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 76\u201390. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40184-8_7"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-24372-1_20","volume-title":"Automated Technology for Verification and Analysis","author":"N Bene\u0161","year":"2011","unstructured":"Bene\u0161, N., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., M\u00f8ller, M.H., Srba, J.: Parametric modal transition systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 275\u2013289. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24372-1_20"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-319-63121-9_12","volume-title":"Models, Algorithms, Logics and Tools","author":"A Benveniste","year":"2017","unstructured":"Benveniste, A., Caillaud, B.: Synchronous interfaces and assume\/guarantee contracts. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Larsen Festschrift. LNCS, vol. 10460, pp. 233\u2013248. Springer, Cham (2017)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). doi: 10.1007\/10722167_15"},{"key":"7_CR7","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). doi: 10.1007\/BFb0025774"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/BFb0039057","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"R Cleaveland","year":"1990","unstructured":"Cleaveland, R., Steffen, B.: A preorder for partial process specifications. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 141\u2013151. Springer, Heidelberg (1990). doi: 10.1007\/BFb0039057"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-51963-0_5","volume-title":"SOFSEM 2017: Theory and Practice of Computer Science","author":"U Fahrenberg","year":"2017","unstructured":"Fahrenberg, U., Legay, A.: A linear-time\u2013branching-time spectrum of behavioral specification theories. In: Steffen, B., Baier, C., Brand, M., Eder, J., Hinchey, M., Margaria, T. (eds.) SOFSEM 2017. LNCS, vol. 10139, pp. 49\u201361. Springer, Cham (2017). doi: 10.1007\/978-3-319-51963-0_5"},{"issue":"1\u20132","key":"7_CR10","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/j.jlap.2008.05.003","volume":"77","author":"H Fecher","year":"2008","unstructured":"Fecher, H., Schmidt, H.: Comparing disjunctive modal transition systems with an one-selecting variant. J. Logic Algebraic Program. 77(1\u20132), 20\u201339 (2008)","journal-title":"J. Logic Algebraic Program."},{"key":"7_CR11","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1145\/1047659.1040315","volume":"40","author":"C Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. ACM SIGPLAN Not. 40, 110\u2013121 (2005)","journal-title":"ACM SIGPLAN Not."},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"787","DOI":"10.1007\/978-3-319-47169-3_59","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"M Geske","year":"2016","unstructured":"Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., Pol, J.: RERS 2016: parallel and sequential benchmarks with focus on LTL verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 787\u2013803. Springer, Cham (2016). doi: 10.1007\/978-3-319-47169-3_59"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","year":"1996","unstructured":"Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996). doi: 10.1007\/3-540-60761-7"},{"key":"7_CR14","first-page":"57","volume":"90","author":"S Graf","year":"1990","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state processes. Comput.-Aided Verification 90, 57\u201373 (1990)","journal-title":"Comput.-Aided Verification"},{"issue":"5","key":"7_CR15","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S Graf","year":"1996","unstructured":"Graf, S., Steffen, B., L\u00fcttgen, G.: Compositional minimisation of finite state systems using interface specifications. Form. Asp. Comput. 8(5), 607\u2013616 (1996)","journal-title":"Form. Asp. Comput."},{"issue":"3","key":"7_CR16","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(3), 843\u2013871 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"1","key":"7_CR17","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/565816.503279","volume":"37","author":"TA Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. ACM SIGPLAN Not. 37(1), 58\u201370 (2002)","journal-title":"ACM SIGPLAN Not."},{"key":"7_CR18","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-1-4757-3472-0_16","volume-title":"The Origin of Concurrent Programming","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413\u2013443. Springer, Heidelberg (1978). doi: 10.1007\/978-1-4757-3472-0_16"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1007\/978-3-642-34026-0_45","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"F Howar","year":"2012","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 608\u2013614. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-34026-0_45"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/3-540-51237-3_14","volume-title":"Logic at Botik \u201989","author":"H H\u00fcttel","year":"1989","unstructured":"H\u00fcttel, H., Larsen, K.G.: The use of static constructs in a model process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 163\u2013180. Springer, Heidelberg (1989). doi: 10.1007\/3-540-51237-3_14"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/3-540-53982-4_21","volume-title":"TAPSOFT \u201991","author":"B Jonsson","year":"1991","unstructured":"Jonsson, B., Larsen, K.G.: On the complexity of equation solving in process algebra. In: Abramsky, S., Maibaum, T.S.E. (eds.) CAAP 1991. LNCS, vol. 493, pp. 381\u2013396. Springer, Heidelberg (1991). doi: 10.1007\/3-540-53982-4_21"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A.,Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Tri.nh, G., Wolf, K.: Complete Results for the 2016 Edition of the Model Checking Contest, June 2016. http:\/\/mcc.lip6.fr\/2016\/results.php","DOI":"10.1007\/978-3-662-53401-4_12"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-35179-2_8","volume-title":"Transactions on Petri Nets and Other Models of Concurrency VI","author":"F Kordon","year":"2012","unstructured":"Kordon, F., et al.: Report on the model checking contest at petri nets 2011. In: Jensen, K., Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol. 7400, pp. 169\u2013196. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-35179-2_8"},{"key":"7_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27919-5","volume-title":"The Correctness-by-Construction Approach to Programming","author":"DG Kourie","year":"2012","unstructured":"Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer Science & Business Media, Berlin (2012). doi: 10.1007\/978-3-642-27919-5"},{"key":"7_CR25","unstructured":"K\u0159et\u00ednsk\u1ef3, J.: Modal transition systems: extensions and analysis. Ph.D. thesis, Masarykova univerzita, Fakulta informatiky (2014)"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-60630-0_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KG Larsen","year":"1995","unstructured":"Larsen, K.G., Steffen, B., Weise, C.: A constraint oriented proof methodology based on modal transition systems. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 17\u201340. Springer, Heidelberg (1995). doi: 10.1007\/3-540-60630-0_2"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BFb0024437","volume-title":"Formal Systems Specification","author":"KG Larsen","year":"1996","unstructured":"Larsen, K.G., Steffen, B., Weise, C.: The methodology of modal constraints. In: Broy, M., Merz, S., Spies, K. (eds.) Formal Systems Specification. LNCS, vol. 1169, pp. 405\u2013435. Springer, Heidelberg (1996). doi: 10.1007\/BFb0024437"},{"issue":"1","key":"7_CR28","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/0304-3975(91)90071-9","volume":"88","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Thomsen, B.: Partial specifications and compositional verification. Theoret. Comput. Sci. 88(1), 15\u201332 (1991)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic Verification Methods for Finite State Systems","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232\u2013246. Springer, Heidelberg (1990). doi: 10.1007\/3-540-52148-8_19"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BFb0039050","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"K Guldstrand Larsen","year":"1990","unstructured":"Guldstrand Larsen, K.: Ideal specification formalism = expressivity + compositionality + decidability + testability +. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 33\u201356. Springer, Heidelberg (1990). doi: 10.1007\/BFb0039050"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 1990, pp. 108\u2013117. IEEE (1990)","DOI":"10.1109\/LICS.1990.113738"},{"issue":"6","key":"7_CR32","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1109\/MC.2010.177","volume":"43","author":"T Margaria","year":"2010","unstructured":"Margaria, T., Steffen, B.: Simplicity as a driver for agile innovation. Computer 43(6), 90\u201392 (2010)","journal-title":"Computer"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993). doi: 10.1007\/3-540-56922-7_34"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1\u20132","key":"7_CR35","doi-asserted-by":"crossref","first-page":"119","DOI":"10.3233\/FI-2011-416","volume":"108","author":"JB Raclet","year":"2011","unstructured":"Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundamenta Informaticae 108(1\u20132), 119\u2013149 (2011)","journal-title":"Fundamenta Informaticae"},{"key":"7_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1007\/BFb0035794","volume-title":"Automata, Languages and Programming","author":"B Steffen","year":"1989","unstructured":"Steffen, B.: Characteristic formulae. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 723\u2013732. Springer, Heidelberg (1989). doi: 10.1007\/BFb0035794"},{"issue":"1","key":"7_CR37","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1006\/inco.1994.1028","volume":"110","author":"B Steffen","year":"1994","unstructured":"Steffen, B., Ing\u00f3lfsd\u00f3ttir, A.: Characteristic formulas for processes with divergence. Inf. Comput. 110(1), 149\u2013163 (1994)","journal-title":"Inf. Comput."},{"issue":"5","key":"7_CR38","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/s10009-014-0336-z","volume":"16","author":"B Steffen","year":"2014","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Int. J. Softw. Tools Technol. Transfer 16(5), 465\u2013479 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Steffen, B., Jasper, M., van de Pol, J., Meijer, J.: Property-preserving generation of tailored benchmark petri nets. In: Proceedings of ACSD 2017. IEEE Computer Society (2017, to appear)","DOI":"10.1109\/ACSD.2017.24"},{"key":"7_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991). doi: 10.1007\/3-540-53863-1_36"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-93900-9_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"O Wei","year":"2008","unstructured":"Wei, O., Gurfinkel, A., Chechik, M.: Mixed transition systems revisited. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 349\u2013365. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-93900-9_28"}],"container-title":["Lecture Notes in Computer Science","Models, Algorithms, Logics and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63121-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,31]],"date-time":"2022-07-31T11:11:57Z","timestamp":1659265917000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63121-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631202","9783319631219"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63121-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}