{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,24]],"date-time":"2026-01-24T01:25:34Z","timestamp":1769217934190,"version":"3.49.0"},"reference-count":60,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2021,2,12]],"date-time":"2021-02-12T00:00:00Z","timestamp":1613088000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ICT4V - Information and Communication Technologies for Verticals","award":["POS_ICT4V_2016_1_15"],"award-info":[{"award-number":["POS_ICT4V_2016_1_15"]}]},{"name":"ANII - Agencia Nacional de Investigaci\u00f3n e Innovaci\u00f3n","award":["FSDA_1_2018_1_154419"],"award-info":[{"award-number":["FSDA_1_2018_1_154419"]}]},{"name":"ANII - Agencia Nacional de Investigaci\u00f3n e Innovaci\u00f3n","award":["FMV_1_2019_1_155913"],"award-info":[{"award-number":["FMV_1_2019_1_155913"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["MAKE"],"abstract":"<jats:p>This paper presents a novel on-the-fly, black-box, property-checking through learning approach as a means for verifying requirements of recurrent neural networks (RNN) in the context of sequence classification. Our technique steps on a tool for learning probably approximately correct (PAC) deterministic finite automata (DFA). The sequence classifier inside the black-box consists of a Boolean combination of several components, including the RNN under analysis together with requirements to be checked, possibly modeled as RNN themselves. On one hand, if the output of the algorithm is an empty DFA, there is a proven upper bound (as a function of the algorithm parameters) on the probability of the language of the black-box to be nonempty. This implies the property probably holds on the RNN with probabilistic guarantees. On the other, if the DFA is nonempty, it is certain that the language of the black-box is nonempty. This entails the RNN does not satisfy the requirement for sure. In this case, the output automaton serves as an explicit and interpretable characterization of the error. Our approach does not rely on a specific property specification formalism and is capable of handling nonregular languages as well. Besides, it neither explicitly builds individual representations of any of the components of the black-box nor resorts to any external decision procedure for verification. This paper also improves previous theoretical results regarding the probabilistic guarantees of the underlying learning algorithm.<\/jats:p>","DOI":"10.3390\/make3010010","type":"journal-article","created":{"date-parts":[[2021,2,12]],"date-time":"2021-02-12T18:46:31Z","timestamp":1613155591000},"page":"205-227","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Property Checking with Interpretable Error Characterization for Recurrent Neural Networks"],"prefix":"10.3390","volume":"3","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1610-7334","authenticated-orcid":false,"given":"Franz","family":"Mayr","sequence":"first","affiliation":[{"name":"Facultad de Ingenier\u00eda, Universidad ORT Uruguay, 11100 Montevideo, Uruguay"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2737-4382","authenticated-orcid":false,"given":"Sergio","family":"Yovine","sequence":"additional","affiliation":[{"name":"Facultad de Ingenier\u00eda, Universidad ORT Uruguay, 11100 Montevideo, Uruguay"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramiro","family":"Visca","sequence":"additional","affiliation":[{"name":"Facultad de Ingenier\u00eda, Universidad ORT Uruguay, 11100 Montevideo, Uruguay"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2021,2,12]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2018.07.007","article-title":"Explanation in artificial intelligence: Insights from the social sciences","volume":"267","author":"Miller","year":"2019","journal-title":"Artif. Intell."},{"key":"ref_2","unstructured":"Biran, O., and Cotton, C.V. (August, January Australia). Explanation and Justification in Machine Learning: A Survey. Proceedings of the IJCAI Workshop on Explainable Artificial Intelligence (XAI), Melbourne."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Ahmad, M., Teredesai, A., and Eckert, C. (2018). Interpretable Machine Learning in Healthcare. Proceedings of the 2018 IEEE International Conference on Healthcare Informatics (ICHI), IEEE Computer Society.","DOI":"10.1109\/ICHI.2018.00095"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1038\/nature14539","article-title":"Deep learning","volume":"521","author":"LeCun","year":"2015","journal-title":"Nature"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Ribeiro, M.T., Singh, S., and Guestrin, C. (2016, January 13\u201317). \u201cWhy Should I Trust You?\u201d: Explaining the Predictions of Any Classifier. Proceedings of the SIGKDD Knowledge Discovery and Data Mining, San Francisco, CA, USA.","DOI":"10.1145\/2939672.2939778"},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Scheiner, N., Appenrodt, N., Dickmann, J., and Sick, B. (2019, January 9\u201312). Radar-based Road User Classification and Novelty Detection with Recurrent Neural Network Ensembles. Proceedings of the 2019 IEEE Intelligent Vehicles Symposium (IV), Paris, France.","DOI":"10.1109\/IVS.2019.8813773"},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Koci\u0107, J., Jovi\u010di\u0107, N., and Drndarevi\u0107, V. (2019). An End-to-End Deep Neural Network for Autonomous Driving Designed for Embedded Automotive Platforms. Sensors, 19.","DOI":"10.3390\/s19092064"},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Kim, J., Kim, J., Thu, H.L.T., and Kim, H. (2016, January 15\u201317). Long short term memory recurrent neural network classifier for intrusion detection. Proceedings of the 2016 International Conference on Platform Technology and Service (PlatCon), Jeju, Korea.","DOI":"10.1109\/PlatCon.2016.7456805"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"21954","DOI":"10.1109\/ACCESS.2017.2762418","article-title":"A deep learning approach for intrusion detection using recurrent neural networks","volume":"5","author":"Yin","year":"2017","journal-title":"IEEE Access"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Pascanu, R., Stokes, J.W., Sanossian, H., Marinescu, M., and Thomas, A. (2015, January 19\u201324). Malware classification with recurrent networks. Proceedings of the 2015 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), South Brisbane, QLD, Australia.","DOI":"10.1109\/ICASSP.2015.7178304"},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1016\/j.cose.2018.05.010","article-title":"Early Stage Malware Prediction Using Recurrent Neural Networks","volume":"77","author":"Rhode","year":"2017","journal-title":"Comput. Secur."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"46717","DOI":"10.1109\/ACCESS.2019.2906934","article-title":"Robust Intelligent Malware Detection Using Deep Learning","volume":"7","author":"Vinayakumar","year":"2019","journal-title":"IEEE Access"},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Singh, D., Merdivan, E., Psychoula, I., Kropf, J., Hanke, S., Geist, M., and Holzinger, A. (2017). Human activity recognition using recurrent neural networks. International Cross-Domain Conference for Machine Learning and Knowledge Extraction, Springer.","DOI":"10.1007\/978-3-319-66808-6_18"},{"key":"ref_14","first-page":"301","article-title":"Doctor AI: Predicting Clinical Events via Recurrent Neural Networks","volume":"Volume 56","author":"Fackler","year":"2016","journal-title":"Proceedings of the 1st Machine Learning for Healthcare Conference"},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1016\/j.jbi.2017.04.001","article-title":"Predicting healthcare trajectories from medical records: A deep learning approach","volume":"69","author":"Pham","year":"2017","journal-title":"J. Biomed. Inform."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"286","DOI":"10.3389\/fgene.2019.00286","article-title":"DeePromoter: Robust promoter predictor using deep learning","volume":"10","author":"Oubounyt","year":"2019","journal-title":"Front. Genet."},{"key":"ref_17","unstructured":"Clarke, E.M., Grumberg, O., and Peled, D.A. (1999). Model Checking, MIT Press."},{"key":"ref_18","unstructured":"Weiss, G., Goldberg, Y., and Yahav, E. (2018, January 10\u201315). Extracting Automata from Recurrent Neural Networks Using Queries and Counterexamples. Proceedings of the International Conference on Machine Learning ICML, PMLR, Stockholm, Sweden."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"2568","DOI":"10.1162\/neco_a_01111","article-title":"An Empirical Evaluation of Rule Extraction from Recurrent Neural Networks","volume":"30","author":"Wang","year":"2018","journal-title":"Neural Comput."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Wang, Q., Zhang, K., Ororbia, A.G., Xing, X., Liu, X., and Giles, C.L. (2018). A Comparison of Rule Extraction for Different Recurrent Neural Network Models and Grammatical Complexity. arXiv.","DOI":"10.1162\/neco_a_01111"},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Merrill, W. (2019). Sequential neural networks as automata. arXiv.","DOI":"10.18653\/v1\/W19-3901"},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Mayr, F., and Yovine, S. (2018). Regular Inference on Artificial Neural Networks. Machine Learning and Knowledge Extraction, Springer.","DOI":"10.1007\/978-3-319-99740-7_25"},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"1134","DOI":"10.1145\/1968.1972","article-title":"A Theory of the Learnable","volume":"27","author":"Valiant","year":"1984","journal-title":"Commun. ACM"},{"key":"ref_24","unstructured":"Odena, A., Olsson, C., Andersen, D., and Goodfellow, I.J. (2019, January 9\u201315). TensorFuzz: Debugging Neural Networks with Coverage-Guided Fuzzing. Proceedings of the International Conference on Machine Learning ICML, PMLR, Long Beach, CA, USA."},{"key":"ref_25","first-page":"343","article-title":"On-the-fly Black-Box Probably Approximately Correct Checking of Recurrent Neural Networks","volume":"Volume 12279","author":"Holzinger","year":"2020","journal-title":"Proceedings of the 4th IFIP TC 5, TC 12, WG 8.4, WG 8.9, WG 12.9 International Cross-Domain Conference on Machine Learning and Knowledge Extraction (CD-MAKE 2020)"},{"key":"ref_26","first-page":"225","article-title":"Black box checking","volume":"7","author":"Peled","year":"2002","journal-title":"J. Autom. Lang. Comb."},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Angluin, D. (1992, January 4\u20136). Computational Learning Theory: Survey and Selected Bibliography. Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing, Victoria, BC, Canada.","DOI":"10.1145\/129712.129746"},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Ben-David, S., and Shalev-Shwartz, S. (2014). Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press.","DOI":"10.1017\/CBO9781107298019"},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","article-title":"Learning Regular Sets from Queries and Counterexamples","volume":"75","author":"Angluin","year":"1987","journal-title":"Inf. Comput."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Siegelmann, H.T., and Sontag, E.D. (1992, January 4\u20136). On the Computational Power of Neural Nets. Proceedings of the twenty-fourth annual ACM symposium on Theory of Computing, Victoria, BC, Canada.","DOI":"10.1145\/130385.130432"},{"key":"ref_31","unstructured":"Suzgun, M., Belinkov, Y., and Shieber, S.M. (2018). On Evaluating the Generalization of LSTM Models in Formal Languages. arXiv."},{"key":"ref_32","unstructured":"Heinz, J., de la Higuera, C., and van Zaanen, M. (2011, January 10\u201313). Formal and Empirical Grammatical Inference. Proceedings of the ACL Annual Meeting, ACL, Minneapolis, MN, USA."},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","article-title":"Long Short-Term Memory","volume":"9","author":"Hochreiter","year":"1997","journal-title":"Neural Comput."},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Hao, Y., Merrill, W., Angluin, D., Frank, R., Amsel, N., Benz, A., and Mendelsohn, S. (2018). Context-free transductions with neural stacks. arXiv.","DOI":"10.18653\/v1\/W18-5433"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1145\/568438.568455","article-title":"Introduction to automata theory, languages, and computation","volume":"32","author":"Hopcroft","year":"2001","journal-title":"ACM Sigact News"},{"key":"ref_36","unstructured":"Tomita, M. (2006, January 26\u201329). Dynamic Construction of Finite Automata from examples using Hill-climbing. Proceedings of the Fourth Annual Conference of the Cognitive Science Society, Vancouver, BC, Canada."},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Meinke, K., and Sindhu, M.A. (2013, January 18\u201322). LBTest: A Learning-Based Testing Tool for Reactive Systems. Proceedings of the 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, Luxembourg.","DOI":"10.1109\/ICST.2013.62"},{"key":"ref_38","unstructured":"Merten, M. (2013). Active Automata Learning for Real Life Applications. [Ph.D. Thesis, Technischen Universit\u00e4t Dortmund]."},{"key":"ref_39","doi-asserted-by":"crossref","unstructured":"Du, M., Li, F., Zheng, G., and Srikumar, V. (November, January 30). DeepLog: Anomaly Detection and Diagnosis from System Logs through Deep Learning. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA.","DOI":"10.1145\/3133956.3134015"},{"key":"ref_40","first-page":"1137","article-title":"A Neural Probabilistic Language Model","volume":"3","author":"Bengio","year":"2003","journal-title":"J. Mach. Learn. Res."},{"key":"ref_41","unstructured":"Craven, M.W. (1996). Extracting Comprehensible Models from Trained Neural Networks. [Ph.D. Thesis, The University of Wisconsin]. AAI9700774."},{"key":"ref_42","doi-asserted-by":"crossref","unstructured":"Cobleigh, J.M., Giannakopoulou, D., and P\u0103s\u0103reanu, C.S. (2003). Learning assumptions for compositional verification. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer.","DOI":"10.1007\/3-540-36577-X_24"},{"key":"ref_43","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P., and Nam, W. (2005). Symbolic compositional verification by learning assumptions. Proceedings of the International Conference on Computer Aided Verification, Springer.","DOI":"10.1007\/11513988_52"},{"key":"ref_44","doi-asserted-by":"crossref","unstructured":"Feng, L., Han, T., Kwiatkowska, M., and Parker, D. (2011). Learning-based compositional verification for synchronous probabilistic systems. Proceedings of the International Symposium on Automated Technology for Verification and Analysis, Springer.","DOI":"10.1007\/978-3-642-24372-1_40"},{"key":"ref_45","doi-asserted-by":"crossref","unstructured":"Vardhan, A., Sen, K., Viswanathan, M., and Agha, G. (2004). Actively learning to verify safety for FIFO automata. Foundations of Software Technology and Theoretical Computer Science, Springer.","DOI":"10.1007\/978-3-540-30482-1_26"},{"key":"ref_46","first-page":"21","article-title":"Regular Model Checking Using Inference of Regular Languages","volume":"138","author":"Habermehl","year":"2004","journal-title":"ENTCS"},{"key":"ref_47","unstructured":"Trakhtenbrot, B.A., and Barzdin, I.M. (1973). Finite Automata: Behavior and Synthesis, North-Holland."},{"key":"ref_48","doi-asserted-by":"crossref","unstructured":"Meinke, K. (2018). Learning-based testing: Recent progress and future prospects. Machine Learning for Dynamic Software Analysis: Potentials and Limits, Springer.","DOI":"10.1007\/978-3-319-96562-8_2"},{"key":"ref_49","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/s11334-019-00342-6","article-title":"Sound black-box checking in the LearnLib","volume":"15","author":"Meijer","year":"2019","journal-title":"Innov. Syst. Softw. Eng."},{"key":"ref_50","doi-asserted-by":"crossref","first-page":"117","DOI":"10.3233\/AIC-2012-0525","article-title":"Challenging SMT solvers to verify neural networks","volume":"25","author":"Pulina","year":"2012","journal-title":"AI Commun."},{"key":"ref_51","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","article-title":"Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks","volume":"Volume 10426","author":"Katz","year":"2017","journal-title":"Proceedings of the International Conference on Computer Aided Verification"},{"key":"ref_52","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","article-title":"Safety Verification of Deep Neural Networks","volume":"Volume 10426","author":"Huang","year":"2017","journal-title":"Proceedings of the International Conference on Computer Aided Verification"},{"key":"ref_53","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/978-3-319-68167-2_19","article-title":"Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks","volume":"Volume 10482","author":"Ehlers","year":"2017","journal-title":"Proceedings of the International Symposium on Automated Technology for Verification and Analysis"},{"key":"ref_54","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-030-01090-4_1","article-title":"DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks","volume":"Volume 11138","author":"Lahiri","year":"2018","journal-title":"Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018)"},{"key":"ref_55","doi-asserted-by":"crossref","unstructured":"Wicker, M., Huang, X., and Kwiatkowska, M. (2018). Feature-guided black-box safety testing of deep neural networks. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer.","DOI":"10.1007\/978-3-319-89960-2_22"},{"key":"ref_56","unstructured":"Wang, Q., Zhang, K., Liu, X., and Giles, C.L. (2019, January 25\u201327). Verification of Recurrent Neural Networks Through Rule Extraction. Proceedings of the AAAI Spring Symposium on Verification of Neural Networks (VNN19), Stanford, CA, USA."},{"key":"ref_57","unstructured":"Kevorchian, A. (2018). Verification of Recurrent Neural Networks. [Master\u2019s Thesis, Imperial College London]."},{"key":"ref_58","doi-asserted-by":"crossref","unstructured":"Akintunde, M.E., Kevorchian, A., Lomuscio, A., and Pirovano, E. (2019, January 7\u201312). Verification of RNN-Based Neural Agent-Environment Systems. Proceedings of the AAAI Conference on Artificial Intelligence, AAAI, New York, NY, USA.","DOI":"10.1609\/aaai.v33i01.33016006"},{"key":"ref_59","doi-asserted-by":"crossref","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., and Grosu, R. (2019). Statistical Model Checking. Computing and Software Science: State of the Art and Perspectives, Springer.","DOI":"10.1007\/978-3-319-91908-9_23"},{"key":"ref_60","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3158668","article-title":"A Survey of Statistical Model Checking","volume":"28","author":"Agha","year":"2018","journal-title":"ACM Trans. Model. Comput. Simul."}],"container-title":["Machine Learning and Knowledge Extraction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2504-4990\/3\/1\/10\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T05:23:10Z","timestamp":1760160190000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2504-4990\/3\/1\/10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,12]]},"references-count":60,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2021,3]]}},"alternative-id":["make3010010"],"URL":"https:\/\/doi.org\/10.3390\/make3010010","relation":{},"ISSN":["2504-4990"],"issn-type":[{"value":"2504-4990","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,2,12]]}}}