Correspondence:
[*]
Address for correspondence: INRIA Rennes Bretagne Atlantique, Campus de Beaulieu, 35042 Rennes Cedex, France
Abstract: This paper considers Structured Data Nets (StDN): a Petri net extension that describes open systems with data. The objective of this language is to serve as a formal basis for the analysis of systems that use data, accept inputs from their environment, and implement complex workflows. 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 coverability, termination and soundness are undecidable for StDNs. 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. We then show the expressive power of StDN on a case study, and compare StDNs and their decidable subclasses with other types of high-level nets and other formalisms adapted to data-centric approaches or to workflows design.
Keywords: Petri nets, Well-Quasi Orders, Structured Data
