Abstract
Given that organizations rely on the support of information systems in automating their business processes, the auditing of these processes is a complex task because it needs to consider both the business process model and the relevant data logs. For the compliance checking of such business situations, we present an extended version of a Hybrid Logics model checking tool, with temporal operators. The support for temporal operators allows for tracing the event logs and the verification of properties, within an abstract representation model corresponding to the intended concern of auditing.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
References
Aldewereld, H., Alvarez-Napagao, S., Dignum, F., Vazquez-Salceda, J.: Making norms concrete. In: 8th International Conference on Autonomous Agents and Multiagent Systems, pp. 807–814 (2009)
Areces, C., Ten Cate, B.: Hybrid logics. In: Blackburn, P., Van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 821–868. Elsevier, Amsterdam (2007)
Arellano, G., Argil, J., Azpeitia, E., Benítez, M., Carrillo, M., Góngora, P., Rosenblueth, D.A., Alvarez-Buylla, E.R.: “antelope”: a hybrid-logic model checker for branching-time boolean grn analysis. BMC Bioinform. 12(1) (2011)
Blackburn, P., Tzakova, M.: Hybrid languages and temporal logic. Logic J. IGPL 7(1), 27–54 (1999)
Caron, F., Vanthienen, J., Baesens, B.: Comprehensive rule-based compliance checking and risk management with process mining. Decis. Support Syst. 54(3), 1357–1369 (2013)
Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at ltl model checking. Formal Methods Syst. Des. 10(1), 47–71 (1997)
Cranefield, S., Winikoff, M.: Verifying social expectations by model checking truncated paths. J. Logic Comput. 21(6), 1217–1256 (2011)
de Leoni, M., Maggi, F.M., van der Aalst, W.M.: An alignment-based framework to check the conformance of declarative process models and to preprocess event-log data. Information Systems (2014)
Franceschet, M., de Rijke, M.: Model checking hybrid logics (with an application to semistructured data). J. Appl. Logic 4, 279–304 (2006)
Hildebrandt, T.T., Mukkamala, R.R.: Declarative event-based workflow as distributed dynamic condition response graphs, Springer. In: Programming Language Approaches to Concurrency and Communication-cEntric Software (2010)
Hull, R., Damaggio, E., De Masellis, R., Fournier, F., Gupta, M., Heath, F.T., III, Hobson, S., Linehan, M., Maradugu, S., Nigam, A., Sukaviriya, P.N., Vaculin, R.: 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, DEBS’11, pp. 51–62, ACM, New York, NY, USA (2011)
Lange, M.: Model checking for hybrid logic. J. Logic, Lang. Inform. 18(4), 465–491 (2009)
Mosca, A., Manzoni, L., Codecasa, D.: HyLMoC: a model checker for hybrid logic. In: Gavanelli, M., Riguzzi, F. (eds.) CILC09: 24-esimo Convegno Italiano di Logica Computazionale. Ferrara, Italy (2009)
Schultz, M.: Enriching process models for business process compliance checking in erp environments. In: vom Brocke, J., Hekkala, R., Ram, S., Rossi, M. (eds.) Design Science at the Intersection of Physical and Virtual Design. Lecture Notes in Computer Science, vol. 7939, pp. 120–135. Springer, Berlin (2013)
Troquard, N., Hoek, W., Wooldridge, M.: Model checking strategic equilibria. Chapter model checking and artificial intelligence, pp. 166–188. Springer, Berlin (2009)
Zhang, Y., Ding, Y.: Ctl model update for system modifications. J. Artif. Int. Res. 31(1), 113–155 (2008)
Acknowledgments
The authors gratefully acknowledge the support by CNCSIS-UEFICSU, National Research Council of the Romanian Ministry for Education and Research, project ID_170/2009.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Letia, I.A., Goron, A. (2016). Verifying Compliance for Business Process Logs with a Hybrid Logic Model Checker. In: Hatzilygeroudis, I., Palade, V., Prentzas, J. (eds) Combinations of Intelligent Methods and Applications. Smart Innovation, Systems and Technologies, vol 46. Springer, Cham. https://doi.org/10.1007/978-3-319-26860-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-26860-6_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-26858-3
Online ISBN: 978-3-319-26860-6
eBook Packages: EngineeringEngineering (R0)