The paper presents a matrix representation notation for spiking neural P systems allowing to investigate various properties of these systems. Some Petri net-like properties are specified in this context. A method based on the translation of spiking neural P systems into kernel P systems is used to formally verify such properties.