Graph-Rewriting Petri Nets

Controlled graph rewriting enhances expressiveness of plain graph-rewriting systems (i.e., sets of graph-rewriting rules) by introducing additional constructs for explicitly controlling graph-rewriting rule applications. In this regard, a formal semantic foundation for controlled graph rewriting is inevitable as a reliable basis for tool-based specification and automated analysis of graph-based algorithms. Although several promising attempts have been proposed in the literature, a comprehensive theory of controlled graph rewriting capturing semantic subtleties of advanced control constructs provided by practical tools is still an open challenge. In this paper, we propose graph-rewriting Petri nets (GPN) as a novel foundation for unifying control-flow and rule-application semantics of controlled graph rewriting. GPN instantiate coloured Petri nets with categorical DPO-based graph-rewriting theory where token colours denote typed graphs and graph morphisms and transitions define templates for guarded graph-rewriting rule applications. Hence, GPN enjoy the rich body of specification and analysis techniques of Petri nets including inherent notions of concurrency. To demonstrate expressiveness of GPN, we present a case study by means of a topology-control algorithm for wireless sensor networks.