Enacting declarative languages using LTL : avoiding errors and improving performance

Onderzoeksoutput: Boek/rapportRapportAcademic

126 Downloads (Pure)


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.
Originele taal-2Engels
Plaats van productieEindhoven
UitgeverijTechnische Universiteit Eindhoven
Aantal pagina's16
StatusGepubliceerd - 2009

Publicatie series

NaamComputer science reports
ISSN van geprinte versie0926-4515

Vingerafdruk Duik in de onderzoeksthema's van 'Enacting declarative languages using LTL : avoiding errors and improving performance'. Samen vormen ze een unieke vingerafdruk.

Citeer dit