{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T10:10:02Z","timestamp":1746267002360,"version":"3.40.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319076010"},{"type":"electronic","value":"9783319076027"}],"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-07602-7_20","type":"book-chapter","created":{"date-parts":[[2014,6,12]],"date-time":"2014-06-12T11:29:08Z","timestamp":1402572548000},"page":"329-347","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Layered Reduction for Modal Specification Theories"],"prefix":"10.1007","author":[{"given":"Arpit","family":"Sharma","sequence":"first","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,6,13]]},"reference":[{"key":"20_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-35743-5_5","volume-title":"Formal Aspects of Component Software","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., Guldstrand Larsen, K., Legay, A., Nyman, U., W\u0105sowski, A.: A modal specification theory for components with data. In: Arbab, F., \u00d6lveczky, P.C. (eds.) FACS 2011. LNCS, vol. 7253, pp. 61\u201378. Springer, Heidelberg (2012)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-24372-1_17","volume-title":"Automated Technology for Verification and Analysis","author":"N Bene\u0161","year":"2011","unstructured":"Bene\u0161, N., \u010cern\u00e1, I., K\u0159et\u00ednsk\u00fd, J.: Modal transition systems: composition and LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 228\u2013242. Springer, Heidelberg (2011)"},{"key":"20_CR4","volume-title":"Concurrency Control and Recovery in Database Systems","author":"PA Bernstein","year":"1986","unstructured":"Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison-Wesley, Boston (1986)"},{"issue":"1\u20132","key":"20_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0167-6423(96)00027-5","volume":"29","author":"G Bruns","year":"1997","unstructured":"Bruns, G.: An industrial application of modal process logic. Sci. Comput. Program. 29(1\u20132), 3\u201322 (1997)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"20_CR6","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","volume":"2","author":"T Elrad","year":"1982","unstructured":"Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155\u2013173 (1982)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"20_CR7","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/357195.357200","volume":"5","author":"RG Gallager","year":"1983","unstructured":"Gallager, R.G., Humblet, P.A., Spira, P.M.: A distributed algorithm for minimum-weight spanning trees. ACM Trans. Program. Lang. Syst. 5(1), 66\u201377 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. In: ISTCS, pp. 130\u2013139 (1995)","DOI":"10.1109\/ISTCS.1995.377038"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-68863-1_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"A Gruler","year":"2008","unstructured":"Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113\u2013131. Springer, Heidelberg (2008)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: a foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155\u2013169. Springer, Heidelberg (2001)"},{"key":"20_CR11","unstructured":"Janssen, W.: Layered design of parallel systems. Ph.D. dissertation, Universiteit Twente (1994)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/3-540-58468-4_175","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"W Janssen","year":"1994","unstructured":"Janssen, W., Poel, M., Xu, Q., Zwiers, J.: Layering of real-time distributed processes. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 393\u2013417. Springer, Heidelberg (1994)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-54430-5_96","volume-title":"CONCUR \u201991","author":"W Janssen","year":"1991","unstructured":"Janssen, W., Poel, M., Zwiers, J.: Action systems and action refinement in the development of parallel systems - an algebraic approach. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 298\u2013316. Springer, Heidelberg (1991)"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Janssen, W., Zwiers, J.: From sequential layers to distributed processes: Deriving a distributed minimum weight spanning tree algorithm (extended anstract). In: PODC, pp. 215\u2013227. ACM (1992)","DOI":"10.1145\/135419.135461"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Kushilevitz, E., Rabin, M.O.: Randomized mutual exclusion algorithms revisited. In : PODC, pp. 275\u2013283 (1992)","DOI":"10.1145\/135419.135468"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"20_CR17","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)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-540-74407-8_8","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"KG Larsen","year":"2007","unstructured":"Larsen, K.G., Nyman, U., W\u0105sowski, A.: On modal refinement and consistency. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 105\u2013119. Springer, Heidelberg (2007)"},{"key":"20_CR19","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., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 17\u201340. Springer, Heidelberg (1995)"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203\u2013210 (1988)","DOI":"10.1109\/LICS.1988.5119"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS, pp. 108\u2013117 (1990)","DOI":"10.1109\/LICS.1990.113738"},{"issue":"1","key":"20_CR22","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.jlap.2007.10.005","volume":"76","author":"AK McIver","year":"2008","unstructured":"McIver, A.K., Gonzalia, C., Cohen, E., Morgan, C.C.: Using probabilistic Kleene algebra pKA for protocol verification. J. Log. Algebr. Program. 76(1), 90\u2013111 (2008)","journal-title":"J. Log. Algebr. Program."},{"key":"20_CR23","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)"},{"issue":"4","key":"20_CR24","doi-asserted-by":"publisher","first-page":"989","DOI":"10.1137\/S0097539799364006","volume":"31","author":"Y Moses","year":"2002","unstructured":"Moses, Y., Rajsbaum, S.: A layered analysis of consensus. SIAM J. Comput. 31(4), 989\u20131021 (2002)","journal-title":"SIAM J. Comput."},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-15297-9_18","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"E-R Olderog","year":"2010","unstructured":"Olderog, E.-R., Swaminathan, M.: Layered composition for timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 228\u2013242. Springer, Heidelberg (2010)"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/3-540-58179-0_69","volume-title":"Computer Aided Verification","author":"D Peled","year":"1994","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377\u2013390. Springer, Heidelberg (1994)"},{"key":"20_CR27","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.entcs.2008.06.023","volume":"215","author":"J-B Raclet","year":"2008","unstructured":"Raclet, J.-B.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93\u2013110 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Passerone, R.: Why are modalities good for interface theories? In: ACSD, pp. 119\u2013127 (2009)","DOI":"10.1109\/ACSD.2009.22"},{"key":"20_CR29","first-page":"53","volume":"33","author":"DA Schmidt","year":"2001","unstructured":"Schmidt, D.A.: From trace sets to modal-transition systems by stepwise abstract interpretation. Theoria 33, 53\u201371 (2001)","journal-title":"Theoria"},{"issue":"4\u20136","key":"20_CR30","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/s00165-012-0231-x","volume":"24","author":"M Swaminathan","year":"2012","unstructured":"Swaminathan, M., Katoen, J.-P., Olderog, E.-R.: Layered reasoning for randomized distributed algorithms. Formal Asp. Comput. 24(4\u20136), 477\u2013496 (2012)","journal-title":"Formal Asp. Comput."},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Uchitel, S., Chechik, M.: Merging partial behavioural models. In: SIGSOFT FSE, pp. 43\u201352 (2004)","DOI":"10.1145\/1041685.1029904"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07602-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T09:44:05Z","timestamp":1746265445000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-07602-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319076010","9783319076027"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07602-7_20","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":"13 June 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}