Enacting declarative languages using LTL: Avoiding errors and improving performance

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

32 Citations (Scopus)


In our earlier work we 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üchi 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 LTL and automata generation algorithm needed to handle occurrences of single events. Besides eliminating errors caused by the ‘multiple properties - single events’ mismatch, the proposed adjustments also improve the performance of the automata generation algorithms dramatically.
Original languageEnglish
Title of host publicationModel Checking Software (17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010)
EditorsJ. Pol, van de, M. Weber
Place of PublicationBerlin
ISBN (Print)978-3-642-16163-6
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Enacting declarative languages using LTL: Avoiding errors and improving performance'. Together they form a unique fingerprint.

Cite this