Petri Nets with Structured Data

• Autorzy: Badouel E. , Hélouët L. , Morvan C.

Identyfikatory

DOI

10.3233/FI-2016-1375

• Konferencja: International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (Petri Nets 2015), (36; 21–26.06.2015; Brussels, Belgium)
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

Petri nets; structured data; well-quasi orders

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 146, nr 1
• Strony: 35--82
• Opis fizyczny: Bibliogr. 42 poz., rys.

Twórcy

autor

Badouel E.

• INRIA Rennes, France

autor

Hélouët L.

• INRIA Rennes, France

autor

Morvan C.

• Université Paris-Est, France

Bibliografia

• [1] Lazic R, Newcomb T, Ouaknine J, Roscoe AW, Worrell J. Nets with Tokens which Carry Data. Fundam Inform. 2008;88(3):251–274. Available from: http://dl.acm.org/citation.cfm?id=1497079.1497082.
• [2] Genest B, Muscholl A, Wu Z. Verifying Recursive Active Documents with Positive Data Tree Rewriting. In: Proc. of FSTTCS 2010. vol. 8 of LIPIcs; 2010. p. 469–480. doi: 10.4230/LIPIcs.FSTTCS.2010.469.
• [3] Wies T, Zufferey T, Henzinger TA. Forward Analysis of Depth-Bounded Processes. In: FOSSACS. vol. 6014 of LNCS. Springer; 2010. p. 94–108. doi: 10.1007/978-3-642-12032-9_8.
• [4] van der Aalst WMP. The Application of Petri Nets to Workflow Management. Journal of Circuits, Systems, and Computers. 1998;8(1):21–66.
• [5] van Hee KM, Hidders J, Houben G, Paredaens J, Thiran P. On the relationship between workflow models and document types. Inf Syst. 2009; 34(1):178–208. doi: 10.1016/j.is.2008.06.003.
• [6] Jensen K. Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use - Volume 1, Second Edition. Monographs in Theoretical Computer Science. An EATCS Series; 1996.
• [7] Genrich H. Predicate/Transition Nets. In: Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986. vol. 254 of LNCS. Springer; 1986. p. 207–247.
• [8] Lenz K, Oberweis A. Modeling Interorganizational Workflows with XML Nets. In: 34th Annual Hawaii International Conference on System Sciences (HICSS-34); 2001. doi: 10.1109/HICSS.2001.927083.
• [9] Lomazova IA, Schnoebelen P. Some Decidability Results for Nested Petri Nets. In: Perspectives of System Informatics. Springer; 1999. p. 208–220.
• [10] Dufourd C, Finkel A, Schnoebelen P. Reset Nets Between Decidability and Undecidability. In: Proc. of ICALP’98. vol. 1443 of LNCS. Springer; 1998. p. 103–115.
• [11] Abiteboul S, Benjelloun O, Manolescu I, Milo T, Weber R. Active XML: A Data-Centric Perspective on Web Services. In: BDA02; 2002. doi: 10.1007/978-3-662-10874-1_12.
• [12] Nigam A, Caswell NS. Business artifacts: An approach to operational specification. IBM Syst J. 2003 July;42:428–445. Available from: http://dx.doi.org/10.1147/sj.423.0428. doi: http://dx.doi.org/10.1147/sj.423.0428.
• [13] Hull R, Damaggio E, Fournier F, Gupta M, Heath FT, Hobson S, et al. Introducing the Guard-Stage-Milestone Approach for Specifying Business Entity Lifecycles. In: Proc. of WS-FM 2010. vol. 6551 of LNCS. Springer; 2011. p. 1–24. doi: 10.1007/978-3-642-19589-1_1.
• [14] Kitchin D, Cook W, Misra J. A Language for Task Orchestration and Its Semantic Properties. In: Concurrency Theory CONCUR’06; 2006. p. 477–491.
• [15] Andrews T, Curbera F, Dholakia H, Goland Y, Klein J, Leymann F, et al.. Business Process Execution Language for Web Services (BPEL4WS). Version 1.1; 2003. Available from: http://xml.coverpages.org/BPELv11-May052003Final.pdf.
• [16] Akshay S, Hélouet L, Mukund M. Sessions with an unbounded number of agents. In: ACSD’14. vol.4281. IEEE; 2014. p. 166–175.
• [17] Badouel E, Hélouët L, Kouamou GE, Morvan C. A Grammatical Approach to Data-centric Case Management in a Distributed Collaborative Environment. In: SAC’15. ACM; 2015. p. 1834–1839. doi:10.1145/2695664.2695698.
• [18] Honda K, Yoshida N, Carbone M. Multiparty asynchronous session types. In: POPL. ACM; 2008. p. 273–284.
• [19] Bruni R, Lanese I, Melgratti HC, Tuosto E. Multiparty Sessions in SOC. In: COORDINATION. vol. 5052 of LNCS. Springer; 2008. p. 67–82.
• [20] Boreale M, Bruni R, De Nicola R, Loreti M. Sessions and Pipelines for Structured Service Programming. In: FMOODS. vol. 5051 of LNCS. Springer; 2008. p. 19–38.
• [21] Pugliese R, Tiezzi F. A calculus for orchestration of Web services. J Applied Logic. 2012;10(1):2–31. doi: 10.1016/j.jal.2011.11.002.
• [22] Abdulla PA, Cerans K, Jonsson B, Tsay YK. General Decidability Theorems for Infinite-State Systems. In: Proc. of LICS’96. IEEE; 1996. p. 313–321.
• [23] Finkel A, Schnoebelen P. Well-structured transition systems everywhere! Theor Comput Sci. 2001;256(1-2): 63–92. doi:10.1016/S0304-3975(00)00102-X. Available from: http://dx.doi.org/10.1016/S0304-3975(00)00102-X.
• [24] David C. Complexity of Data Tree Patterns over XML Documents. In: Mathematical Foundations of Computer Science. vol. 5162 of LNCS; 2008. p. 278–289.
• [25] Miklau G, Suciu D. Containment and equivalence for a fragment of XPath. J ACM. 2004;51(1):2–45.
• [26] World Wide Web Consortium. XML Path Language (Xpath). W3C; 1999. W3C Recommendation, Available from: http://www.w3.org/TR/xpath.
• [27] Ding G. Subgraphs and well-quasi-ordering. In: Journal of Graph Theory. 1992;16(5):489–502.
• [28] OASIS. Web Services Business Process Execution Language. OASIS; 2007. Available from: http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.pdf.
• [29] World Wide Web Consortium. XQuery 1.0: An XML Query Language. W3C; 1999. W3C Recommendation, Available from: http://www.w3.org/TR/xquery.
• [30] Gostellow K, Cerf V, Estrin G, Volansky S. Proper Termination of Flow-of-control in Programs Involving Concurrent Processes. In: Application and Theory of Petri Nets ICATPN ’97. vol. 7(11) of ACM Sigplan. Springer; 1972. p. 15–27.
• [31] van der Aalst WMP. Verification of Workflow Nets. In: Application and Theory of Petri Nets 1997 ICATPN ’97. vol. 1248 of LNCS. Springer; 1997. p. 407–426.
• [32] Mlynkova I, Toman K, Pokorný J. Statistical Analysis of Real XML Data Collections. In: Proc. of International Conference on Management of Data’06. Tata McGraw-Hill; 2006. p. 15–26.
• [33] Higman G. Ordering by divisibility in abstract algebras. Proc London Math Soc (3). 1952;2:326–336.
• [34] Damaggio E, Deutsch A, Vianu V. Artifact systems with data dependencies and arithmetic. ACM Trans Database Syst. 2012;37(3):22. doi: 10.1145/2338626.2338628.
• [35] Misra J, Cook W. Computation Orchestration. Software and Systems Modeling. 2007;6(1):83–110.
• [36] Abiteboul S, Benjelloun O, Milo T. Positive Active XML. In: Proc. of PODS’04. ACM; 2004. p. 35–45.
• [37] Abiteboul S, Segoufin L, Vianu V. Static analysis of active XML systems. ACM Trans Database Syst. 2009; 34(4) p.23:1–23:44. doi: 10.1145/1620585.1620590.
• [38] Deniélou P, Yoshida N. Dynamic multirole session types. In: POPL; 2011. p. 435–446. doi:10.1145/1925844.1926435.
• [39] Demangeon R, Honda K. Nested Protocols in Session Types. In: CONCUR; 2012. p. 272–286. doi:10.1007/978-3-642-32940-1_20.
• [40] Acciai L, Boreale M. Deciding Safety Properties in Infinite-State Pi-Calculus via Behavioural Types. In: ICALP (2). vol. 5556 of LNCS. Springer; 2009. p. 31–42. doi: 10.1007/978-3-642-02930-1_3.
• [41] Lanese I, Martins F, Vasconcelos VT, Ravara A. Disciplining Orchestration and Conversation in Service-Oriented Computing. In: SEFM. IEEE Computer Society; 2007. p. 305–314.
• [42] Caires L, Torres Vieira H. Conversation types. Theor Comput Sci. 2010;411(51-52):4399–4440. doi:10.1016/j.tcs.2010.09.010.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).