Formal Methods in Software Engineering

Strategy-Based Proof Calculus for Membrane Systems

Year2009
TypeConference
StatusPostproceedings
AuthorsOana Andrei, Dorel Lucanu

Links

Abstract

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.

BibTeX

@article{AndreiL09, author = {Oana Andrei and Dorel Lucanu}, title = {Strategy-Based Proof Calculus for Membrane Systems}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {238}, number = {3}, year = {2009}, pages = {23-43}, publisher = {Elsevier}, url = {wrla08.cs.uiuc.edu [WRLA 2008]}, url_publisher = {http://www.sciencedirect.com/science/article/pii/S1571066109001339} }