Better Algorithms for Analyzing and Enacting Declarative Workflow Languages Using LTL

  • Michael Westergaard
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6896)


Declarative workflow languages are easy for humans to understand and use for specifications, but difficult for computers to check for consistency and use for enactment. Therefore, declarative languages need to be translated to something a computer can handle. One approach is to translate the declarative language to linear temporal logic (LTL), which can be translated to finite automata. While computers are very good at handling finite automata, the translation itself is often a road block as it may take time exponential in the size of the input. Here, we present algorithms for doing this translation much more efficiently (around a factor of 10,000 times faster and handling 10 times larger systems on a standard computer), making declarative specifications scale to realistic settings.


Linear Temporal Logic Finite Automaton Atomic Proposition Proof Obligation Binary Decision Diagram 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bryant, R.E.: Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)CrossRefzbMATHGoogle Scholar
  2. 2.
    Chesani, F., Mello, P., Montali, M., Torroni, P.: Verification of Choreographies During Execution Using the Reactive Event Calculus. In: Bruni, R., Wolf, K. (eds.) WS-FM 2008. LNCS, vol. 5387, pp. 55–72. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  3. 3.
    Declare webpage,
  4. 4.
    Etessami, K., Holzmann, G.J.: Optimizing Büchi Automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–168. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  5. 5.
    Garey, M.R., Johnson, D.S., Stockmeyer, L.: Some simplified NP-complete graph problems. Theoretical Computer Science 1, 237–267 (1976)CrossRefzbMATHGoogle Scholar
  6. 6.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple On-the-fly Automatic Verification of Linear Temporal Logic. In: Proc. of Protocol Specification, Testing and Verification, pp. 3–18 (1995)Google Scholar
  7. 7.
    Giannakopoulou, D., Havelund, K.: Automata-Based Verification of Temporal Properties on Running Programs. In: Proc. of ASE 2001, pp. 412–416. IEEE Computer Society, Los Alamitos (2001)Google Scholar
  8. 8.
    Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite automaton. Technical report, Stanford University (1971)Google Scholar
  9. 9.
    Kamp, H.W.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California (1968)Google Scholar
  10. 10.
    Kimura, S., Clarke, E.M.: A parallel algorithm for constructing binary decision diagrams. In: Proc. of ICCD 1990, pp. 220–223 (1990)Google Scholar
  11. 11.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)CrossRefzbMATHGoogle Scholar
  12. 12.
    Object Management Group (OMG). Business Process Modeling Notation (BPML). Version 2.0. OMG Avaiable SpecificationGoogle Scholar
  13. 13.
    Paige, R., Tarjan, R.E.: Three Partition Refinement Algorithms. SIAM Journal on Computing 16(6), 973–989 (1987)CrossRefzbMATHGoogle Scholar
  14. 14.
    Pei, M., Bonaki, D., van der Aalst, W.M.P.: Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol. 6349, pp. 146–161. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    Pei, M., Schonenberg, M.H., Sidorova, N., van der Aalst, W.M.P.: Constraint-Based Workflow Models: Change Made Easy. In: Chung, S. (ed.) OTM 2007, Part I. LNCS, vol. 4803, pp. 77–94. Springer, Heidelberg (2007)Google Scholar
  16. 16.
    Ravikumar, B., Xiong, X.: A Parallel Algorithm for Minimization of Finite Automata. In: Proc. of IPPS 1996, pp. 187–191. IEEE Computer Society, Los Alamitos (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Michael Westergaard
    • 1
  1. 1.Department of Mathematics and Computer ScienceEindhoven University of TechnologyThe Netherlands

Personalised recommendations