{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:52:52Z","timestamp":1725490372061},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540741275"},{"type":"electronic","value":"9783540741282"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74128-2_1","type":"book-chapter","created":{"date-parts":[[2007,8,27]],"date-time":"2007-08-27T06:05:15Z","timestamp":1188194715000},"page":"1-18","source":"Crossref","is-referenced-by-count":8,"title":["A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis"],"prefix":"10.1007","author":[{"given":"Piergiorgio","family":"Bertoli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Bozzano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"\u00c5kerlund, O., Bieber, P., B\u00f6ede, E., Bozzano, M., Bretschneider, M., Castel, C., Cavallo, A., Cifaldi, M., Gauthier, J., Griffault, A., Lisagor, O., L\u00fcdtke, A., Metge, S., Papadopoulos, C., Peikenkamp, T., Sagaspe, L., Seguin, C., Trivedi, H., Valacca, L.: ISAAC, a framework for integrated safety analysis of functional, geometrical and human aspects. In: Proc. European Congress on Embedded Real Time Software (ERTS 2006) (2006)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/11875567_10","volume-title":"Computer Safety, Reliability, and Security","author":"R. Banach","year":"2006","unstructured":"Banach, R., Bozzano, M.: Retrenchment, and the Generation of Fault Trees for Static, Dynamic and Cyclic Systems. In: Gorski, J. (ed.) SAFECOMP 2006. LNCS, vol.\u00a04166, pp. 127\u2013141. Springer, Heidelberg (2006)"},{"key":"1_CR3","unstructured":"Bertoli, P., Cimatti, A., Pistore, M.: Strong Cyclic Planning under Partial Observability. In: Proc. of 17th European Conference on Artificial Intelligence (ECAI 2006) (2006)"},{"key":"1_CR4","unstructured":"Bertoli, P., Cimatti, A., Pistore, M., Traverso, P.: A Framework for Planning with Extended Goals under Partial Observability. In: Proc. International Conference on Automated Planning and Scheduling (ICAPS 2003) (2003)"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/j.artint.2006.01.004","volume":"170","author":"P. Bertoli","year":"2006","unstructured":"Bertoli, P., Cimatti, A., Roveri, M., Traverso, P.: Strong Planning under Partial Observability. Artificial Intelligence\u00a0170, 337\u2013384 (2006)","journal-title":"Artificial Intelligence"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1145\/309847.309942","volume-title":"Proceedings of the 36th Design Automation Conference (DAC 1999)","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic Model Checking Using SAT Procedures instead of BDDs. In: Proceedings of the 36th Design Automation Conference (DAC 1999), New Orleans, LA, USA, pp. 317\u2013320. ACM Press, New York (1999)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"1_CR8","unstructured":"Bonet, B., Geffner, H.: Planning with Incomplete Information as Heuristic Search in Belief Space. In: Proc. 5th International Conference on Artificial Intelligence Planning and Scheduling (AIPS 2000), pp. 52\u201361 (2000)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-540-45236-2_13","volume-title":"FME 2003: Formal Methods","author":"M. Bozzano","year":"2003","unstructured":"Bozzano, M., Cavallo, A., Cifaldi, M., Valacca, L., Villafiorita, A.: Improving Safety Assessment of Complex Systems: An industrial case study. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 208\u2013222. Springer, Heidelberg (2003)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Villafiorita, A.: The FSAP\/NuSMV-SA Safety Analysis Platform. International Journal on Software Tools for Technology Transfer, 2006. DOI 10.1007\/s10009-006-0001-2 (to appear)","DOI":"10.1007\/s10009-006-0001-2"},{"key":"1_CR11","unstructured":"Bozzano, M., Villafiorita, A., \u00c5kerlund, O., Bieber, P., Bougnol, C., B\u00f6de, E., Bretschneider, M., Cavallo, A., Castel, C., Cifaldi, M., Cimatti, A., Griffault, A., Kehren, C., Lawrence, B., L\u00fcdtke, A., Metge, S., Papadopoulos, C., Passarello, R., Peikenkamp, T., Persson, P., Seguin, C., Trotta, L., Valacca, L., Zacco, G.: ESACS: An Integrated Methodology for Design and Safety Analysis of Complex Systems. In: Proc. European Safety and Reliability Conference (ESREL 2003), pp. 237\u2013245. Balkema Publisher, 2003"},{"issue":"8","key":"1_CR12","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"issue":"3","key":"1_CR13","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"issue":"4","key":"1_CR14","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a013(4), 401\u2013424 (1994)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"1_CR17","first-page":"363","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 2003)","author":"A. Cimatti","year":"2003","unstructured":"Cimatti, A., Pecheur, C., Cavada, R.: Formal Verification of Diagnosability via Symbolic Model Checking. In: Gottlob, G., Walsh, T. (eds.) Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 2003), Acapulco, Mexico, pp. 363\u2013369. Morgan Kaufmann, San Francisco (2003)"},{"issue":"1-2","key":"1_CR18","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/S0004-3702(02)00374-0","volume":"147","author":"A. Cimatti","year":"2003","unstructured":"Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, Strong, and Strong Cyclic Planning via Symbolic Model Checking. Artificial Intelligence\u00a0147(1-2), 35\u201384 (2003)","journal-title":"Artificial Intelligence"},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.artint.2004.05.003","volume":"159","author":"A. Cimatti","year":"2004","unstructured":"Cimatti, A., Roveri, M., Bertoli, P.: Conformant Planning via Symbolic Model Checking and Heuristic Search. Artificial Intelligence\u00a0159, 127\u2013206 (2004)","journal-title":"Artificial Intelligence"},{"key":"1_CR20","volume-title":"Proc. 4th International Conference on Artificial Intelligence Planning Systems (AIPS- 1998)","author":"A. Cimatti","year":"1998","unstructured":"Cimatti, A., Roveri, M., Traverso, P.: Strong Planning in Non-Deterministic Domains via Model Checking. In: Proc. 4th International Conference on Artificial Intelligence Planning Systems (AIPS- 1998), Carnegie Mellon University, Pittsburgh, USA, AAAI-Press, Stanford, California, USA (1998)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, Springer, Heidelberg (1982)"},{"issue":"2","key":"1_CR22","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR23","unstructured":"Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D., McMillan, K.L., Ness, L.: Verification of the FUTUREBUS+ Cache Coherence Protocol. In: Proc. of 11th International Symposium on Computer Hardware Description Languages and their Applications (CHDL-1993) (1993)"},{"key":"1_CR24","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA (1999)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Proc. 12 th Intl. Conference on Computer Aided Verification (CAV 2001)","author":"F. Copty","year":"2001","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 436\u2013453. Springer, Heidelberg (2001)"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. of International Workshop on Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1989","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of Synchronous Sequential Machines Using Symbolic Execution. In: Proc. of International Workshop on Automatic Verification Methods for Finite State Systems. LNCS, vol.\u00a0407, Springer, Heidelberg (1989)"},{"key":"1_CR27","unstructured":"Coudert, O., Madre, J.C.: Fault Tree Analysis: 1020 Prime Implicants and Beyond. In: Proc. Annual Reliability and Maintainability Symposium (RAMS 1993) (1993)"},{"key":"1_CR28","unstructured":"Dal Lago, U., Pistore, M., Traverso, P.: Planning with a Language for Extended Goals. In: Proc. 18th National Conference on Artificial Intelligence (AAAI 2002) (2002)"},{"key":"1_CR29","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1109\/ICCD.1992.276232","volume-title":"International Conference on Computer Design, VLSI in Computers and Processors","author":"D.L. Dill","year":"1992","unstructured":"Dill, D.L., Drexler, A J., Hu, A.J., Yang, C.H.: Protocol Verification as a Hardware Design Aid. In: International Conference on Computer Design, VLSI in Computers and Processors, pp. 522\u2013525. IEEE Computer Society Press, Los Alamitos, Ca., USA (October 1992)"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"E\u00e8n, N., S\u00f6rensson, N.: An extensible sat solver. In: Proc. of the 6th International Conference on Theory and Applications of Satisfiability Testing, pp. 502\u2013518 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"1_CR31","volume-title":"Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics","author":"E. Emerson","year":"1990","unstructured":"Emerson, E.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. B, Formal Models and Semantics, Elsevier, Amsterdam (1990)"},{"key":"1_CR32","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/0004-3702(71)90010-5","volume":"2","author":"R.E. Fikes","year":"1971","unstructured":"Fikes, R.E., Nilsson, N.J.: STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. Artificial Intelligence\u00a02, 187\u2013208 (1971)","journal-title":"Artificial Intelligence"},{"key":"1_CR33","unstructured":"The FSAP platform. http:\/\/sra.itc.it\/tools\/FSAP"},{"key":"1_CR34","series-title":"1","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/B978-155860856-6\/50005-3","volume-title":"Automated Planning: Theory and Practice","author":"M. Ghallab","year":"2004","unstructured":"Ghallab, M., Nau, D., Traverso, P.: Automated Planning: Theory and Practice. 1, pp. 17\u2013110. Morgan Kaufmann, Washington (2004)"},{"key":"1_CR35","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1109\/TCAD.2003.822105","volume":"23","author":"A. Gupta","year":"2004","unstructured":"Gupta, A., Clarke, E., Strichman, O.: Sat based counterexample-guided abstraction-refinement. IEEE Transactions on Computer Aided Design\u00a023, 1113\u20131123 (2004)","journal-title":"IEEE Transactions on Computer Aided Design"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer Aided Verification","author":"K. Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 98\u2013111. Springer, Heidelberg (2005)"},{"key":"1_CR37","first-page":"71","volume-title":"(ICAPS-2005)","author":"J. Hoffmann","year":"2005","unstructured":"Hoffmann, J., Brafman, R.: Contingent Planning via Heuristic Forward Search with Implicit Belief States. In (ICAPS-2005). Proc. of 15th International Conference on Automated Planning and Scheduling, Monterey, CA, USA, pp. 71\u201380. Kaufmann, San Francisco (2005)"},{"issue":"5","key":"1_CR38","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker Spin. IEEE Trans. on Software Engineering, Special issue on Formal Methods in Software Practice.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering, Special issue on Formal Methods in Software Practice."},{"issue":"8","key":"1_CR39","doi-asserted-by":"publisher","first-page":"1318","DOI":"10.1109\/9.940942","volume":"46","author":"S. Jiang","year":"2001","unstructured":"Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A polynomial algorithm for testing diagnosability of discrete event systems. IEEE Transactions on Automatic Control\u00a046(8), 1318\u20131321 (2001)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"1_CR40","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"1_CR41","unstructured":"The NuSMV model checker, http:\/\/nusmv.itc.it"},{"key":"1_CR42","unstructured":"Pistore, M., Traverso, P.: Planning as Model Checking for Extended Goals in Non-deterministic Domains. In: Proc. of 17th International Joint Conference on Artificial Intelligence (IJCAI-2001) (2001)"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Pixley, C.: A Computational Theory and Implementation of Sequential Hardware Equivalence. In: DIMACS Workshop on Computer Aided Verification \u201990, Providence, RI pp. 293\u2013320 (1990)","DOI":"10.1090\/dimacs\/003\/20"},{"key":"1_CR44","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M. Prasad","year":"2005","unstructured":"Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in sat-based formal verification. STTT\u00a0(7), 156\u2013173 (2005)","journal-title":"STTT"},{"key":"1_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol.\u00a0137, pp. 337\u2013371. Springer, Heidelberg (1982)"},{"issue":"3","key":"1_CR46","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0951-8320(93)90060-C","volume":"40","author":"A. Rauzy","year":"1993","unstructured":"Rauzy, A.: New Algorithms for Fault Trees Analysis. Reliability Engineering and System Safety\u00a040(3), 203\u2013211 (1993)","journal-title":"Reliability Engineering and System Safety"},{"key":"1_CR47","unstructured":"Rintanen, J.: Backward Plan Construction for Planning as Search in Belief Space. In: Proc. of 6th International Conference on Artificial Intelligence Planning and Scheduling (AIPS 2002), pp. 93\u2013102 (2002)"},{"issue":"9","key":"1_CR48","doi-asserted-by":"publisher","first-page":"1555","DOI":"10.1109\/9.412626","volume":"40","author":"M. Sampath","year":"1995","unstructured":"Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete-event systems. IEEE Transactions on Automatic Control\u00a040(9), 1555\u20131575 (1995)","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"2","key":"1_CR49","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1109\/87.486338","volume":"4","author":"M. Sampath","year":"1996","unstructured":"Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Failure diagnosis using discrete event models. IEEE Transactions on Control Systems\u00a04(2), 105\u2013124 (1996)","journal-title":"IEEE Transactions on Control Systems"},{"key":"1_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a sat-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, Springer, Heidelberg (2000)"},{"key":"1_CR51","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0951-8320(94)90095-7","volume":"43","author":"N.O. Siu","year":"1994","unstructured":"Siu, N.O.: Risk Assessment for Dynamic Systems: An Overview. Reliability Engineering and System Safety\u00a043, 43\u201374 (1994)","journal-title":"Reliability Engineering and System Safety"},{"key":"1_CR52","first-page":"130","volume-title":"Proc. of the IEEE International Conference on Computer-Aided Design","author":"H.J. Touati","year":"1990","unstructured":"Touati, H.J., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.: Implicit State Enumeration of Finite State Machines Using BDDs. In: Proc. of the IEEE International Conference on Computer-Aided Design, pp. 130\u2013133, Santa Clara, CA , IEEE Computer Society Press, Los Alamitos (November 1990)"},{"key":"1_CR53","unstructured":"Vesely, W.E., Goldberg, F.F., Roberts, N.H., Haasl, D.F.: Fault Tree Handbook. Technical Report NUREG-0492, Systems and Reliability Research Office of Nuclear Regulatory Research U.S. Nuclear Regulatory Commission (1981)"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74128-2_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T16:06:53Z","timestamp":1708186013000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74128-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540741275","9783540741282"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74128-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}