Pérez Jiménez, Mario de JesúsValencia Cabrera, LuisOrellana Martín, DavidRamírez de Arellano Marrero, Antonio2025-05-262025-05-262024-10-01Pérez Jiménez, M.d.J., Valencia Cabrera, L., Orellana Martín, D. y Ramírez de Arellano Marrero, A. (2024). Towards a general methodology for formal verification on spiking neural P systems. TheiretucaL Computer Science, 1011, 114705. https://doi.org/10.1016/j.tcs.2024.114705.0304-39751879-2294https://hdl.handle.net/11441/173302P systems are non-deterministic, parallel and distributed models of computation inspired by the behaviour and structure of living cells. Spiking neural P systems synthesise the connections that exist between neurons in the human brain, using pulses as a form of transmission of information. Usually, when a spiking neural P system is defined to solve any problem, it is checked in several cases to know if it works for them. But this methodology is not sufficient to verify if the system always works in a correct way. In this work, we introduce a methodology to look for characteristics in computations of spiking neural P systems that can be used to formally verify that the model works as it is intended.application/pdf8 p.engAttribution 4.0 Internationalhttp://creativecommons.org/licenses/by/4.0/Membrane computingSpiking neural P systemsFormal verificationTowards a general methodology for formal verification on spiking neural P systemsinfo:eu-repo/semantics/articleinfo:eu-repo/semantics/openAccesshttps://doi.org/10.1016/j.tcs.2024.114705