Petri Nets with Structured Data

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.
Keywords : Petri nets Data
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/hal-01379245
Contributor : Loic Helouet <>
Submitted on : Tuesday, October 11, 2016 - 12:04:17 PM
Last modification on : Tuesday, July 9, 2019 - 1:16:29 AM

Identifiers

  • HAL Id : hal-01379245, version 1

Citation

Eric Badouel, Christophe Morvan, Loïc Hélouët. Petri Nets with Structured Data . Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2016, Application and Theory of Petri Nets and Other Models of Concurrency: Special Issue of Selected Papers from Petri Nets 2015 146 (1), pp.119. ⟨hal-01379245⟩

Share

Metrics

Record views

461