Strategy-Based Proof Calculus for Membrane Systems

In a previous work, we showed how rewrite strategies can be used for defining the semantics of membrane systems, in particular for expressing the different control mechanisms in membranes. The insufficient expressivity of the existing concept of rewrite strategies for describing certain control mechanisms for membranes lead us to defining a more generic concept of strategies.In this paper we introduce strategy-based rewriting logic which uses strategy controllers to reason at the higher level of computation given by the evolution of the membrane systems. We give a detailed presentation of the proof calculus, model theory, and completeness. A main consequence of the approach is that we get an algebraic semantics for membrane systems. Implementation issues are also discussed.