{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:50:24Z","timestamp":1750308624466,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"8","license":[{"start":{"date-parts":[[2023,6,28]],"date-time":"2023-06-28T00:00:00Z","timestamp":1687910400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Knowl. Discov. Data"],"published-print":{"date-parts":[[2023,9,30]]},"abstract":"<jats:p>In last years, we are witnessing a growing interest in the application of supervised machine learning techniques in the most disparate fields. One winning factor of machine learning is represented by its ability to easily create models, as it does not require prior knowledge about the application domain. Complementary to machine learning are formal methods, that intrinsically offer safeness check and mechanism for reasoning on failures. Considering the weaknesses of machine learning, a new challenge could be represented by the use of formal methods. However, formal methods require the expertise of the domain, knowledge about modeling language with its semantic and mathematical rigour to specify properties. In this article, we propose a novel learning technique based on the adoption of formal methods for classification thanks to the automatic generation both of the formula and of the model. In this way the proposed method does not require any human intervention and thus it can be applied also to complex\/large datasets. This leads to less effort both in using formal methods and in a better explainability and reasoning about the obtained results. Through a set of case studies from different real-world domains (i.e., driver detection, scada attack identification, arrhythmia characterization, mobile malware detection, and radiomics for lung cancer analysis), we demonstrate the usefulness of the proposed method, by showing that we are able to overcome the performances obtained from widespread classification algorithms.<\/jats:p>","DOI":"10.1145\/3592796","type":"journal-article","created":{"date-parts":[[2023,4,14]],"date-time":"2023-04-14T14:00:59Z","timestamp":1681480859000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Novel Classification Technique based on Formal Methods"],"prefix":"10.1145","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0049-1279","authenticated-orcid":false,"given":"Gerardo","family":"Canfora","sequence":"first","affiliation":[{"name":"Department of Engineering, University of Sannio"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9425-1657","authenticated-orcid":false,"given":"Francesco","family":"Mercaldo","sequence":"additional","affiliation":[{"name":"Department of Medicine and Health Sciences \u201cVincenzo Tiberio\u201d, University of Molise"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2634-4456","authenticated-orcid":false,"given":"Antonella","family":"Santone","sequence":"additional","affiliation":[{"name":"Department of Medicine and Health Sciences \u201cVincenzo Tiberio\u201d, University of Molise"}]}],"member":"320","published-online":{"date-parts":[[2023,6,28]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/319382.319388"},{"key":"e_1_3_2_3_2","volume-title":"The Discipline of Machine Learning","author":"Mitchell Tom Michael","year":"2006","unstructured":"Tom Michael Mitchell. 2006. The Discipline of Machine Learning. Carnegie Mellon University, School of Computer Science, Machine Learning ...."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3132724"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1080\/03155986.1988.11732068"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.07.015"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205179"},{"key":"e_1_3_2_8_2","first-page":"197","volume-title":"Proceedings of the International Conference on Concurrency","author":"Milner Robin","year":"1984","unstructured":"Robin Milner. 1984. Lectures on a calculus for communicating systems. In Proceedings of the International Conference on Concurrency. Springer, 197\u2013220."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1090\/dimacs\/031\/06"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2006.03.003"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270- 014-0416-2"},{"key":"e_1_3_2_12_2","first-page":"2","volume-title":"Proceedings of the Concurrency: Theory, Language, and Architecture","author":"Stirling Colin","year":"1989","unstructured":"Colin Stirling. 1989. An introduction to modal and temporal logics for CCS. In Proceedings of the Concurrency: Theory, Language, and Architecture. 2\u201320."},{"key":"e_1_3_2_13_2","volume-title":"Communication and Concurrency","author":"Milner Robin","year":"1989","unstructured":"Robin Milner. 1989. Communication and Concurrency. Prentice Hall."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_87"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-1-55860-377-6.50032-3"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1155\/2018\/1758731"},{"key":"e_1_3_2_17_2","first-page":"1","article-title":"A \u201cpay-how-you-drive\u201d car insurance approach through cluster analysis","author":"Carfora Maria Francesca","year":"2018","unstructured":"Maria Francesca Carfora, Fabio Martinelli, Francesco Mercaldo, Vittoria Nardone, Albina Orlando, Antonella Santone, and Gigliola Vaglini. 2018. A \u201cpay-how-you-drive\u201d car insurance approach through cluster analysis. Soft Computing 23, 13 (2018), 1\u201313.","journal-title":"Soft Computing"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1061\/(ASCE)WR.1943-5452.0000969"},{"key":"e_1_3_2_19_2","article-title":"ECG heartbeat classification: A deep transferable representation","author":"Kachuee Mohammad","year":"2018","unstructured":"Mohammad Kachuee, Shayan Fazeli, and Majid Sarrafzadeh. 2018. ECG heartbeat classification: A deep transferable representation. IEEE International Conference on Healthcare Informatics (ICHI\u201918), IEEE, 443\u2013444.","journal-title":"IEEE International Conference on Healthcare Informatics (ICHI\u201918)"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2014.23247"},{"key":"e_1_3_2_21_2","volume-title":"Proceedings of the 28th International ACM Symposium on Applied Computing","author":"Michael Spreitzenbarth","year":"2013","unstructured":"Spreitzenbarth Michael, Echtler Florian, Schreck Thomas, C. Freiling Felix, and Johannes Hoffmann. 2013. Mobilesandbox: Looking deeper into android applications. In Proceedings of the 28th International ACM Symposium on Applied Computing."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2019.101691"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.3390\/biology10020089"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.3390\/diagnostics11101796"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/IJCNN.2019.8852169"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"Steven L. Salzberg. 1994. C4. 5: Programs for Machine Learning by J. Ross Quinlan . Morgan Kaufmann Publishers.","DOI":"10.1007\/BF00993309"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/502512.502529"},{"issue":"3","key":"e_1_3_2_28_2","first-page":"369","article-title":"Bayesian network classifiers in weka for version 3-5-7","volume":"11","author":"Bouckaert Remco R.","year":"2008","unstructured":"Remco R. Bouckaert. 2008. Bayesian network classifiers in weka for version 3-5-7. Artificial Intelligence Tools 11, 3 (2008), 369\u2013387.","journal-title":"Artificial Intelligence Tools"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-1-55860-377-6.50023-2"},{"key":"e_1_3_2_30_2","unstructured":"Chih-Chung Chang. 2001. LIBSVM: A library for support vector machines 2001. Retrieved from http:\/\/www.csie.ntu.edu.tw\/cjlin\/libsvm."},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2016.2585083"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_15"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-0266(199606)17:6<441::AID-SMJ819>3.0.CO;2-G"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45231-8_30"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/2124284.2124288"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-1733-7_30"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1467247.1467271"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34691-0_11"},{"key":"e_1_3_2_39_2","first-page":"147","volume-title":"Proceedings of the International Conference on Runtime Verification","author":"Asarin Eugene","year":"2011","unstructured":"Eugene Asarin, Alexandre Donz\u00e9, Oded Maler, and Dejan Nickovic. 2011. Parametric identification of temporal properties. In Proceedings of the International Conference on Runtime Verification. Springer, 147\u2013160."},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","unstructured":"Shichao Zhang and Jiaye Li. 2021. Knn classification with one-step computation. IEEE Transactions on Knowledge and Data Engineering IEEE.","DOI":"10.1109\/TKDE.2021.3119140"},{"key":"e_1_3_2_41_2","article-title":"Reachable distance function for KNN classification","author":"Zhang Shichao","year":"2022","unstructured":"Shichao Zhang, Jiaye Li, and Yangding Li. 2022. Reachable distance function for KNN classification. IEEE Transactions on Knowledge and Data Engineering 1, 1 (2022), 1\u201315.","journal-title":"IEEE Transactions on Knowledge and Data Engineering"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/TNNLS.2017.2673241"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-815480-9.00015-3"}],"container-title":["ACM Transactions on Knowledge Discovery from Data"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3592796","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3592796","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:07:46Z","timestamp":1750273666000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3592796"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,28]]},"references-count":42,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2023,9,30]]}},"alternative-id":["10.1145\/3592796"],"URL":"https:\/\/doi.org\/10.1145\/3592796","relation":{},"ISSN":["1556-4681","1556-472X"],"issn-type":[{"type":"print","value":"1556-4681"},{"type":"electronic","value":"1556-472X"}],"subject":[],"published":{"date-parts":[[2023,6,28]]},"assertion":[{"value":"2022-07-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-04-10","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}