Verifying a P system generating squares

Abstract

In [1], an example of a P system generating exactly all the squares of natural numbers greater than 1 is given. Nevertheless, only an informal reasoning of this result is presented. In this paper we study a similar P system to it (only one evolution rule is modified). A formalization of the syntax of the P system following [3] is given, and we state the verification of the given P system through soundness and completeness: (a) every successful computation of the P system generate a square greater or equal to 1 (soundness); (b) every natural number greater or equal to 1 is the output of a successful computation of the system (completeness). Then we establish the formal verification through the study of the critical points of the computations of the P system that give to us important information to characterize the successful computations.