Model Checking of Constraint-Based Workflow Based on Linear Temporal Logic

Abstract:

The degree of flexibility of workflow management systems heavily influences the way business processes are executed. Constraint-based models are considered to be more flexible than traditional models because of their semantics: everything that does not violate constraints is allowed. More and more people use declarative languages to define workflow, such as linear temporal logic. But how to guarantee the correctness of the model based on the linear temporal logic is still a problem. This article proposes a way to verify the model based on Büchi automaton and gives the corresponding algorithms. Thus the verification of declarative workflow based on the linear temporal logic is solved.

• Periodical: Advanced Materials Research (Volume 601)
• Pages: 401-405
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.601.401
• Online since: December 2012
• Authors: Wen Bo Zhou, Shu Zhen Yao
• Keywords: Büchi Automata, Constraint-Based Workflow, Linear Temporal Logic, Model Checking

References

[1] N. Russell, A.H.M. ter Hofstede, D. Edmond, and W.M.P. van der Aalst. Workflow Data Patterns. QUT Technical report, FIT-TR-2004-01, Queensland University of Technology, Brisbane, (2004).

[2] M. Pesic, H. Schonenberg, and W. Aalst, Declarative Workflow, , A. H. M. Hofstede, W. M. P. Aalst, M. Adams, and N. Russell, Ed., Springer Berlin Heidelberg, 2010, pp.175-201.

DOI: 10.1007/978-3-642-03121-2_6

[3] M. Pesic and W. van der Aalst, A Declarative Approach for Flexible Business Processes Management, , J. Eder and S. Dustdar, Ed., Springer Berlin / Heidelberg, 2006, vol. 4103, pp.169-180.

DOI: 10.1007/11837862_18

[4] Gerth R, Peled D, Vardi M Y, et al. Simple on-the-fly automatic verification of linear temporal logic. In: Proc. 15th Work. Protocol Specification, Testing, and Verification. Warsaw, Poland, 1995: 3-18.

DOI: 10.1007/978-0-387-34892-6_1

[5] Gastin P, Oddoux D. Fast LTL to Büchi automata translation. Lecture Notes in Computer Science, 2001, 2102: 53-65.

DOI: 10.1007/3-540-44585-4_6

[6] M. Pesic, H. Schonenberg, and W. M. P. van der Aalst, DECLARE: Full Support for Loosely-Structured Processes. Washington, DC, USA: IEEE Computer Society, 2007, p.287.

DOI: 10.1109/edoc.2007.14

[7] Giannakopoulou D, Lerda F. Efficient translation of LTL formulae into Büchi automata. In: RIACS Technical Report. (2001).

[8] M. Pesic, M. Schonenberg, N. Sidorova, and W. van der Aalst, Constraint-Based Workflow Models: Change Made Easy, , R. Meersman and Z. Tari, Ed., Springer Berlin / Heidelberg, 2007, vol. 4803, pp.77-94.

DOI: 10.1007/978-3-540-76848-7_7

[9] Giannakopoulou D, Lerda F. From states to transitions: Improving translation of LTL formulae to Büchi automata. Lecture Notes in Computer Science, 2002, 2529: 308-326.

DOI: 10.1007/3-540-36135-9_20

[10] A. Bauer, M. Leucker, and C. Schallhart. Comparing LTL Semantics for Runtime Verification. Logic and Computation, 20(3): 651-674, (2010).

DOI: 10.1093/logcom/exn075

[11] REGEV G, SOFFER P, SCHMIDT R. Taxonomy of flexibility in business processes[EB/OL](2006-06-06)[2009-09-07].