Projects I am currently involved in are:
We have defined an operational semantics of a basic class of P systems and we implemented it using rewriting logic. The structure and behavior of a P system is described by means of an executable specifications in Maude, a software system supporting rewriting and equational logic. We can verify properties of the system expressed as linear temporal logic formulas by using the model checker implemented in Maude. Within this project, I had a major role in defining and implementing the inference rules. This work was done in the context of my Master thesis.