A Non-Deterministic Multiset Query Language

• Autorzy: Zieliński Bartosz

Identyfikatory

DOI

10.3233/FI-2021-2095

• Języki publikacji: EN

Abstrakty

EN

We develop a multiset query and update language executable in a term rewriting system. Its most remarkable feature, besides non-standard approach to quantification and introduction of fresh values, is non-determinism — a query result is not uniquely determined by the database. We argue that this feature is very useful, e.g., in modelling user choices during simulation or reachability analysis of a data-centric business process — the intended application of our work. Query evaluation is implemented by converting the query into a terminating term rewriting system and normalizing the initial term which encapsulates the current database. A normal form encapsulates a query result. We prove that our language can express any relational algebra query. Finally, we present a simple business process specification framework (and an example specification). Both syntax and semantics of our query language is implemented in Maude

Słowa kluczowe

EN

term rewriting; query languages; business process modelling

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 184, nr 2
• Strony: 141--180
• Opis fizyczny: Bibliogr. 46 poz., rys.

Twórcy

autor

Zieliński Bartosz

• Department of Computer Science Faculty of Physics and Applied Informatics, University of Łódź

Bibliografia

• [1] Hull R. Artifact-Centric Business Process Models: Brief Survey of Research Results and Challenges. In: Meersman R, Tari Z (eds.), On the Move to Meaningful Internet Systems: OTM 2008. Springer Berlin Heidelberg, Berlin, Heidelberg, 2008 pp. 1152-1163. doi:10.1007/978-3-540-88873-4_17.
• [2] Calvanese D, De Giacomo G, Montali M. Foundations of Data-aware Process Analysis: A Database Theory Perspective. In: Proceedings of the 32Nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS ’13. ACM, New York, NY, USA, 2013 pp. 1-12. doi:10.1145/2463664.2467796.
• [3] van der Aalst WM. The application of Petri nets to workflow management. Journal of circuits, systems, and computers, 1998. 8(01):21-66. doi:10.1142/S0218126698000043.
• [4] van der Aalst WM, Ter Hofstede AH. YAWL: yet another workflow language. Information systems, 2005. 30(4):245-275. doi:10.1016/j.is.2004.02.002.
• [5] Rosa-Velardo F, de Frutos-Escrig D. Decidability and complexity of Petri nets with unordered data. Theoretical Computer Science, 2011. 412(34):4439-4451.
• [6] Lasota S. Decidability border for Petri nets with data: WQO dichotomy conjecture. In: International Conference on Application and Theory of Petri Nets and Concurrency. Springer, 2016 pp. 20-36. doi:10.1007/978-3-319-39086-4_3.
• [7] Montali M, Rivkin A. Model checking Petri nets with names using data-centric dynamic systems. Formal Aspects of Computing, 2016. 28(4):615-641. doi:10.1007/s00165-016-0370-6.
• [8] Montali M, Rivkin A. DB-Nets: On the Marriage of Colored Petri Nets and Relational Databases. In: Transactions on Petri Nets and Other Models of Concurrency XII. Springer Berlin Heidelberg, Berlin, Heidelberg, 2017 pp. 91-118. doi:10.1007/978-3-662-55862-1_5.
• [9] Montali M, Rivkin A. From DB-nets to Coloured Petri Nets with Priorities. In: International Conference on Applications and Theory of Petri Nets and Concurrency. Springer, 2019 pp. 449-469. doi:10.1007/978-3-030-21571-2_24.
• [10] Meseguer J. Conditional rewriting logic as a unified model of concurrency. Theoretical computer science, 1992. 96(1):73-155. doi:10.1016/0304-3975(92)90182-F.
• [11] Meseguer J, Rosu G. The rewriting logic semantics project. Theoretical Computer Science, 2007. 373(3):213 - 237. doi:10.1016/j.tcs.2006.12.018.
• [12] Stehr MO, Meseguer J, Ölveczky PC. Rewriting Logic as a Unifying Framework for Petri Nets. In: Unifying Petri Nets: Advances in Petri Nets. Springer Berlin Heidelberg, Berlin, Heidelberg, 2001 pp. 250-303. doi:10.1007/3-540-45541-8_9.
• [13] Padberg J, Schulz A. Model Checking Reconfigurable Petri Nets with Maude. In: Echahed R, Minas M (eds.), Graph Transformation. Springer International Publishing, Cham, 2016 pp. 54-70. doi:10.1007/978-3-319-40530-8_4.
• [14] Kheldoun A, Barkaoui K, Ioualalen M. Formal verification of complex business processes based on high-level Petri nets. Information Sciences, 2017. 385:39-54. doi:10.1016/j.ins.2016.12.044.
• [15] Zieli´nski B. A Query Language Based on Term Matching and Rewriting. Fundamenta Informaticae, 2019. 169:237-274. doi:10.3233/FI-2019-1845.
• [16] Meseguer J, Thati P. Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation, 2007. 20(1-2):123-160. doi:10.1007/s10990-007-9000-6.
• [17] Fay M. First-order unification in an equational theory. In: Proceedings of the 4th Workshop on Automated Deduction, Austin, Texas, 1979.
• [18] Hullot JM. Canonical forms and unification. In: International Conference on Automated Deduction. Springer, 1980 pp. 318-334. doi:10.1007/3-540-10009-1 25.
• [19] Alpuente M, Escobar S, Iborra J. Termination of narrowing revisited. Theoretical Computer Science, 2009. 410(46):4608-4625. doi:10.1016/j.tcs.2009.07.037.
• [20] Zieli´nski B, Ma´slanka P. Relational Transition System in Maude. In: Beyond Databases, Architectures and Structures. Towards Efficient Solutions for Data Analysis and Knowledge Representation: 13th International Conference, BDAS 2017, Ustroń, Poland, May 30 - June 2, 2017, Proceedings. Springer International Publishing, Cham, 2017 pp. 497-511. doi:10.1007/978-3-319-58274-0_39.
• [21] Ros¸u G, Ellison C, Schulte W. Matching Logic: An Alternative to Hoare/Floyd Logic. In: Algebraic Methodology and Software Technology. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011 pp. 142-162. doi:10.1007/978-3-642-17796-5_9.
• [22] Ros¸u G. Matching logic. arXiv:1705.06312, 2017.
• [23] Stehr MO. CINNI-A Generic Calculus of Explicit Substitutions and its Application to λ-ς-and π-Calculi. Electronic Notes in Theoretical Computer Science, 2000. 36:70-92. doi:10.1016/S1571-0661(05)80125-2.
• [24] Baader F. The description logic handbook: Theory, implementation and applications. Cambridge University Press, New York, NY, USA, 2003. ISBN:0-521-78176-0.
• [25] De Giacomo G, De Masellis R, Rosati R. Verification of conjunctive artifact-centric services. International Journal of Cooperative Information Systems, 2012. 21(02):111-139. doi:10.1142/S0218843012500025.
• [26] Hariri BB, Calvanese D, De Giacomo G, De Masellis R, Felli P. Foundations of relational artifacts verification. In: International Conference on Business Process Management. Springer, 2011 pp. 379-395. doi:10.1007/978-3-642-23059-2_28.
• [27] Calvanese D, Montali M, Patrizi F, De Giacomo G. Description logic based dynamic systems: modeling, verification, and synthesis. In: Proceedings of the 24th International Conference on Artificial Intelligence. AAAI Press, 2015 pp. 4247-4253.
• [28] Abdulla PA, Aiswarya C, Atig MF, Montali M, Rezine O. Recency-Bounded Verification of Dynamic Database-Driven Systems. In: Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS ’16. ACM, New York, NY, USA, 2016 pp. 195-210. doi:10.1145/2902251.2902300.
• [29] Chen-Burger YH, Robertson D. Automating business modelling: a guide to using logic to represent informal methods and support reasoning. Springer Science & Business Media, 2006. doi:10.1007/b138799.
• [30] Merouani H, Mokhati F, Seridi-Bouchelaghem H. Formalizing Artifact-Centric Business Processes - Towards a Conformance Testing Approach. In: Proceedings of the 16th International Conference on Enterprise Information Systems. 2014 pp. 368-374. doi:10.5220/0004951803680374.
• [31] McCarthy J, Hayes PJ. Some philosophical problems from the standpoint of artificial intelligence. Readings in artificial intelligence, 1969. pp. 431-450.
• [32] Deutsch A, Li Y, Vianu V. Verifas: a practical verifier for artifact systems. Proceedings of the VLDB Endowment, 2017. 11(3):283-296. doi:10.14778/3157794.3157798.
• [33] Deutsch A, Li Y, Vianu V. Verification of hierarchical artifact systems. ACM Transactions on Database Systems (TODS), 2019. 44(3):1-68. doi:10.1145/3321487.
• [34] Calvanese D, Ghilardi S, Gianola A, Montali M, Rivkin A. Formal modeling and SMT-based parameterized verification of data-aware BPMN. In: International Conference on Business Process Management. Springer, 2019 pp. 157-175. doi:10.1007/978-3-030-26619-6_12.
• [35] Seco JC, Debois S, Hildebrandt T, Slaats T. RESEDA: Declaring live event-driven computations as REactive SEmi-structured DAta. In: 2018 IEEE 22nd International enterprise distributed object computing conference (EDOC). IEEE, 2018 pp. 75-84. doi:10.1109/EDOC.2018.00020.
• [36] Meseguer J. Membership algebra as a logical framework for equational specification. In: Recent Trends in Algebraic Development Techniques. Springer Berlin Heidelberg, Berlin, Heidelberg, 1998 pp. 18-61. doi:10.1007/3-540-64299-4_26.
• [37] Huet G. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. Journal of the ACM (JACM), 1980. 27(4):797-821.
• [38] Thielscher M. Introduction to the Fluent Calculus. Electronic Transactions on Artificial Intelligence, 1998. 2(3-4):179-192.
• [39] Ochremiak J. Nominal sets over algebraic atoms. In: International Conference on Relational and Algebraic Methods in Computer Science. Springer, 2014 pp. 429-445. doi:10.1007/978-3-319-06251-8 26.
• [40] Hull R, Damaggio E, De Masellis R, Fournier F, Gupta M, Heath III FT, Hobson S, Linehan M, Maradugu S, Nigam A, et al. Business artifacts with guard-stage-milestone lifecycles: managing artifact interactions with conditions and events. In: Proceedings of the 5th ACM international conference on Distributed event-based system. ACM, 2011 pp. 51-62. doi:10.1145/2002259.2002270.
• [41] Abiteboul S, Vianu V, Fordham B, Yesha Y. Relational Transducers for Electronic Commerce. In: Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, PODS ’98. ACM, New York, NY, USA. ISBN 0-89791-996-3, 1998 pp. 179-187. doi:10.1145/275487.275507.
• [42] Abiteboul S, Vianu V, Fordham B, Yesha Y. Relational transducers for electronic commerce. Journal of Computer and System Sciences, 2000. 61(2):236-269. doi:10.1006/jcss.2000.1708.
• [43] Abdulla PA, Aiswarya C, Atig MF, Montali M, Rezine O. Recency-bounded verification of dynamic database-driven systems (extended version). arXiv preprint arXiv:1604.03413, 2016.
• [44] Clavel M, Dur´an F, Eker S, Lincoln P, Mart´ı-Oliet N, Meseguer J, Talcott C. The Maude 2.0 System. In:Nieuwenhuis R (ed.), Rewriting Techniques and Applications (RTA 2003), number 2706 in Lecture Notes in Computer Science. Springer-Verlag, 2003 pp. 76-87. doi:10.1007/3-540-44881-0_7.
• [45] Zieliński B. Nondeterministic Rewriting Query Language (NDRQL). Project website, http://ki.wfi.uni.lodz.pl/ndrql/.
• [46] Clavel M, Duràn F, Eker S, Escobar S, Lincoln P, Martì-Oliet N, Meseguer J, Talcott C. Maude Manual (Version 2.7.1), 2016.

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023). (PL)