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 processes in autonomous web services. DecSerFlow uses constraints specified with Linear Temporal Logic (LTL) to implicitly define possible executions of a model: any execution that satisfies all constraints is possible. Hence, a finite representation of all possible executions is retrieved as an automaton generated from LTL-based constraints. Standard model checking algorithms for creating B¨uchi automata from LTL formulas are not applicable because of the requirements posed by the proper execution of DecSerFlow (and LTL-based process engines). On the one hand, LTL handles infinite words where each element of the word can refer to zero or more propositions. On the other hand, each execution of a DecSerFlow model is a finite sequence of single events. In this paper we adopt an existing approach to finite-word semantics of LTL and propose the modifications of LT...

• Type: Journal
• Year: 2010
• Where: SPIN
• Authors: Maja Pesic, Dragan Bosnacki, Wil M. P. van der Aalst
• Keywords: Linear Temporal Logic, Possible Executions, Single Events, SPIN 2010, Theoretical Computer Science