Abstract : This paper considers Structured Data Nets (StDN): a Petri net extension that describes
transactional systems with data. In StDNs, tokens are structured documents. Each transition is at-
tached 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. However, using an order on documents, and putting reasonable
restrictions both on the expressiveness of patterns and queries and on the documents, we show that
StDNs are well-structured transition systems, for which coverability, termination and soundness are
decidable.
