Spiking Neural P(SN P) system with anti-spikes uses two types of objects called spikes and anti-spikes which can encode binary digits in a natural way. We propose a formal method based on Petri nets, which provides a natural and powerful framework to formalize SN P systems with anti-spikes. This enables the use of existing tools for Petri nets to study the computability and behavioural properties of SN P systems with anti-spikes. © 2012 ICST Institute for Computer Science, Social Informatics and Telecommunications Engineering.