Patterns for a Log-Based Strengthening of Declarative Compliance Models

  • Dennis M. M. Schunselaar
  • Fabrizio M. Maggi
  • Natalia Sidorova
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7321)


LTL-based declarative process models are very effective when modelling loosely structured processes or working in environments with a lot of variability. A process model is represented by a set of constraints that must be satisfied during the process execution. An important application of such models is compliance checking: a process model defines then the boundaries in which a system/organisation may work, and the actual behaviour of the system, recorded in an event log, can be checked on its compliance to the given model.

A compliance model is often a general one, e.g., applicable for a whole branch of industry, and some constraints used there may be irrelevant for a company in question: for example, a constraint related to property assessment regulations will be irrelevant for a rental agency that does not execute property assessment at all. In this paper, we take the compliance model and the information about past executions of the process instances registered in an event log and, by using a set of patterns, we check which constraints of the compliance model are irrelevant (vacuously satisfied) with respect to the event log. Our compliance patterns are inspired by vacuity detection techniques working on a single trace. However, here we take all the knowledge available in the log into consideration.


Linear Temporal Logic Declare Vacuity detection Compliance checking Event log 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    van der Aalst, W.M.P., Pesic, M., Schonenberg, M.H.: Declarative workflows: Balancing between flexibility and support. Computer Science - Research and Development 23, 99–113 (2009)CrossRefGoogle Scholar
  2. 2.
    Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient Detection of Vacuity in Temporal Model Checking. Formal Methods in System Design 18, 141–163 (2001)zbMATHCrossRefGoogle Scholar
  3. 3.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 411–420. ACM (1999)Google Scholar
  4. 4.
    van Hee, K.M., Liu, Z., Sidorova, N.: Is my event log complete? - A probabilistic approach to process mining. In: Proceedings of RCIS 2011, pp. 1–7. IEEE (2011)Google Scholar
  5. 5.
    Knuplesch, D., Ly, L.T., Rinderle-Ma, S., Pfeifer, H., Dadam, P.: On Enabling Data-Aware Compliance Checking of Business Process Models. In: Parsons, J., Saeki, M., Shoval, P., Woo, C., Wand, Y. (eds.) ER 2010. LNCS, vol. 6412, pp. 332–346. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Kupferman, O., Vardi, M.Y.: Vacuity Detection in Temporal Model Checking. International Journal on Software Tools for Technology Transfer 4(2), 224–233 (2003)CrossRefGoogle Scholar
  7. 7.
    Lamma, E., Mello, P., Montali, M., Riguzzi, F., Storari, S.: Inducing Declarative Logic-Based Models from Labeled Traces. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 344–359. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Lichtenstein, O., Pnueli, A., Zuck, L.D.: The Glory of the Past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)CrossRefGoogle Scholar
  9. 9.
    Maggi, F.M., Mooij, A.J., van der Aalst, W.M.P.: Analyzing Vessel Behavior using Process Mining in the Poseidon book edited by Springer (to appear)Google Scholar
  10. 10.
    Maggi, F.M., Montali, M., Westergaard, M., van der Aalst, W.M.P.: Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata. In: Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol. 6896, pp. 132–147. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  11. 11.
    Maggi, F.M., Mooij, A.J., van der Aalst, W.M.P.: User-guided discovery of declarative process models. In: Proceedings of CIDM 2011, pp. 192–199. IEEE (2011)Google Scholar
  12. 12.
    Montali, M., Maggi, F.M., Chesani, F., Mello, P., van der Aalst, W.M.P.: Monitoring Business Constraints with the Event Calculus. Technical Report DEIS-LIA-002-11, University of Bologna, Italy (2011)Google Scholar
  13. 13.
    Pesic, M., van der Aalst, W.M.P.: A Declarative Approach for Flexible Business Processes Management. In: Eder, J., Dustdar, S. (eds.) BPM Workshops 2006. LNCS, vol. 4103, pp. 169–180. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Pesic, M., Schonenberg, M.H., Sidorova, N., van der Aalst, W.M.P.: Constraint-Based Workflow Models: Change Made Easy. In: Meersman, R., Tari, Z. (eds.) OTM 2007, Part I. LNCS, vol. 4803, pp. 77–94. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Pesic, M., Schonenberg, M.H., van der Aalst, W.M.P.: DECLARE: Full Support for Loosely-Structured Processes. In: Proceedings of EDOC 2007, pp. 287–300. IEEE Computer Society (2007)Google Scholar
  16. 16.
    Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of FOCS 1977, pp. 46–57. IEEE Computer Society (1977)Google Scholar
  17. 17.
    Purandare, M., Somenzi, F.: Vacuum Cleaning CTL Formulae. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 485–499. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Dennis M. M. Schunselaar
    • 1
  • Fabrizio M. Maggi
    • 1
  • Natalia Sidorova
    • 1
  1. 1.Eindhoven University of TechnologyThe Netherlands

Personalised recommendations