{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T15:17:16Z","timestamp":1725981436169},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319941103"},{"type":"electronic","value":"9783319941110"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-94111-0_13","type":"book-chapter","created":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T15:07:44Z","timestamp":1529075264000},"page":"216-234","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Comparative Study of Decision Diagrams for Real-Time Model Checking"],"prefix":"10.1007","author":[{"given":"Omar","family":"Al-Bataineh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Rosenblum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,16]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.tcs.2016.12.020","volume":"665","author":"OI Al-Bataineh","year":"2017","unstructured":"Al-Bataineh, O.I., Reynolds, M., French, T.: Finding minimum and maximum termination time of timed automata models with cyclic behaviour. Theor. Comput. Sci. 665, 87\u2013104 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104, 2\u201334 (1993)","journal-title":"Inf. Comput."},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: Proceedings of the 5th Annual Symposium on Logic in Computer Science, pp. 414\u2013425 (1990)","DOI":"10.1109\/LICS.1990.113766"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. TCS 126, 183\u2013235 (1994)","journal-title":"TCS"},{"key":"13_CR5","first-page":"1","volume-title":"Lecture Notes in Computer Science","author":"Rajeev Alur","year":"2004","unstructured":"Alur, R., Madhusudan, P.: Decision problems for timed automata: a survey. In: International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, pp. 200\u2013236 (2004)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Atif, M.: Analysis and verification of two-phase commit and three-phase commit protocols. In: Emerging Technologies ICET 2009, pp. 326\u2013331 (2009)","DOI":"10.1109\/ICET.2009.5353152"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/s10009-005-0190-0","volume":"8","author":"G Behrmann","year":"2006","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Radek, P.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8, 204\u2013215 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification","author":"G Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341\u2013353. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_30"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"13_CR11","volume-title":"Concurrency Control and Recovery in Database Systems","author":"PA Bernstein","year":"1987","unstructured":"Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison-Wesley, Reading (1987)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-45069-6_13","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2003","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: a tool for BDD-based verification of real-time systems. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 122\u2013125. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_13"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-39979-7_13","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2003","author":"D Beyer","year":"2003","unstructured":"Beyer, D., Noack, A.: Can decision diagrams overcome state space explosion in real-time verification? In: K\u00f6nig, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 193\u2013208. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39979-7_13"},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1023\/B:FORM.0000026093.21513.31","volume":"24","author":"P Bouyer","year":"2004","unstructured":"Bouyer, P.: Forward analysis of updatable timed automata. Formal Meth. Syst. Des. 24, 281\u2013320 (2004)","journal-title":"Formal Meth. Syst. Des."},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35, 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"13_CR16","unstructured":"Davidson, S., Lee, I., Wolfe, V.: A protocol for times atomic commitment. In: Proceedings of 9th International Conference on Distributed Computing System (1989)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"DL Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197\u2013212. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_17"},{"key":"13_CR18","first-page":"394","volume":"111","author":"TA Henzinger","year":"1992","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111, 394\u2013406 (1992)","journal-title":"Inf. Comput."},{"key":"13_CR19","volume-title":"FDDI Handbook: High-Speed Networking Using Fiber and Other Media","author":"R Jain","year":"1994","unstructured":"Jain, R.: FDDI Handbook: High-Speed Networking Using Fiber and Other Media. Addison-Wesley Longman Publishing Co. Inc., Boston (1994)"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Kaynar, D., Lynch, N., Segala, R., Vaandrager, F.: Timed I\/O automata: a mathematical framework for modelling and analyzing real-time systems. In: Proceedings of 24th IEEE International Real-Time Systems Symposium (RTSS 2003), pp. 166\u2013177 (2003)","DOI":"10.1109\/REAL.2003.1253264"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structures and state-space reduction. In: Proceedings of the 18th IEEE Real-Time Systems Symposium, pp. 14\u201324 (1997)","DOI":"10.1109\/REAL.1997.641265"},{"key":"13_CR22","unstructured":"Magee, J.: Analyzing synchronous distributed algorithms (2003)"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-540-24732-6_9","volume-title":"Model Checking Software","author":"I Ober","year":"2004","unstructured":"Ober, I., Graf, S., Ober, I.: Validation of UML models via a mapping to communicating extended timed automata. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 127\u2013145. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24732-6_9"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Formal modeling and analysis of a distributed database protocol in Maude. In: Proceedings of the 2008 11th IEEE International Conference on Computational Science and Engineering - Workshops, pp. 37\u201344 (2008)","DOI":"10.1109\/CSEW.2008.30"},{"key":"13_CR25","unstructured":"Tripakis, S.: The analysis of timed systems in practice. Ph.D. thesis, Universite Joseph Fourier, Grenoble, France (1998)"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Wang, F.: Symbolic verification of complex real-time systems with clock-restriction diagram. In: Proceedings of the IFIP TC6\/WG6.1, pp. 235\u2013250. Kluwer, B.V. (2001)","DOI":"10.1007\/0-306-47003-9_15"},{"key":"13_CR27","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine, S.: Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transfer 1, 123\u2013133 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94111-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T10:24:16Z","timestamp":1571480656000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94111-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319941103","9783319941110"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94111-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}