Verification of membrane systems with delays via Petri nets with delays

In this paper we verify certain properties of membrane systems through the use of specific techniques and a software tool developed for coloured Petri nets. We characterise some subclasses of membrane systems in which various qualitative properties (reachability, liveness) and quantitative properties (boundedness) are decidable. We establish a formal connection between membrane systems with delays and Petri nets with delays, and prove an operational correspondence between them. By assigning delays to rules and transitions, respectively, we make a distinction between the occurrence of the rule (transition) and its effects which become apparent after the delay. For both Petri nets and membrane systems we prove that adding finite delays does not increase their expressive power; however, both formalisms become more flexible in describing molecular phenomena where time represents a critical resource.