On Model-Checking of P Systems