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
Type de document :
Article dans une revue
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
Liste complète des métadonnées

https://hal.inria.fr/hal-01379245
Contributeur : Loic Helouet <>
Soumis le : mardi 11 octobre 2016 - 12:04:17
Dernière modification le : mardi 28 août 2018 - 10:24:07

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

387