{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T10:20:27Z","timestamp":1752229227986,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662630785"},{"type":"electronic","value":"9783662630792"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","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":[[2021]]},"DOI":"10.1007\/978-3-662-63079-2_8","type":"book-chapter","created":{"date-parts":[[2021,2,24]],"date-time":"2021-02-24T13:04:14Z","timestamp":1614171854000},"page":"165-183","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verification of the MQTT IoT Protocol Using Property-Specific CTL Sweep-Line Algorithms"],"prefix":"10.1007","author":[{"given":"Alejandro","family":"Rodr\u00edguez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars Michael","family":"Kristensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adrian","family":"Rutle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,2,25]]},"reference":[{"key":"8_CR1","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"8_CR2","unstructured":"Banks, A., Gupta, R.: MQTT Version 3.1.1. OASIS Stand. 29, 89 (2014). http:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v3.1.1\/mqtt-v3.1.1.html"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Cheng, A., Christensen, S., Mortensen, K.H.: Model checking coloured petri nets - exploiting strongly connected components. DAIMI Rep. Ser. 26, 519 (1997)","DOI":"10.7146\/dpb.v26i519.7048"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-45319-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Christensen","year":"2001","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450\u2013464. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_31"},{"key":"8_CR5","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). https:\/\/doi.org\/10.1007\/BFb0025774"},{"issue":"2","key":"8_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM 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 Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"3","key":"8_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. Int. J. Softw. Tools Technol. Transf. 2(3), 279\u2013287 (1999)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1\u201330. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35746-6_1"},{"key":"8_CR9","unstructured":"CPN tools. http:\/\/cpntools.org\/"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31131-4_14","volume-title":"Application and Theory of Petri Nets","author":"S Evangelista","year":"2012","unstructured":"Evangelista, S., Kristensen, L.M.: Hybrid on-the-fly LTL model checking with the sweep-line method. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 248\u2013267. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31131-4_14"},{"key":"8_CR11","unstructured":"Iwashita, H., Nakata, T., Hirose, F.: CTL model checking based on forward state traversal. In: Proceedings of International Conference on Computer Aided Design, pp. 82\u201387. IEEE Computer Society (1996)"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.tcs.2011.12.036","volume":"429","author":"K Jensen","year":"2012","unstructured":"Jensen, K., Kristensen, L., Mailund, T.: The sweep-line state space exploration method. Theor. Comput. Sci. 429, 169\u2013179 (2012)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"8_CR13","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. 9(3), 213\u2013254 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/3-540-45614-7_31","volume-title":"FME 2002:Formal Methods\u2014Getting IT Right","author":"LM Kristensen","year":"2002","unstructured":"Kristensen, L.M., Mailund, T.: A generalised sweep-line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 549\u2013567. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45614-7_31"},{"issue":"3","key":"8_CR15","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1023\/B:LISP.0000029445.29210.ca","volume":"17","author":"LM Kristensen","year":"2004","unstructured":"Kristensen, L.M., Christensen, S.: Implementing coloured petri nets using a functional programming language. Higher-order Symbolic Comput. 17(3), 207\u2013243 (2004)","journal-title":"Higher-order Symbolic Comput."},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-030-21571-2_18","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"T Liebke","year":"2019","unstructured":"Liebke, T., Wolf, K.: Taking some burden off an explicit CTL model checker. In: Donatelli, S., Haar, S. (eds.) PETRI NETS 2019. LNCS, vol. 11522, pp. 321\u2013341. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-21571-2_18"},{"key":"8_CR17","unstructured":"Lilleskare, A., Kristensen, L.M., H\u00f8yland, S.-O.: CTL model checking with the sweep-line state space exploration method. In: Proceedings of Norwegian Informatics Conference (NIK) (2017)"},{"key":"8_CR18","unstructured":"MQTT essentials part 3: Client, broker and connection establishment. https:\/\/www.hivemq.com\/blog\/mqtt-essentials-part2-publish-subscribe"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-662-60651-3_5","volume-title":"Transactions on Petri Nets and Other Models of Concurrency XIV","author":"A Rodr\u00edguez","year":"2019","unstructured":"Rodr\u00edguez, A., Kristensen, L.M., Rutle, A.: Formal modelling and incremental verification of the MQTT IoT protocol. In: Koutny, M., Pomello, L., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency XIV. LNCS, vol. 11790, pp. 126\u2013145. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-662-60651-3_5"},{"key":"8_CR20","unstructured":"Rodriguez, A., Kristensen, L.M., Rutle, A.: On CTL model checking of the MQTT IoT protocol using the sweep-line method. In: Petri Nets and Software Engineering. International Workshop, PNSE 19, Aachen, Germany, June 24, 2019, volume 2424 of CEUR Workshop Proceedings, pp. 57\u201372 (2019)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/3-540-60385-9_13","volume-title":"Correct Hardware Design and Verification Methods","author":"U Stern","year":"1995","unstructured":"Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 206\u2013224. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60385-9_13"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Valmari, A.: The state explosion problem. In: Advanced Course on Petri Nets, pp. 429\u2013528. Springer (1996)","DOI":"10.1007\/3-540-65306-6_21"},{"key":"8_CR23","unstructured":"Van\u00a0Leeuwen, J., Leeuwen, J.: Handbook of Theoretical Computer Science, vol. 1. Mit Press, Elsevier (1990)"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MY Vardi","year":"2001","unstructured":"Vardi, M.Y.: Branching vs. Linear time: final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1\u201322. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_1"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency XV"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-63079-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,27]],"date-time":"2021-03-27T18:03:31Z","timestamp":1616868211000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-63079-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783662630785","9783662630792"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-63079-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"25 February 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}