{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T17:48:12Z","timestamp":1754156892346,"version":"3.41.2"},"reference-count":21,"publisher":"Emerald","issue":"3","license":[{"start":{"date-parts":[[2015,6,1]],"date-time":"2015-06-01T00:00:00Z","timestamp":1433116800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.emerald.com\/insight\/site-policies"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,6,1]]},"abstract":"\n Purpose<\/jats:title>\n \u2013 An integral part of declarative process modelling is to guarantee that the execution of a declarative workflow is compliant with the respective business rules. The purpose of this paper is to establish a formal framework for representing business rules and determining whether any business rules are violated during the executions of declarative process models. <\/jats:p>\n <\/jats:sec>\n \n Design\/methodology\/approach<\/jats:title>\n \u2013 In the approach, a business rule is phrased in terms of restricted English that is related to a constraint template. Linear temporal logic (LTL) is employed as a formalism for defining the set of constraint templates. By exploiting the theorem-proving feature of the Logics Workbench (LWB), business rule violations are then detected in an automatic manner. <\/jats:p>\n <\/jats:sec>\n \n Findings<\/jats:title>\n \u2013 This study explored the viability of encoding: first, process executions by means of LTL and second, business rules in terms of restricted English that built upon pattern-oriented templates and LTL. The LWB was used for carrying out temporal reasoning through automated techniques. The applicability of the formal verification approach was exemplified by a case study concerning supply chain management. The findings showed that practical reasoning could be achieved by combining declarative process modelling, restricted English, pattern-oriented templates, LTL and LWB. <\/jats:p>\n <\/jats:sec>\n \n Originality\/value<\/jats:title>\n \u2013 First, new business rule templates are proposed; second, business rules are expressed in restricted English instead of graphical constructs; third, both finite execution trace and business rules are grounded in LTL. There is no need to deal with the semantic differences between different formalisms; and finally, the theorem prover LWB is used for the conformance checking of a finite execution trace against business rules.<\/jats:p>\n <\/jats:sec>","DOI":"10.1108\/bpmj-10-2014-0092","type":"journal-article","created":{"date-parts":[[2015,5,28]],"date-time":"2015-05-28T11:32:26Z","timestamp":1432812746000},"page":"586-609","source":"Crossref","is-referenced-by-count":2,"title":["Constraint-based reasoning on declarative process execution with the logics workbench"],"prefix":"10.1108","volume":"21","author":[{"given":"Vitus","family":"Lam","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"140","reference":[{"key":"key2020122303123757000_b16","unstructured":"Awad, A.\n (2007), \u201cBPMN-Q: a language to query business processes\u201d, \n EMISA\n , pp. 115-128."},{"key":"key2020122303123757000_b15","doi-asserted-by":"crossref","unstructured":"Awad, A.\n , \n Weidlich, M.\n and \n Weske, M.\n (2011), \u201cVisually specifying compliance rules and explaining their violations for business processes\u201d, \n Journal of Visual Languages and Computing\n , Vol. 22 No. 1, pp. 30-55.","DOI":"10.1016\/j.jvlc.2010.11.002"},{"key":"key2020122303123757000_b20","unstructured":"Bauer, A.\n and \n Haslum, P.\n (2010), \u201cLTL goal specifications revisited\u201d, 19th European Conference on Artificial Intelligence, pp. 881-886."},{"key":"key2020122303123757000_b8","unstructured":"Clarke, E.M.\n , \n Grumberg, O.\n and \n Peled, D.A.\n (1999), \n Model Checking\n , MIT Press, Cambridge, MA."},{"key":"key2020122303123757000_b1","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B.\n , \n Avrunin, G.S.\n and \n Corbett, J.C.\n (1998), \u201cProperty specification patterns for finite-state verification\u201d, Proceedings of the Second Workshop on Formal Methods in Software Practice, pp. 7-15.","DOI":"10.1145\/298595.298598"},{"key":"key2020122303123757000_b2","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B.\n , \n Avrunin, G.S.\n and \n Corbett, J.C.\n (1999), \u201cPatterns in property specifications for finite-state verification\u201d, in \n Boehm, B.W.\n , \n Garlan, D.\n and \n Kramer, J.\n (Eds), \n ICSE \u201999\n , IEEE Computer Society Press, New York, NY, pp. 411-420.","DOI":"10.1145\/302405.302672"},{"key":"key2020122303123757000_b19","doi-asserted-by":"crossref","unstructured":"Goedertier, S.\n , \n Haesen, R.\n and \n Vanthienen, J.\n (2007), \u201cEM-BrA2CE v0.1: a vocabulary and execution model for declarative business process modeling\u201d, technical report, Department of Decision Sciences and Information Management, K.U. Leuven.","DOI":"10.2139\/ssrn.1086027"},{"key":"key2020122303123757000_b14","unstructured":"Hoare, C.A.R.\n (1985), \n Communicating Sequential Processes\n , Prentice-Hall, Englewood Cliffs, NJ."},{"key":"key2020122303123757000_b9","doi-asserted-by":"crossref","unstructured":"Huth, M.\n and \n Ryan, M.\n (2004), \n Logic in Computer Science: Modelling and Reasoning about Systems\n , 2nd ed., Cambridge University Press, Cambridge.","DOI":"10.1017\/CBO9780511810275"},{"key":"key2020122303123757000_b21","unstructured":"Law, V.S.W.\n (2014), Constraint-based reasoning on declarative process execution with the Logics Workbench (extended version), Technical report no. BPM-14-01, HKU."},{"key":"key2020122303123757000_b10","unstructured":"LWB 1.1 Reference Manual\n (1997), available at: www.lwb.unibe.ch\/, accessed 26 April 2014."},{"key":"key2020122303123757000_b18","doi-asserted-by":"crossref","unstructured":"Maggi, F.M.\n , \n Montali, M.\n , \n Westergaard, M.\n and \n van der Aalst, W.M.P.\n (2011), \u201cMonitoring business constraints with linear temporal logic: an approach based on colored automata\u201d, BPM 2011, LNCS 6896, pp. 132-147.","DOI":"10.1007\/978-3-642-23059-2_13"},{"key":"key2020122303123757000_b6","unstructured":"Pesic, M.\n (2008), \u201cConstraint-based workflow management systems: shifting control to users\u201d, PhD thesis, Eindhoven University of Technology, Eindhoven, 8 October."},{"key":"key2020122303123757000_b17","doi-asserted-by":"crossref","unstructured":"Pesic, M.\n , \n Schonenberg, M.H.\n , \n Sidorova, N.\n and \n van der Aalst, W.M.P.\n (2007), \u201cConstraint-based workflow models: change made easy\u201d, \n OTM 2007\n , pp. 77-94.","DOI":"10.1007\/978-3-540-76848-7_7"},{"key":"key2020122303123757000_b11","unstructured":"Runte, W.\n and \n El Kharbili, M.\n (2009), \u201cConstraint checking for business process management\u201d, \n GI Jahrestagung\n , pp. 4093-4103."},{"key":"key2020122303123757000_b3","unstructured":"Specification Patterns\n , available at: http:\/\/patterns.projects.cis.ksu.edu (accessed 10 March 2014)."},{"key":"key2020122303123757000_b4","unstructured":"van der Aalst, W.M.P.\n and \n Pesic, M.\n (2006), \u201cSpecifying, discovering, and monitoring service flows: making web services process-aware\u201d, Technical Report No. BPM-06-09, BPM Center, Eindhoven."},{"key":"key2020122303123757000_b5","unstructured":"van der Aalst, W.M.P.\n and \n Pesic, M.\n (2007), \u201cSpecifying and monitoring service flows: making web services process-aware\u201d, in, \n Baresi, L.\n and \n Di Nitto, E.\n (Eds), \n Test and Analysis of Web Services\n , Springer, Berlin Heidelberg, pp. 11-55."},{"key":"key2020122303123757000_b7","doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P.\n , \n Pesic, M.\n and \n Schonenberg, H.\n (2009), \u201cDeclarative workflows: balancing between flexibility and support\u201d, \n Computer Science \u2013 Research and Development\n , Vol. 23 No. 2, pp. 99-113.","DOI":"10.1007\/s00450-009-0057-9"},{"key":"key2020122303123757000_b12","doi-asserted-by":"crossref","unstructured":"Wong, P.Y.H.\n and \n Gibbons, J.\n (2009), \u201cProperty specifications for workflow modelling\u201d, \n IFM\n , pp. 56-71.","DOI":"10.1007\/978-3-642-00255-7_5"},{"key":"key2020122303123757000_b13","doi-asserted-by":"crossref","unstructured":"Wong, P.Y.H.\n and \n Gibbons, J.\n (2011), \u201cProperty specifications for workflow modelling\u201d, \n Science of Computer Programming\n , Vol. 76 No. 10, pp. 942-967.","DOI":"10.1016\/j.scico.2010.09.007"}],"container-title":["Business Process Management Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.emeraldinsight.com\/doi\/full-xml\/10.1108\/BPMJ-10-2014-0092","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/BPMJ-10-2014-0092\/full\/xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/BPMJ-10-2014-0092\/full\/html","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,24]],"date-time":"2025-07-24T23:16:08Z","timestamp":1753398968000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.emerald.com\/bpmj\/article\/21\/3\/586-609\/257989"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,1]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6,1]]}},"alternative-id":["10.1108\/BPMJ-10-2014-0092"],"URL":"https:\/\/doi.org\/10.1108\/bpmj-10-2014-0092","relation":{},"ISSN":["1463-7154"],"issn-type":[{"type":"print","value":"1463-7154"}],"subject":[],"published":{"date-parts":[[2015,6,1]]}}}