Enacting declarative languages using LTL : avoiding errors and improving performance

In our earlier work we have proposed using the declarative language DecSerFlow for modeling, analysis and enactment of web service processes. DecSerFlow uses constraints, which are formally specified as Linear Temporal Logic (LTL) formulas, to implicitly define possible executions of a model: any execution that satisfies all constraints is possible. A finite representation of all possible executions is retrieved as an automaton generated from LTL-based constraints. Standard algorithms for creating B¨uchi automata from LTL formulas cause errors when be applied to DecSerFlow due to important semantical differences. On the one hand, LTL handles infinite traces where each element of the trace can refer to zero or more propositions. On the other hand, executions of DecSerFlow models are finite sequences of single events. In this paper we describe how both LTL and automata generation algorithms can be adjusted to fit two properties of DecSerFlow. Since adjustments for finite traces have already been proposed by other researchers, this paper focuses on the modifications needed to handle occurrences of single events. Besides eliminating errors caused by the described mismatch, the proposed adjustments also improve the performance of the model checking algorithms dramatically. This is important as for the enactment of declarative languages like DecSerFlow new problems related to model checking techniques are generated after each step in the process.