Workflow Nets Verification: SMT or CLP?

  • Hadrien Bride
  • Olga Kouchnarenko
  • Fabien Peureux
  • Guillaume VoironEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9933)


The design and the analysis of business processes commonly relies on workflow nets, a suited class of Petri nets. This paper evaluates and compares two resolution methods—Satisfiability Modulo Theory (SMT) and Constraint Logic Programming (CLP)—applied to the verification of modal specifications over workflow nets. Firstly, it provides a concise description of the verification methods based on constraint solving. Secondly, it presents the experimental protocol designed to evaluate and compare the scalability and efficiency of both resolution approaches. Thirdly, the paper reports on the obtained results and discusses the lessons learned from these experiments.


Workflow nets Modal specifications Verification method Experimental comparison Satisfiability modulo theory Constraint solving problem 


  1. 1.
    Bride, H., Kouchnarenko, O., Peureux, F.: Verifying modal workflow specifications using constraint solving. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 171–186. Springer, Heidelberg (2014)Google Scholar
  2. 2.
    Tsang, E.P.K.: Foundations of Constraint Satisfaction. Computation in Cognitive Science. Academic Press, San Diego (1993)Google Scholar
  3. 3.
    De Moura, L., Bjørner, N.: Satisfiability modulo theories: Introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRefGoogle Scholar
  4. 4.
    van der Aalst, W.M.P.: The application of Petri nets to workflow management. J. Circ. Syst. Comput. 08(01), 21–66 (1998)CrossRefGoogle Scholar
  5. 5.
    Murata, T.: Petri nets: properties, analysis and applications. IEEE 77(4), 541–580 (1989)CrossRefGoogle Scholar
  6. 6.
    de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Carlsson, M., et al.: SICStus Prolog User’s Manual (Release 4.2.3). Swedish Institute of Computer Science, Kista (2012)Google Scholar
  8. 8.
    Bi, H., Zhao, J.: Applying propositional logic to workflow verification. Inf. Technol. Manag. 5(3–4), 293–318 (2004)CrossRefGoogle Scholar
  9. 9.
    Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Logical Methods Comput. Sci. 8(3), 827–846 (2012)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Haddad, S.: Decidability and complexity of Petri net problems. In: Petri Nets: Fundamental Models, Verification and Applications, pp. 87–122 (2009)Google Scholar
  11. 11.
    Larsen, K., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science, LICS 1988, pp. 203–210 (1988)Google Scholar
  12. 12.
    Kouchnarenko, O., Sidorova, N., Trcka, N.: Petri nets with may/must semantics. In: Workshop on Concurrency, Specification, and Programming, CS&P 2009, Kraków-Przegorzaly, Poland, vol. 1, September 2009Google Scholar
  13. 13.
    Monakova, G., Kopp, O., Leymann, F., Moser, S., Schäfers, K.: Verifying business rules using an SMT solver for BPEL processes. In: BPSC. LNI, vol. 147, pp. 81–94. GI (2009)Google Scholar
  14. 14.
    Pólrola, A., Cybula, P., Meski, A.: Smt-based reachability checking for bounded time Petri nets. Fundam. Inform. 135(4), 467–482 (2014)MathSciNetzbMATHGoogle Scholar
  15. 15.
    Kleine, M., Göthel, T.: Specification, verification and implementation of business processes using CSP. In: TASE, pp. 145–154. IEEE Computer Society (2010)Google Scholar
  16. 16.
    Soliman, S.: Finding minimal p/t-invariants as a CSP. In: Proceedings of the 4th Workshop on Constraint Based Methods for Bioinformatics, WCB, vol. 8 (2008)Google Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Hadrien Bride
    • 1
  • Olga Kouchnarenko
    • 1
  • Fabien Peureux
    • 1
  • Guillaume Voiron
    • 1
    Email author
  1. 1.Institut FEMTO-ST – UMR CNRS 6174University of Franche-ComtéBesançonFrance

Personalised recommendations