Sciweavers

Share
SPIN
2010
Springer

Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance

8 years 5 months ago
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...
Maja Pesic, Dragan Bosnacki, Wil M. P. van der Aal
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where SPIN
Authors Maja Pesic, Dragan Bosnacki, Wil M. P. van der Aalst
Comments (0)
books