F. Baader and T. Nipkow, Term Rewriting and All That, 1999.

K. Bae and C. Rocha, Guarded Terms for Rewriting Modulo SMT, Formal Aspects of Component Software, pp.78-97, 2017.
DOI : 10.1016/j.jlamp.2016.10.001

R. Bruni and J. Meseguer, Semantic foundations for generalized rewrite theories, Theoretical Computer Science, vol.360, issue.1-3, pp.386-414, 2006.
DOI : 10.1016/j.tcs.2006.04.012

D. Calvanese, M. Dumas, U. Laurson, F. M. Maggi, M. Montali et al., Semantics and Analysis of DMN Decision Tables, Proc. of BPM, pp.217-233, 2016.
DOI : 10.1016/S0005-1098(96)00165-3

URL : http://arxiv.org/pdf/1603.07466

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All About Maude -A High-Performance Logical Framework, LNCS, vol.4350, 2007.

F. Corradini, F. Fornari, A. Polini, B. Re, F. Tiezzi et al., BProVe: A formal verification framework for business process models, 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp.217-228, 2017.
DOI : 10.1109/ASE.2017.8115635

URL : http://orbit.dtu.dk/files/140315415/08115635.pdf

G. Decker and M. Weske, Interaction-centric modeling of process choreographies, Information Systems, vol.36, issue.2, pp.292-312, 2011.
DOI : 10.1016/j.is.2010.06.005

R. Dijkman, M. Dumas, and C. Ouyang, Semantics and Analysis of Business Process Models in BPMN. Information and Software Technology, pp.1281-1294, 2008.

R. M. Dijkman, M. Dumas, and C. Ouyang, Semantics and analysis of business process models in BPMN, Information and Software Technology, vol.50, issue.12, pp.1281-1294, 2008.
DOI : 10.1016/j.infsof.2008.02.006

F. Durán, S. Lucas, C. Marché, J. Meseguer, and X. Urbain, Proving operational termination of membership equational programs, Higher-Order and Symbolic Computation, pp.59-88, 2008.
DOI : 10.1007/3-540-62950-5_69

F. Durán and G. Salaün, Verifying Timed BPMN Processes Using Maude, Proc. of CO- ORDINATION, pp.219-236, 2017.
DOI : 10.1016/j.entcs.2009.06.029

N. El-saber and A. Boronat, BPMN Formalization and Verification using Maude, Proceedings of the 2014 Workshop on Behaviour Modelling-Foundations and Applications, BM-FA '14, pp.1-8, 2014.
DOI : 10.1145/2630768.2630769

J. A. Goguen and J. Meseguer, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoretical Computer Science, vol.105, issue.2, pp.217-273, 1992.
DOI : 10.1016/0304-3975(92)90302-V

URL : https://doi.org/10.1016/0304-3975(92)90302-v

M. Güdemann, P. Poizat, G. Salaün, and L. Ye, VerChor: A Framework for the Design and Verification of Choreographies, IEEE Transactions on Services Computing, vol.9, issue.4, pp.647-660, 2016.
DOI : 10.1109/TSC.2015.2413401

L. Herbert and R. Sharp, Using Stochastic Model Checking to Provision Complex Business Services, 2012 IEEE 14th International Symposium on High-Assurance Systems Engineering, pp.98-105, 2012.
DOI : 10.1109/HASE.2012.29

I. Iec, International Standard Information technology ? Business Process Model and Notation, 2013.

F. Durán, C. Rocha, and G. Salaün,

A. Kheldoun, K. Barkaoui, and M. Ioualalen, Specification and Verification of Complex Business Processes - A High-Level Petri Net-Based Approach, Proc. of BPMN, pp.55-71, 2015.
DOI : 10.1007/978-3-319-23063-4_4

F. Kossak, C. Illibauer, V. Geist, J. Kubovy, C. Natschläger et al., Schewe. A Rigorous Semantics for BPMN 2.0 Process Diagrams, 2014.

A. Martens, Analyzing Web Service Based Business Processes, Proc. of FASE, pp.19-33, 2005.
DOI : 10.1007/978-3-540-31984-9_3

R. Mateescu, G. Salaün, and L. Ye, Quantifying the parallelism in BPMN processes using model checking, Proceedings of the 17th international ACM Sigsoft symposium on Component-based software engineering, CBSE '14, pp.159-168, 2014.
DOI : 10.1145/2602458.2602473

URL : https://hal.archives-ouvertes.fr/hal-01016412

J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, vol.96, issue.1, pp.73-155, 1992.
DOI : 10.1016/0304-3975(92)90182-F

J. Meseguer, Membership algebra as a logical framework for equational specification, Proc. of WADT'97, pp.18-61, 1998.
DOI : 10.1007/3-540-64299-4_26

H. N. Nguyen, P. Poizat, and F. Zaïdi, A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies, Proc. of ICSOC, pp.525-532, 2012.
DOI : 10.1007/978-3-642-34321-6_36

URL : https://hal.archives-ouvertes.fr/hal-01367304

, Object Management Group Business Process Model and Notation (BPMN) ? V. 2.0, 2011.

, Object Management Group Decision Model and Notation Specification (DMN) ? V. 1.1, 2016.

P. Poizat and G. Salaün, Checking the realizability of BPMN 2.0 choreographies, Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC '12, pp.1927-1934, 2012.
DOI : 10.1145/2245276.2232095

URL : https://hal.archives-ouvertes.fr/hal-00685393

D. Prandi, P. Quaglia, and N. Zannone, Formal Analysis of BPMN Via a Translation into COWS, Proc. of COORDINATION, pp.249-263, 2008.
DOI : 10.1007/978-3-540-68265-3_16

R. Pugliese and F. Tiezzi, A calculus for orchestration of web services, Journal of Applied Logic, vol.10, issue.1, pp.2-31, 2012.
DOI : 10.1016/j.jal.2011.11.002

I. Raedts, M. Petkovic, Y. S. Usenko, J. M. Van-der-werf, J. F. Groote et al., Transformation of BPMN Models for Behaviour Analysis, Proc. of MSVVEIS, pp.126-137, 2007.

C. Rocha, J. Meseguer, and C. Muñoz, Rewriting modulo SMT and open system analysis, Journal of Logical and Algebraic Methods in Programming, vol.86, issue.1, pp.269-297, 2017.
DOI : 10.1016/j.jlamp.2016.10.001

URL : https://riuma.uma.es/xmlui/bitstream/10630/16949/1/conf-rocha.pdf

P. Viry, Equational rules for rewriting logic, Theoretical Computer Science, vol.285, issue.2, pp.487-517, 2002.
DOI : 10.1016/S0304-3975(01)00366-8

URL : https://doi.org/10.1016/s0304-3975(01)00366-8

D. J. White, Markov Decision Processes, 1993.

P. Wong and J. Gibbons, A Process Semantics for BPMN, Proc. of ICFEM, pp.355-374, 2008.
DOI : 10.1016/j.jlap.2006.05.007

P. Wong and J. Gibbons, Verifying Business Process Compatibility, Proc. of QSIC, pp.126-131, 2008.
DOI : 10.1109/qsic.2008.6

M. T. Wynn, H. M. Verbeek, W. M. Van-der-aalst, A. H. Ter-hofstede, and D. Edmond, Business Process Verification -Finally a Reality! Business Process Management Journal, pp.74-92, 2009.