{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:19:23Z","timestamp":1745986763219,"version":"3.40.4"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031877742","type":"print"},{"value":"9783031877759","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-87775-9_30","type":"book-chapter","created":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T16:23:49Z","timestamp":1745943829000},"page":"356-367","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Local Model Checking on\u00a0an\u00a0IoT Based System: Use Case of\u00a0Cellular M2M in\u00a0Agriculture"],"prefix":"10.1007","author":[{"given":"Sawsen","family":"Khlifa","sequence":"first","affiliation":[]},{"given":"Chiheb Ameur","family":"Abid","sequence":"additional","affiliation":[]},{"given":"Asman Ben","family":"Letaifa","sequence":"additional","affiliation":[]},{"given":"Belhassen","family":"Zouari","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,4,30]]},"reference":[{"key":"30_CR1","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, p. 988. MIT Press, Cambridge. Massachusetts, London, UK (1999)"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models. ACPN 1996. Lecture Notes in Computer Science, vol. 1491. Springer, Heidelberg (1998)","DOI":"10.1007\/3-540-65306-6_21"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Couvreur, J.M.: On-the-fly verification of linear temporal logic. In: FM, ser. LNCS, vol. 1709. SV, pp. 253\u2013271 (1999)","DOI":"10.1007\/3-540-48119-2_16"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification Testing and Verification, p. 711 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 174\u2013190. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_12"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. In: Proceedings of Annual IEEE Symposium on Logic in Computer Science, LICS\u201991, pp. 406\u2013415. IEEE (1991)","DOI":"10.1109\/LICS.1991.151664"},{"issue":"4","key":"30_CR7","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Formal Meth. Syst. Des. 1(4), 297\u2013322 (1992)","journal-title":"Formal Meth. Syst. Des."},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Vernadat, F., Az\u00e9ma, P., Michel, F.: Covering step graph. In: International Conference on Application and Theory of Petri Nets, pp. 516\u2013535. Springer (1996)","DOI":"10.1007\/3-540-61363-3_28"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. Int. J. Software Tools Technol. Transf. 279\u2013287 (1999)","DOI":"10.1007\/s100090050035"},{"issue":"4","key":"30_CR10","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"JR Burch","year":"1994","unstructured":"Burch, J.R., et al.: Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4), 401\u2013424 (1994)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"30_CR11","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1186\/s13673-019-0165-x","volume":"9","author":"A Souri","year":"2019","unstructured":"Souri, A., Rahmani, A.M., Navimipour, N.J., et al.: A symbolic model checking approach in formal verification of distributed systems. Hum. Cent. Comput. Inf. Sci. 9, 4 (2019)","journal-title":"Hum. Cent. Comput. Inf. Sci."},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Abid, C.A., Klai, K., Arias, J., Ouni, H., SOG-based multi-core LTL model checking. In: IEEE International Conference on Parallel & Distributed Processing with Applications, Big Data & Cloud Computing, Sustainable Computing & Communications, Social Computing & Networking (ISPA, BDCloud, SocialCom, SustainCom): Exeter. United Kingdom 2020, 9\u201317 (2020)","DOI":"10.1109\/ISPA-BDCloud-SocialCom-SustainCom51426.2020.00028"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Rao, A., Wang, Y.: Formal Verification of Autonomous Vehicles: Bridging the Gap between Model-Based Design and Model Checking. In: SAE Technical Paper 2023-01-0116 (2023)","DOI":"10.4271\/2023-01-0116"},{"key":"30_CR14","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1613\/jair.4586","volume":"51","author":"P Kissmann","year":"2014","unstructured":"Kissmann, P., Hoffmann, J.: BDD ordering heuristics for classical planning. J. Artif. Intell. Res. 51, 779\u2013804 (2014)","journal-title":"J. Artif. Intell. Res."},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 677\u2013691. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_60"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"He, L., Liu, G., Sun, Y.: PNer: a petri-net-based model checker for computation tree logic. In IEEE International Conference on Networking, Sensing and Control (ICNSC), Marseille, France, pp. 1\u20137 (2023)","DOI":"10.1109\/ICNSC58704.2023.10319044"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Lakos, C., Petrucci, L.: Modular analysis of systems composed of semiautonomous. In: International Conference on Application of Concurrency to System Design, pp. 185\u2013196 (2004)","DOI":"10.1109\/CSD.2004.1309131"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Klai, K., Petrucci, L.: Modular construction of the symbolic observation graph. In: 8th International Conference on Application of Concurrency to System Design, Xi\u2019an, China, pp. 88\u201397 (2008)","DOI":"10.1109\/ACSD.2008.4574600"},{"issue":"4","key":"30_CR19","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1109\/TC.2009.187","volume":"59","author":"H Zheng","year":"2010","unstructured":"Zheng, H., Yao, H., Yoneda, T.: Modular model checking of large asynchronous designs with efficient abstraction refinement. IEEE Trans. Comput. 59(4), 561\u2013573 (2010)","journal-title":"IEEE Trans. Comput."},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Khlifa, S., Abid, C.A., Zouari, B.: A reduced distributed state space for modular petri Nets. In: Barolli, L. (eds.) Advanced Information Networking and Applications. AINA 2023. Lecture Notes in Networks and Systems, vol. 661. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-29056-5_29"},{"key":"30_CR21","first-page":"224","volume":"43","author":"S Christensen","year":"2000","unstructured":"Christensen, S., Petrucci, L.: Modular analysis of Petri Nets. Br. Comput. Soc.: Comput. J. 43, 224\u2013242 (2000)","journal-title":"Br. Comput. Soc.: Comput. J."},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Ouni, H., Abid, C.A., Zouari, B.: A distributed state space for modular Petri nets. In: 7th International Conference on Modelling, Identification and Control (2015)","DOI":"10.1109\/ICMIC.2015.7409394"},{"key":"30_CR23","unstructured":"Khlifa, S., Abid, C.A., Zouari, B.: Local model checking on a modular system. In: 10th International Conference on Control, Decision and Information Technologies (CoDIT), Valetta, Malta"},{"key":"30_CR24","doi-asserted-by":"crossref","unstructured":"Lucic, D., Caric, A., Lovrek, I.: Standardisation and regulatory context of machine-to-machine communication. In: 13th International Conference on Telecommunications (ConTEL), Graz, Austria, 2015, pp. 1\u20137 (2015)","DOI":"10.1109\/ConTEL.2015.7231216"}],"container-title":["Lecture Notes on Data Engineering and Communications Technologies","Advanced Information Networking and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-87775-9_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T16:24:05Z","timestamp":1745943845000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-87775-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031877742","9783031877759"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-87775-9_30","relation":{},"ISSN":["2367-4512","2367-4520"],"issn-type":[{"value":"2367-4512","type":"print"},{"value":"2367-4520","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 April 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"AINA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Advanced Information Networking and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 April 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"39","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aina0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/voyager.ce.fit.ac.jp\/conf\/aina\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}