{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T09:05:41Z","timestamp":1726045541145},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030315139"},{"type":"electronic","value":"9783030315146"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-31514-6_8","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"126-145","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Generating Hard Benchmark Problems for Weak Bisimulation"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Steffen","sequence":"first","affiliation":[]},{"given":"Marc","family":"Jasper","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Bartocci, E., et al.: First international competition on runtime verification: rules, benchmarks, tools, and final results of CRV 2014. STTT, pp. 1\u201340, April 2017","DOI":"10.1007\/s10009-017-0454-5"},{"key":"8_CR2","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., et al.: Moving from specifications to contracts in component-based design. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 43\u201358. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_3"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 233\u2013248. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_12"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-28756-5_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2012","unstructured":"Beyer, D.: Competition on software verification. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504\u2013524. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_38"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bunte","year":"2019","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21\u201339. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2"},{"key":"8_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). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-44577-3_12","volume-title":"Informatics","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Wilhelm, R. (ed.) Informatics. LNCS, vol. 2000, pp. 176\u2013194. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44577-3_12"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36\u201372 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR9","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). https:\/\/doi.org\/10.1007\/BFb0039057"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Czech, M., H\u00fcllermeier, E., Jakobs, M.C., Wehrheim, H.: Predicting rankings of software verification tools. In: Proceedings of the 3rd ACM SIGSOFT International Workshop on Software Analytics, SWAN 2017, pp. 23\u201326. ACM (2017)","DOI":"10.1145\/3121257.3121262"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transfer 15(2), 89\u2013107 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"8_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., van de 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). https:\/\/doi.org\/10.1007\/978-3-319-47169-3_59"},{"key":"8_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). https:\/\/doi.org\/10.1007\/3-540-60761-7"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/BFb0023732","volume-title":"Computer-Aided Verification","author":"S Graf","year":"1991","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186\u2013196. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023732"},{"issue":"5","key":"8_CR15","doi-asserted-by":"publisher","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. Formal Aspects Comput. 8(5), 607\u2013616 (1996)","journal-title":"Formal Aspects Comput."},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Grosu","year":"2005","unstructured":"Grosu, R., Smolka, S.A.: Monte Carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 271\u2013286. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_18"},{"issue":"3","key":"8_CR17","doi-asserted-by":"publisher","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)"},{"key":"8_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, New York (1978). https:\/\/doi.org\/10.1007\/978-1-4757-3472-0_16"},{"issue":"5","key":"8_CR19","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/s10009-014-0337-y","volume":"16","author":"F Howar","year":"2014","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., P\u0103s\u0103reanu, C.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. STTT 16(5), 457\u2013464 (2014)","journal-title":"STTT"},{"issue":"6","key":"8_CR20","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10009-015-0396-8","volume":"17","author":"M Huisman","year":"2015","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis 2012. STTT 17(6), 647\u2013657 (2015)","journal-title":"STTT"},{"key":"8_CR21","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). https:\/\/doi.org\/10.1007\/3-540-51237-3_14"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-030-17502-3_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Jasper","year":"2019","unstructured":"Jasper, M., et al.: RERS 2019: combining synthesis with real-world models. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 101\u2013115. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_7"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-030-03421-4_27","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"M Jasper","year":"2018","unstructured":"Jasper, M., Mues, M., Schl\u00fcter, M., Steffen, B., Howar, F.: RERS 2018: CTL, LTL, and reachability. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 433\u2013447. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_27"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-030-03421-4_16","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"M Jasper","year":"2018","unstructured":"Jasper, M., Steffen, B.: Synthesizing subtle bugs with known witnesses. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 235\u2013257. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_16"},{"issue":"1","key":"8_CR25","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"PC Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"key":"8_CR26","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., van der 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). https:\/\/doi.org\/10.1007\/978-3-642-35179-2_8"},{"key":"8_CR27","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). https:\/\/doi.org\/10.1007\/3-540-52148-8_19"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_11"},{"issue":"6","key":"8_CR29","doi-asserted-by":"publisher","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":"8_CR30","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167\u2013183. Springer, Heidelberg (1981). https:\/\/doi.org\/10.1007\/BFb0017309"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1989, pp. 179\u2013190. ACM (1989)","DOI":"10.1145\/75277.75293"},{"issue":"1\u20132","key":"8_CR33","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":"8_CR34","doi-asserted-by":"crossref","unstructured":"Steffen, B., Jasper, M., Meijer, J., van de Pol, J.: Property-preserving generation of tailored benchmark petri nets. In: 17th International Conference on Application of Concurrency to System Design (ACSD), pp. 1\u20138, June 2017","DOI":"10.1109\/ACSD.2017.24"},{"key":"8_CR35","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., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 723\u2013732. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0035794"},{"key":"8_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-21455-4_8","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"B Steffen","year":"2011","unstructured":"Steffen, B., Howar, F., Merten, M.: Introduction to active automata learning from a practical perspective. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 256\u2013296. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_8"},{"issue":"5","key":"8_CR37","doi-asserted-by":"publisher","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":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-63121-9_7","volume-title":"Models, Algorithms, Logics and Tools","author":"B Steffen","year":"2017","unstructured":"Steffen, B., Jasper, M.: Property-preserving parallel decomposition. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 125\u2013145. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_7"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/3-540-65306-6_21","volume-title":"Lectures on Petri Nets I: Basic Models","author":"A Valmari","year":"1998","unstructured":"Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429\u2013528. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-65306-6_21"},{"issue":"1","key":"8_CR40","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1006\/inco.1995.1123","volume":"121","author":"R Vanglabbeek","year":"1995","unstructured":"Vanglabbeek, R., Smolka, S., Steffen, B.: Reactive, generative, and stratified models of probabilistic processes. Inf. Comput. 121(1), 59\u201380 (1995)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","From Reactive Systems to Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31514-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,7]],"date-time":"2019-12-07T18:55:33Z","timestamp":1575744933000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31514-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030315139","9783030315146"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31514-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}