Abstract
Petri nets with name creation and management (\({\nu}\)-PNs) have been recently introduced as an expressive model for dynamic (distributed) systems, whose dynamics are determined not only by how tokens flow in the system, but also by the pure names they carry. On the one hand, this extension makes the resulting nets strictly more expressive than P/T nets: they can be exploited to capture a plethora of interesting systems, such as distributed systems enriched with channels and name passing, service interaction with correlation mechanisms, and resource-constrained workflow nets that explicitly account for process instances. On the other hand, fundamental properties like coverability, termination and boundedness are decidable for \({\nu}\)-PNs. In this work, we go one step beyond the verification of such general properties, and provide decidability and undecidability results of model checking \({\nu}\)-PNs against variants of first-order \({\mu}\)-calculus, recently proposed in the area of data-aware process analysis. While this model checking problem is undecidable in the general case, decidability can be obtained by considering different forms of boundedness, which still give raise to an infinite-state transition system. We then ground our framework to tackle the problem of soundness checking over workflow nets enriched with explicit process instances and resources. Notably, our decidability results are obtained via a translation to data-centric dynamic systems, a recently devised framework for the formal specification and verification of data-aware business processes working over full-fledged relational databases with constraints. In this light, our results contribute to the cross-fertilization between the area of formal methods for concurrent systems and that of foundations of data-aware processes, which has not been extensively investigated so far.
Similar content being viewed by others
References
Abadi M, Gordon AD (1997) A calculus for cryptographic protocols: the spi calculus. In: Proceedings of the 4th ACM conference on computer and communications security, CCS ’97, pp 36–47, New York, NY, USA. ACM
Anisimov NA, Koutny M (1995) On compositionality and petri nets in protocol engineering. In: Piotr Dembinski and Marek Sredniawa, editors, PSTV, vol. 38 of IFIP Conference Proceedings, pp 71–86. Chapman & Hall
Bojanczyk M, Braud L, Klin B, Lasota S (2012) Towards nominal computation. In Proceedings of POPL. ACM Press
Bagheri Hariri B, Calvanese D, De Giacomo G, Deutsch A, Montali M (2013) Verification of relational data-centric dynamic systems with external services. In: Proceedings of PODS, pp 163–174. ACM
Bagheri Hariri B, Calvanese D, Deutsch A, Montali M (2014) State boundedness in data-aware dynamic systems. In: Proceedings of KR
Bagheri Hariri B, Calvanese B, Montali M, De Giacomo G, De Masellis R, Felli P (2013) Description logic knowledge and action bases. J Artif Intell Res
Belardinelli F, Lomuscio A, Patrizi F (2012) An abstraction technique for the verification of artifact-centric systems. In: Proceedings KR
Bojanczyk M, Segoufin L, Torunczyk S (2013) Verification of database-driven systems via amalgamation. In: Proceedings of PODS
Calvanese D, De Giacomo G, Montali M (2013) Foundations of data aware process analysis: a database theory perspective. In: Proceedings of PODS
Calvanese D, De Giacomo G, Montali M, Patrizi F (2013) Verification and synthesis in description logic based dynamic systems. In: Proceedings of RR, vol 7994 of LNCS. Springer, New York
Chandra A, Harel D (1980) Computable queries for relational database systems. J Comput Syst Sci 21
Decker G, Weske M (2008) Instance isolation analysis for service-oriented architectures. In: Proceedings of SCC, pp 249–256. IEEE Computer Society
Allen Emerson E (1996) Model checking and the Mu-calculus. In: Proceedings of the DIMACS symposium on descriptive complexity and finite models, pp 185–214. American Mathematical Society Press
Esparza J (1994) On the decidability of model checking for several \({\mu}\)-calculi and petri nets. In: Proceedings of CAAP, vol 787 of LNCS, pp 115–129. Springer, New York
Gabbay M, Pitts AM (2002) A new approach to abstract syntax with variable binding. Formal Asp Comput 13(3–5)
Hüchting R, Majumdar R, Meyer R (2013) A theory of name boundedness. In: Proceedings of CONCUR, vol 8052 of LNCS, pp 182–196. Springer, New York
Jensen K, Michael Kristensen L (2009) Coloured petri nets—modelling and validation of concurrent systems. Springer, New York
Köhler M, Rölke H (2004) Properties of object petri nets. In: Proceedings of ICATPN, vol 3099 of LNCS, pp 278–297. Springer, New York
Libkin L (2004) Elements of finite model theory, vol 7360 of LNCS, chapter fixed point logics and complexity classes. Springer, New York
Lazic R, Newcomb T, Ouaknine J, Roscoe AW, Worrell J (2008) Nets with tokens which carry data. Fundam Inf 88(3): 251–274
Martos-Salgado M, Rosa-Velardo F (2011) Dynamic soundness in resource-constrained workflow nets. In: Proceedings of FMOODS/FORTE, vol 6722 of LNCS, pp 259–273. Springer, New York
Needham RM (1989) Names. In: Mullender S (ed) Distributed systems, pp 89–101. ACM Press, Wokingham
Peterson JL (1980) A note on colored petri nets. Inf Process Lett 11(1): 40–43
Reisig W (2013) Understanding petri nets: modeling techniques, analysis methods, case studies. Springer, New York
Rosa-Velardo F, de Frutos-Escrig D (2008) Name creation vs. replication in petri net systems. Fundam Inf 88(3): 329–356
Rosa-Velardo F, de Frutos-Escrig D (2011) Decidability and complexity of petri nets with unordered data. Theor Comput Sci 412(34): 4439–4451
Vardi MY (2005) Model checking for database theoreticians. In: Proceedings of ICDT, vol 3363 of LNCS, pp 1–16. Springer, New York
van der Aalst WMP (1997) Verification of workflow nets. In: Proceedings of ICATPN, vol 1248 of LNCS, pp 407–426. Springer, New York
van der Aalst WMP (2005) Pi calculus versus petri nets: let us eat humble pie rather than further inflate the pi hype. BPTrends 3(5)
van der Aalst WMP, Stahl C (2011) Modeling business processes—a petri net-oriented approach. Cooperative Information Systems series. MIT Press
van der Aalst WMP, van Hee KM, ter Hofstede AHM, Sidorova N, Verbeek HMW, Voorhoeve M, Thandar Wynn M (2011) Soundness of workflow nets: classification, decidability, and analysis. Formal Asp Comput 23(3):333–363
van Hee KM, Serebrenik A, Sidorova N, Voorhoeve M (2005) Soundness of resource-constrained workflow nets. In: Proceedings of ICATPN, vol 3536 of LNCS, pp 250–267. Springer, New York
van Hee KM, Sidorova N, Voorhoeve M (2006) Resource-constrained workflow nets. Fundam Inf 71(2-3): 243–257
Vianu V (2009) Automatic verification of database-driven systems: a new frontier. In: Proceedings of ICDT, pp 1–13
Westergaard M, Maria Maggi F (2011) Modeling and verification of a protocol for operational support using coloured petri nets. In: Proceedings of Applications and theory of petri nets—32nd international conference, PETRI NETS 2011, Newcastle, UK, June 20–24, 2011, pp 169–188
Author information
Authors and Affiliations
Corresponding authors
Additional information
Thomas Hildebrandt, Joachim Parrow, Matthias Weidlich, and Marco Carbone
Rights and permissions
About this article
Cite this article
Montali, M., Rivkin, A. Model checking Petri nets with names using data-centric dynamic systems. Form Asp Comp 28, 615–641 (2016). https://doi.org/10.1007/s00165-016-0370-6
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-016-0370-6