Petri nets with structured data

Abstract

This paper proposes Structured Data Nets (StDN), a Petri net extension that describes transactional systems with data. In StDNs, tokens are structured documents. Each transition is attached to a query, guarded by patterns, (logical assertions on the contents of its preset) and transforms tokens. We define StDNs and their semantics. We then consider their formal properties: coverability of a marking, termination and soundness of transactions. Unrestricted StDNs are Turing complete, so these properties are undecidable. We thus use an order on documents, and show that under reasonable restrictions on documents and on the expressiveness of patterns and queries, StDNs are well-structured transition system, for which coverability, termination and soundness are decidable.