A Query Language Based on Term Matching and Rewriting

• Autorzy: Zieliński Bartosz

Identyfikatory

DOI

10.3233/FI-2019-1845

• Języki publikacji: EN

Abstrakty

EN

Recent years have seen the emergence of a data-centric approach to business process modelling as an attractive alternative to the dominant task-centric one. This new paradigm requires new tools for effective specification, simulation and validation of data-centric models. In particular, such tools must include support for expressive query and database update languages. Rewriting logic was proposed (and successfully used) as a generic framework for the specification of dynamic systems. However, though relational and other data models can be easily simulated, rewriting systems lack the direct support for first-order queries. In this paper we describe a novel condition and query language (at least as expressive as relational algebra), implemented in the term rewriting language Maude, together with a simple framework for relational transition system specification and simulation. The language is designed to be easy to implement on the top of a conditional rewriting system. Its most interesting feature is that it avoids all problems with variable binding. It works with models founded both on sets and multisets, and the language has linear-like facilities to refer to multiplicities of facts (in the case of multiset-founded models). As an example of the use of our language and simulation framework we reproduce some specifications of business processes from the literature. We also compare several methods for choosing the next action and its input during simulation.

Słowa kluczowe

EN

term rewriting; query language; business process modelling; Maude

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 169, nr 3
• Strony: 237--274
• Opis fizyczny: Bibliogr. 59 poz., rys., tab.

Twórcy

autor

Zieliński Bartosz

• Department of Computer Science, Faculty of Physics and Applied Informatics, University of Łódź, Pomorska 149/153, 90-236 Łódź, Poland

Bibliografia

• [1] Reichert M. Process and Data: Two Sides of the Same Coin? In: On the Move to Meaningful Internet Systems: OTM 2012: Confederated International Conferences: CoopIS, DOA-SVI, and ODBASE 2012, Rome, Italy, September 10-14, 2012. Proceedings, Part I. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-33606-5, 2012 pp. 2-19. doi:10.1007/978-3-642-33606-5_2.
• [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] Hull R. Artifact-Centric Business Process Models: Brief Survey of Research Results and Challenges. In: On the Move to Meaningful Internet Systems: OTM 2008: OTM 2008 Confederated International Conferences, CoopIS, DOA, GADA, IS, and ODBASE 2008, Monterrey, Mexico, November 9-14, 2008, Proceedings, Part II. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-88873-4, 2008 pp. 1152-1163. doi:10.1007/978-3-540-88873-4_17.
• [4] Cangialosi P, De Giacomo G, De Masellis R, Rosati R. Conjunctive Artifact-Centric Services. In: Service-Oriented Computing: 8th International Conference, ICSOC 2010, San Francisco, CA, USA, December 7-10, 2010. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010 pp. 318-333. doi:10.1007/978-3-642-17358-5_22.
• [5] 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.
• [6] 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.
• [7] 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.
• [8] 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.
• [9] 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.
• [10] 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.
• [11] Vianu V. Automatic Verification of Database-driven Systems: A New Frontier. In: Proceedings of the 12th International Conference on Database Theory, ICDT ’09. ACM, New York, NY, USA. ISBN 978-1-60558-423-2, 2009 pp. 1-13. doi:10.1145/1514894.1514896.
• [12] Damaggio E, Deutsch A, Vianu V. Artifact Systems with Data Dependencies and Arithmetic. ACM Trans. Database Syst., 2012. 37(3):22:1-22:36. doi:10.1145/2338626.2338628.
• [13] Bojańczyk M, Segoufin L, Toruńczyk S. Verification of Database-driven Systems via Amalgamation. In: Proceedings of the 32Nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS ’13. ACM, New York, NY, USA. ISBN 978-1-4503-2066-5, 2013 pp. 63-74. doi:10.1145/2463664.2465228.
• [14] Bagheri Hariri B, Calvanese D, De Giacomo G, Deutsch A, Montali M. Verification of Relational Datacentric Dynamic Systems with External Services. In: Proceedings of the 32Nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS ’13. ACM, New York, NY, USA. ISBN 978-1-4503-2066-5, 2013 pp. 163-174. doi:10.1145/2463664.2465221.
• [15] 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. ISBN 978-1-4503-2066-5, 2013 pp. 1-12. doi:10.1145/2463664.2467796.
• [16] Deutsch A, Hull R, Vianu V. Automatic Verification of Database-Centric Systems. SIGMOD Rec., 2014. 43(3):5-17. doi:10.1145/2694428.2694430.
• [17] Belardinelli F, Lomuscio A, Patrizi F. Verification of agent-based artifact systems. Journal of Artificial Intelligence Research, 2014. 51:333-376. doi:10.1613/jair.4424.
• [18] Deutsch A, Li Y, Vianu V. Verification of Hierarchical Artifact Systems. In: Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS ’16. ACM, New York, NY, USA. ISBN 978-1-4503-4191-2, 2016 pp. 179-194. doi:10.1145/2902251.2902275.
• [19] Deutsch A, Hull R, Li Y, Vianu V. Automatic Verification of Database-centric Systems. ACM SIGLOG News, 2018. 5(2):37-56. doi:10.1145/3212019.3212025.
• [20] Calvanese D, Giacomo GD, Montali M, Patrizi F. First-order μ-calculus over generic transition systems and applications to the situation calculus. Information and Computation, 2018. 259:328-347. doi:10.1016/j.ic.2017.08.007. 22nd International Symposium on Temporal Representation and Reasoning.
• [21] Levesque H, Pirri F, Reiter R. Foundations for the situation calculus. Electronic Transactions on Artificial Intelligence, 1998. 2(3-4):159-178.
• [22] Thielscher M. Introduction To The Fluent Calculus. Electronic Transactions on Artificial Intelligence, 1998. 2(3-4):179-192.
• [23] Puhlmann F, Weske M. Using the π-Calculus for Formalizing Workflow Patterns. In: Business Process Management: 3rd International Conference, BPM 2005, Nancy, France, September 5-8, 2005. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, 2005 pp. 153-168. doi:10.1007/11538394_11.
• [24] 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.
• [25] 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.
• [26] 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.
• [27] 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.
• [28] Verdejo A, Martí-Oliet N. Implementing CCS in Maude 2. Electronic Notes in Theoretical Computer Science, 2004. 71:282-300. doi:10.1016/S1571-0661(05)82540-X.
• [29] Thati P, Sen K, Martí-Oliet N. An executable specification of asynchronous Pi-Calculus semantics and may testing in Maude 2.0. Electronic Notes in Theoretical Computer Science, 2004. 71:261-281. doi:10.1016/S1571-0661(05)82539-3.
• [30] 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.
• [31] Clavel M, Durán 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.
• [32] Maude Query Language project page. URL http://www.wfis.uni.lodz.pl/kft2/mql/.
• [33] 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.
• [34] 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.
• [35] Zieliński B, Maślanka 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.
• [36] Roşu G, Ellison C, Schulte W. Matching Logic: An Alternative to Hoare/Floyd Logic. In: Algebraic Methodology and Software Technology: 13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010. Revised Selected Papers. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011 pp. 142-162. doi:10.1007/978-3-642-17796-5_9.
• [37] Rosu G. Matching Logic. Logical Methods in Computer Science, 2017. 13(4). doi:10.23638/LMCS-13(4:28)2017.
• [38] Benzaken V, Contejean E, Dumbrava S. A Coq Formalization of the Relational Data Model. In: Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410. Springer-Verlag New York, Inc., New York, NY, USA, 2014 pp. 189-208. doi:10.1007/978-3-642-54833-8_11.
• [39] Malecha G, Morrisett G, Shinnar A, Wisnesky R. Toward a Verified Relational Database Management System. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’10. ACM, New York, NY, USA, 2010 pp. 237-248. doi:10.1145/1706299.1706329.
• [40] Alpuente M, Feliú MA, Joubert C, Villanueva A. Defining Datalog in Rewriting Logic. In: Logic-Based Program Synthesis and Transformation: 19th International Symposium, LOPSTR 2009, Coimbra, Portugal, September 2009, Revised Selected Papers. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010 pp. 188-204. doi:10.1007/978-3-642-12592-8_14.
• [41] Alpuente M, Feliú MA, Joubert C, Villanueva A. Implementing Datalog in Maude. In: Peña R (ed.), Proceedings of the IX Jornadas sobre Programación y Lenguajes (PROLE’09) and I Taller de Programación Funcional (TPF’09). 2009 p. 15-22.
• [42] 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.
• [43] Baader F. The description logic handbook: Theory, implementation and applications. Cambridge University Press, New York, NY, USA, 2003. ISBN 0-521-78176-0.
• [44] Meseguer J. Membership algebra as a logical framework for equational specification. In: Recent Trends in Algebraic Development Techniques: 12th International Workshop, WADT’97 Tarquinia, Italy, June 3-7, 1997 Selected Papers. Springer Berlin Heidelberg, Berlin, Heidelberg, 1998 pp. 18-61. doi:10.1007/3-540-64299-4_26.
• [45] Bergstra JA, Tucker JV. A characterisation of computable data types by means of a finite equational specification method. In: International Colloquium on Automata, Languages, and Programming. Springer, 1980 pp. 76-90.
• [46] Clavel M, Meseguer J. Reflection in conditional rewriting logic. Theoretical Computer Science, 2002. 285(2):245-288. doi:10.1016/S0304-3975(01)00360-7.
• [47] Girard JY. Linear logic. Theoretical computer science, 1987. 50(1):1-101. doi:10.1016/0304-3975(87)90045-4.
• [48] Hull R, Damaggio E, Fournier F, Gupta M, Heath FT, Hobson S, Linehan M, Maradugu S, Nigam A, Sukaviriya P, Vaculin R. Introducing the Guard-Stage-Milestone Approach for Specifying Business Entity Lifecycles. In: Web Services and Formal Methods: 7th International Workshop, WS-FM 2010, Hoboken, NJ, USA, September 16-17, 2010. Revised Selected Papers. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011 pp. 1-24. doi:10.1007/978-3-642-19589-1_1.
• [49] Damaggio E, Hull R, Vaculín R. On the equivalence of incremental and fixpoint semantics for business artifacts with Guard-Stage-Milestone lifecycles. Information Systems, 2013. 38(4):561-584. doi:10.1016/j.is.2012.09.002.
• [50] Hull R, Damaggio E, De Masellis R, Fournier F, Gupta M, Fenno Terry Heath I, Hobson S, Linehan M, Maradugu S, Nigam A, et al. A Formal Introduction to Business Artifacts with Guard-Stage-Milestone Lifecycles, 2011. Draft IBM Research internal report, available at https://pdfs.semanticscholar.org/1367/0bc6a5948d90ada4ae7d86b6f79e796a567e.pdf.
• [51] Vardi MY. Model Checking for Database Theoreticians. In: Eiter T, Libkin L (eds.), Database Theory - ICDT 2005. Springer Berlin Heidelberg, Berlin, Heidelberg, 2005 pp. 1-16. doi:10.1007/978-3-540-30570-5_1.
• [52] Fikes RE, Nilsson NJ. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial intelligence, 1971. 2(3-4):189-208. doi:10.1016/0004-3702(71)90010-5.
• [53] Rosa-Velardo F, de Frutos-Escrig D. Decidability problems in Petri nets with names and replication. Fundamenta informaticae, 2010. 105(3):291-317. doi:10.3233/FI-2010-368.
• [54] 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.
• [55] Vitter JS. Random sampling with a reservoir. ACM Transactions on Mathematical Software (TOMS), 1985. 11(1):37-57. doi:10.1145/3147.3165.
• [56] Padberg J, Schulz A. Model Checking Reconfigurable Petri Nets with Maude. In: Graph Transformation: 9th International Conference, ICGT 2016, in Memory of Hartmut Ehrig, Held as Part of STAF 2016, Vienna, Austria, July 5-6, 2016, Proceedings. Springer International Publishing, Cham, 2016 pp. 54-70. doi:10.1007/978-3-319-40530-8_4.
• [57] 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.
• [58] Cervesato I, Scedrov A. Relating state-based and process-based concurrency through linear logic (full version). Information and Computation, 2009. 207(10):1044-1077. doi:10.1016/j.ic.2008.11.006.
• [59] Lam ESL, Cervesato I. Modeling Datalog fact assertion and retraction in linear logic. In: Proceedings of the 14th symposium on Principles and practice of declarative programming. ACM, 2012 pp. 67-78. doi:10.1145/2370776.2370786.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).